week2: ~~>_eta

[lambda.git] / week2.mdwn

diff --git a/week2.mdwn b/week2.mdwn
index ce2df76..eedc6de 100644 (file)
--- 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.