X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=week2.mdwn;h=2a17a8b0dde21036c19fb2676be73f2792c79d8c;hp=13fd1c891e0ba552b8d7cc96433d4e0519064019;hb=b7d91eac8927d07994f585d0c03a1fe1f729f6c5;hpb=1382359a2b828f0172b4bbaf3828100e0e47db3e diff --git a/week2.mdwn b/week2.mdwn index 13fd1c89..2a17a8b0 100644 --- a/week2.mdwn +++ b/week2.mdwn @@ -1,5 +1,54 @@ [[!toc]] +Substitution and Alpha-Conversion +================================= + +Intuitively, (a) and (b) express the application of the same function to the argument `y`: + +
(\x. \z. z x) y
+(\x. \y. y x) y
+(\z. (\z. z z) y
+λ ... `___` ...
+^ |
+|`______`|
+
+
+Here there are no bound variables, but there are *bound positions*. We can regard formula like (a) and (b) as just helpfully readable ways to designate these abstract structures.
+
+A version of this last approach is known as **de Bruijn notation** for the lambda calculus.
+
+It doesn't matter which of these approaches one takes; the logical properties of the systems are exactly the same. It just affects the particulars of how one states the rules for substitution, and so on. And whether one talks about expressions being literally "syntactically identical," or whether one instead counts them as "equivalent modulu alpha-conversion."
+
+(In a bit, we'll discuss other systems that lack variables. Those systems will not just lack variables in the sense that de Bruijn notation does; they will furthermore lack any notion of a bound position.)
+
+
Syntactic equality, reduction, convertibility
=============================================
@@ -154,6 +203,12 @@ The orginal lambda term lifts its first argument (think of it as reversing the o
Viola: the combinator takes any X and Y as arguments, and returns Y applied to X.
+One very nice property of combinatory logic is that there is no need to worry about alphabetic variance, or
+variable collision---since there are no (bound) variables, there is no possibility of accidental variable capture,
+and so reduction can be performed without any fear of variable collision. We haven't mentioned the intricacies of
+alpha equivalence or safe variable substitution, but they are in fact quite intricate. (The best way to gain
+an appreciation of that intricacy is to write a program that performs lambda reduction.)
+
Back to linguistic applications: one consequence of the equivalence between the lambda calculus and combinatory
logic is that anything that can be done by binding variables can just as well be done with combinators.
This has given rise to a style of semantic analysis called Variable Free Semantics (in addition to
@@ -184,7 +239,14 @@ van Heijenoort (ed) 1967 *From Frege to Goedel,
Cresswell has also developed a variable-free approach of some philosophical and linguistic interest
in two books in the 1990's.
-These systems are Turing complete. In other words: every computation we know how to describe can be represented in a logical system consisting of only a single primitive operation!
+A final linguistic application: Steedman's Combinatory Categorial Grammar, where the "Combinatory" is
+from combinatory logic (see especially his 2000 book, *The Syntactic Process*). Steedman attempts to build
+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.
+
+Many of these combinatory logics, in particular, the SKI system,
+are Turing complete. In other words: every computation we know how to describe can be represented in a logical system consisting of only a single primitive operation!
Here's more to read about combinatorial logic.
Surely the most entertaining exposition is Smullyan's [[!wikipedia To_Mock_a_Mockingbird]].