week2: expand on eta and extensionality

Signed-off-by: Jim Pryor <profjim@jimpryor.net>

diff --git a/week2.mdwn b/week2.mdwn
index c4d573d..ebc5959 100644 (file)
--- a/week2.mdwn
+++ b/week2.mdwn
@@ -320,7 +320,20 @@ 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.
 
 
 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
+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.
+

 
 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 neither `y` nor `z` occur in M, this: