From a9e5201a0fefa3602e5d3477bd2d9670aee40515 Mon Sep 17 00:00:00 2001 From: Chris Barker Date: Sat, 18 Sep 2010 09:25:25 -0400 Subject: [PATCH 1/1] Writing lecture 2 --- week2.mdwn | 35 ++++++++++++++++++++++++++++++++--- 1 file changed, 32 insertions(+), 3 deletions(-) diff --git a/week2.mdwn b/week2.mdwn index 77459bfd..ac2a7c32 100644 --- a/week2.mdwn +++ b/week2.mdwn @@ -6,6 +6,13 @@ Define T to be `(\x. x y) z`. Then T and `(\x. x y) z` are syntactically equal, 
T ≡ (\x. x y) z ≡ (\z. z y) z
+[Fussy note: the justification for counting `(\x. x y) z` as +equivalent to `(\z. z y) z` is that when a lambda binds a set of +occurrences, it doesn't matter which variable serves to carry out the +binding. Either way, the function does the same thing and means the +same thing. Look in the standard treatments for discussions of alpha +equivalence for more detail.] + This: T ~~> z y @@ -23,21 +30,43 @@ Lambda expressions that have no free variables are known as **combinators**. Her > **I** is defined to be `\x x` -> **K** is defined to be `\x y. x`, That is, it throws away its second argument. So `K x` is a constant function from any (further) argument to `x`. ("K" for "constant".) Compare K to our definition of **true**. +> **K** is defined to be `\x y. x`, That is, it throws away its + second argument. So `K x` is a constant function from any + (further) argument to `x`. ("K" for "constant".) Compare K + to our definition of **true**. > **get-first** was our function for extracting the first element of an ordered pair: `\fst snd. fst`. Compare this to **K** and **true** as well. > **get-second** was our function for extracting the second element of an ordered pair: `\fst snd. snd`. Compare this to our definition of **false**. -> **ω** is defined to be: `\x. x x` +> **ω** is defined to be: `\x. x x (\x. x x)` It's possible to build a logical system equally powerful as the lambda calculus (and readily intertranslatable with it) using just combinators, considered as atomic operations. Such a language doesn't have any variables in it: not just no free variables, but no variables at all. One can do that with a very spare set of basic combinators. These days the standard base is just three combinators: K and I from above, and also one more, **S**, which behaves the same as the lambda expression `\f g x. f x (g x)`. behaves. But it's possible to be even more minimalistic, and get by with only a single combinator. (And there are different single-combinator bases you can choose.) +There are some well-known linguistic applications of Combinatory +Logic, due to Anna Szabolcsi, Mark Steedman, and Pauline Jacobson. +Szabolcsi supposed that the meanings of certain expressions could be +insightfully expressed in the form of combinators. A couple more +combinators: + + **C** is defined to be: `\f x y. f y x` [swap arguments] + + **W** is defined to be: `\f x . f x x` [duplicate argument] + +For instance, Szabolcsi argues that reflexive pronouns are argument +duplicators. + + +![Szabolcsi's analysis of *himself* as the duplicator combinator](szabolcsi-reflexive.png) + + 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! -Here's more to read about combinatorial logic: +Here's more to read about combinatorial logic. +Surely the most entertaining exposition is Smullyan's [[!wikipedia To_Mock_a_Mockingbird]]. +Other sources include * [[!wikipedia Combinatory logic]] at Wikipedia * [Combinatory logic](http://plato.stanford.edu/entries/logic-combinatory/) at the Stanford Encyclopedia of Philosophy -- 2.11.0