week1: functional ocaml turing complete after all
[lambda.git] / week2.mdwn
index 2612dd2..b43576f 100644 (file)
@@ -1,5 +1,55 @@
 [[!toc]]
 
+Substitution and Alpha-Conversion
+=================================
+
+Intuitively, (a) and (b) express the application of the same function to the argument `y`:
+
+<OL type=a>
+<LI><code>(\x. \z. z x) y</code>
+<LI><code>(\x. \y. y x) y</code>
+</OL>
+
+One can't just rename variables freely. (a) and (b) are different than what's expressed by:
+
+<OL type=a start=3>
+<LI><code>(\z. (\z. z z) y</code>
+</OL>
+
+
+Substituting `y` into the body of `(\x. \z. z x)` is unproblematic:
+
+       (\x. \z. z x) y ~~> \z. z y
+
+However, with (b) we have to be more careful. If we just substituted blindly, then we might take the result to be `\y. y y`. But this is the self-application function, not the function which accepts an arbitrary argument and applies that argument to the free variable `y`. In fact, the self-application function is what (c) reduces to. So if we took (b) to reduce to `\y. y y`, we'd wrongly be counting (b) to be equivalent to (c), instead of (a).
+
+To reduce (b), then, we need to be careful to that no free variables in what we're substituting in get captured by binding &lambda;s that they shouldn't be captured by.
+
+In practical terms, you'd just replace (b) with (a) and do the unproblematic substitution into (a).
+
+What attitude should we have to this?
+
+One way to think of it is to identify expressions of the lambda calculus with particular alphabetic sequences. Then (a) and (b) would be distinct expressions, and we'd have to explicitly articulate a rule permitting you to do the kind of variable-renaming that would take you from (a) to (b) (or vice versa). This kind of renaming is called "alpha-conversion."
+
+Another way to think of it is to identify expressions not with particular alphabetic sequences, but rather with classes of alphabetic sequences, which stand to each other in the way that (a) and (b) do. That's the way we'll talk. We say that (a) and (b) are just typographically different notations for a *single* lambda formula. As we'll say, the lambda formula written with (a) and the lambda formula written with (b) are literally syntactically identical.
+
+A third way to think is to identify the lambda formula not with classes of alphabetic sequences, but rather with abstract structures that we might draw like this:
+
+<pre><code>
+       &lambda; ... ___ ...
+       ^      |
+       |______|
+</code></pre>
+
+Here there are no bound variables, but there are *bound positions*. We can regard formula like (a) and (b) as just helpfully readable ways to designate these abstract structures.
+
+A version of this last approach is known as **de Bruijn notation** for the lambda calculus.
+
+It doesn't matter which of these approaches one takes; the logical properties of the systems are exactly the same. It just affects the particulars of how one states the rules for substitution, and so on. And whether one talks about expressions being literally "syntactically identical," or whether one instead counts them as "equivalent modulu alpha-conversion."
+
+(In a bit, we'll discuss other systems that lack variables. Those systems will not just lack variables in the sense that de Bruijn notation does; they will furthermore lack any notion of a bound position.)
+
+
 
 Syntactic equality, reduction, convertibility
 =============================================
@@ -121,7 +171,7 @@ Combinatory Logic is what you have when you choose a set of combinators and regu
 We've claimed that Combinatory Logic is equivalent to the lambda calculus.  If that's so, then S, K, and I must be enough to accomplish any computational task imaginable.  Actually, S and K must suffice, since we've just seen that we can simulate I using only S and K.  In order to get an intuition about what it takes to be Turing complete, imagine what a text editor does:
 it transforms any arbitrary text into any other arbitrary text.  The way it does this is by deleting, copying, and reordering characters.  We've already seen that K deletes its second argument, so we have deletion covered.  S duplicates and reorders, so we have some reason to hope that S and K are enough to define arbitrary functions.  
 
-We've already established that the behavior of combinatory terms can be perfectly mimicked by lambda terms: just replace each combinator with its equivalent lambda term, i.e., replace I with `\x.x`, replace K with `\fxy.x`, and replace S with `\fgx.fx(gx)`.  How about the other direction?  Here is a method for converting an arbitrary lambda term into an equivalent Combinatory Logic term using only S, K, and I.  Besides the intrinsic beauty of this mapping, and the importance of what it says about the nature of binding and computation, it is possible to hear an echo of computing with continuations in this conversion strategy (though you would be able to hear these echos until we've covered a considerable portion of the rest of the course).
+We've already established that the behavior of combinatory terms can be perfectly mimicked by lambda terms: just replace each combinator with its equivalent lambda term, i.e., replace I with `\x.x`, replace K with `\fxy.x`, and replace S with `\fgx.fx(gx)`.  How about the other direction?  Here is a method for converting an arbitrary lambda term into an equivalent Combinatory Logic term using only S, K, and I.  Besides the intrinsic beauty of this mapping, and the importance of what it says about the nature of binding and computation, it is possible to hear an echo of computing with continuations in this conversion strategy (though you wouldn't be able to hear these echos until we've covered a considerable portion of the rest of the course).
 
 Assume that for any lambda term T, [T] is the equivalent combinatory logic term.  The we can define the [.] mapping as follows:
 
@@ -148,7 +198,7 @@ Let's check that the translation of the false boolean behaves as expected by fee
 
 Throws away the first argument, returns the second argument---yep, it works.
 
-Here's a more elaborat example of the translation.  The goal is to establish that combinators can reverse order, so we use the T combinator, where `T = \x\y.yx`:
+Here's a more elaborate example of the translation.  The goal is to establish that combinators can reverse order, so we use the T combinator, where `T = \x\y.yx`:
 
     [\x\y.yx] = [\x[\y.yx]] = [\x.S[\y.y][\y.x]] = [\x.(SI)(Kx)] = S[\x.SI][\x.Kx] = S(K(SI))(S[\x.K][\x.x]) = S(K(SI))(S(KK)I)
 
@@ -271,16 +321,29 @@ This question highlights that there are different choices to make about how eval
 
 With regard to Q3, it should be intuitively clear that `\x. M x` and `M` will behave the same with respect to any arguments they are given. It can also be proven that no other functions can behave differently with respect to them. However, the logical system you get when eta-reduction is added to the proof theory is importantly different from the one where only beta-reduction is permitted.
 
-MORE on extensionality
-
-If we answer Q2 by permitting reduction inside abstracts, and we also permit eta-reduction, then where neither `y` nor `z` occur in M, this:
+If we answer Q2 by permitting reduction inside abstracts, and we also permit eta-reduction, then where none of <code>y<sub>1</sub>, ..., y<sub>n</sub> occur free in M, this:
 
-       \x y z. M y z
+<pre><code>\x y<sub>1</sub>... y<sub>n</sub>. M y<sub>1</sub>... y<sub>n</sub></code></pre>
 
-will eta-reduce by two steps to:
+will eta-reduce by n steps to:
 
        \x. M
 
+The logical system you get when eta-reduction is added to the proof system has the following property:
+
+>      if `M`, `N` are normal forms with no free variables, then <code>M &equiv; N</code> iff `M` and `N` behave the same with respect to every possible sequence of arguments.
+
+That is, when `M` and `N` are (closed normal forms that are) syntactically distinct, there will always be some sequences of arguments <code>L<sub>1</sub>, ..., L<sub>n</sub></code> such that:
+
+<pre><code>M L<sub>1</sub> ... L<sub>n</sub> x y ~~> x
+N L<sub>1</sub> ... L<sub>n</sub> x y ~~> y
+</code></pre>
+
+That is, closed normal forms that are not just beta-reduced but also fully eta-reduced, will be syntactically different iff they yield different values for some arguments. That is, iff their extensions differ.
+
+So the proof theory with eta-reduction added is called "extensional," because its notion of normal form makes syntactic identity of closed normal forms coincide with extensional equivalence.
+
+
 The evaluation strategy which answers Q1 by saying "reduce arguments first" is known as **call-by-value**. The evaluation strategy which answers Q1 by saying "substitute arguments in unreduced" is known as **call-by-name** or **call-by-need** (the difference between these has to do with efficiency, not semantics).
 
 When one has a call-by-value strategy that also permits reduction to continue inside unapplied abstracts, that's known as "applicative order" reduction. When one has a call-by-name strategy that permits reduction inside abstracts, that's known as "normal order" reduction. Consider an expression of the form: