X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=week2.mdwn;h=bd86cbbf3a0cadaadc2f259b3602b5c04ff878c9;hp=ce2df76df252e30b20e142599925ed771e6097a2;hb=c595c61a3fc33a2343e3ef906a382652c655d518;hpb=6b354c56b73998dfcdd5be0f148ad24f1b9fed1d

diff --git a/week2.mdwn b/week2.mdwn
index ce2df76d..bd86cbbf 100644
--- a/week2.mdwn
+++ b/week2.mdwn
@@ -241,7 +241,7 @@ in two books in the 1990's.
 
 A final linguistic application: Steedman's Combinatory Categorial Grammar, where the "Combinatory" is 
 from combinatory logic (see especially his 2000 book, <cite>The Syntactic Processs</cite>).  Steedman attempts to build
-a syntax/semantics interface using a small number of combinators, including T = `\xy.yx`, B = `\fxy.f(xy)`,
+a syntax/semantics interface using a small number of combinators, including T &equiv; `\xy.yx`, B &equiv; `\fxy.f(xy)`,
 and our friend S.  Steedman used Smullyan's fanciful bird 
 names for the combinators, Thrush, Bluebird, and Starling.
 
@@ -318,6 +318,8 @@ will eta-reduce by n steps to:
 
 	\x. M
 
+When we add eta-reduction to our proof system, we end up reconstruing the meaning of `~~>` and `<~~>` and "normal form", all in terms that permit eta-reduction as well. Sometimes these expressions will be annotated to indicate whether only beta-reduction is allowed (<code>~~><sub>&beta;</sub></code>) or whether both beta- and eta-reduction is allowed (<code>~~><sub>&beta;&eta;</sub></code>).
+
 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.
@@ -328,7 +330,7 @@ That is, when `M` and `N` are (closed normal forms that are) syntactically disti
 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.
+That is, closed beta-plus-eta-normal forms 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.