X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=week2.mdwn;h=a8e3ca4e6968aa393b6de9e0a7a8c1d74724d7be;hp=ce2df76df252e30b20e142599925ed771e6097a2;hb=b81bb9f115db430bc26377fe825aeab2a7d270a2;hpb=6b354c56b73998dfcdd5be0f148ad24f1b9fed1d
diff --git a/week2.mdwn b/week2.mdwn
index ce2df76d..a8e3ca4e 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, The Syntactic Processs). 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 ≡ `\xy.yx`, B ≡ `\fxy.f(xy)`,
and our friend S. Steedman used Smullyan's fanciful bird
names for the combinators, Thrush, Bluebird, and Starling.
@@ -318,17 +318,19 @@ 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 (~~>β
) or whether both beta- and eta-reduction is allowed (~~>βη
).
+
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 M ≡ N
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 L1, ..., Ln
such that:
+This implies that, when `M` and `N` are (closed normal forms that are) syntactically distinct, there will always be some sequences of arguments L1, ..., Ln
such that:
M L1 ... Ln x y ~~> x
N L1 ... Ln x y ~~> y
-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 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.
@@ -430,6 +432,7 @@ But is there any method for doing this in general---for telling, of any given co
* [Scooping the Loop Snooper](http://www.cl.cam.ac.uk/teaching/0910/CompTheory/scooping.pdf), a proof of the undecidability of the halting problem in the style of Dr Seuss by Geoffrey K. Pullum
+Interestingly, Church also set up an association between the lambda calculus and first-order predicate logic, such that, for arbitrary lambda formulas `M` and `N`, some formula would be provable in predicate logic iff `M` and `N` were convertible. So since the right-hand side is not decidable, questions of provability in first-order predicate logic must not be decidable either. This was the first proof of the undecidability of first-order predicate logic.
##[[Lists and Numbers]]##