X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=week2.mdwn;h=b43576f0b0e8d688eabad988701eb82e3446d4b0;hp=b944f5c4b199225e136c7b1ac4ebe0bf8a3deab0;hb=a74e125da6d29f39933f380fd6b0f91e9e4e3791;hpb=cf5b5115875d5df10051a6325c39ae362fcd1fcd

diff --git a/week2.mdwn b/week2.mdwn
index b944f5c4..b43576f0 100644
--- a/week2.mdwn
+++ b/week2.mdwn
@@ -321,6 +321,14 @@ 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.
 
+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:
+
+<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 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.
@@ -336,14 +344,6 @@ That is, closed normal forms that are not just beta-reduced but also fully eta-r
 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.
 
 
-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:
-
-	\x y z. M y z
-
-will eta-reduce by two steps to:
-
-	\x. M
-
 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: