From: Chris Date: Thu, 12 Feb 2015 02:59:07 +0000 (-0500) Subject: moved file live X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=b2419a4f0b2553436526080563affc9877b278f1;ds=sidebyside moved file live --- diff --git a/topics/_week3_combinatory_logic.mdwn b/topics/week3_combinatory_logic.mdwn similarity index 87% rename from topics/_week3_combinatory_logic.mdwn rename to topics/week3_combinatory_logic.mdwn index 5a176575..59811278 100644 --- a/topics/_week3_combinatory_logic.mdwn +++ b/topics/week3_combinatory_logic.mdwn @@ -1,6 +1,15 @@ Combinators and Combinatorial Logic =================================== +Combinatory logic is of interest here in part because it provides a +useful computational system that is equivalent to the lambda calculus, +but different from it. In addition, Combinatory Logic has a number of +applications in natural language semantics. Exploring Combinatory +Logic will involve defining a difference notion of reduction from the +one we have been using for the lambda calculus. This will provide us +with a second parallel example later when we're thinking through +such topics as evaluation strategies and recursion. + Lambda expressions that have no free variables are known as **combinators**. Here are some common ones: > **I** is defined to be `\x x` @@ -68,6 +77,8 @@ S(\xy.yx) ≡ \gx.(gx)x ≡ W +###A different set of reduction rules### + Ok, here comes a shift in thinking. Instead of defining combinators as equivalent to certain lambda terms, we can define combinators by what they do. If we have the I combinator followed by any expression X, I will take that expression as its argument and return that same expression as the result. In pictures, @@ -107,7 +118,7 @@ Logic as beta reduction and eta reduction, etc., have with respect to the lambda calculus: they are purely syntactic rules for transforming one sequence of symbols (e.g., a redex) into another (a reduced form). It's worth noting that the reduction rules for Combinatory -Logic are considerably more simple than, say, beta reduction. Since +Logic are considerably more simple than, say, beta reduction. Also, since there are no variables in Combiantory Logic, there is no need to worry about variable collision. @@ -148,7 +159,7 @@ Assume that for any lambda term T, [T] is the equivalent combinatory logic term. 1. [a] a 2. [(M N)] ([M][N]) 3. [\a.a] I - 4. [\a.M] KM assumption: a does not occur free in M + 4. [\a.M] K[M] assumption: a does not occur free in M 5. [\a.(M N)] S[\a.M][\a.N] 6. [\a\b.M] [\a[\b.M]] @@ -217,12 +228,14 @@ A philosophical connection: Quine went through a phase in which he developed a v Quine, Willard. 1960. "Variables explained away" Proceedings of the American Philosophical Society. Volume 104: 343--347. Also in W. V. Quine. 1960. Selected Logical Papers. Random House: New York. 227--235. -The reason this was important to Quine is similar to the worries that Jim was talking about -in the first class in which using non-referring expressions such as Santa Claus might commit -one to believing in non-existant things. Quine's slogan was that "to be is to be the value of a variable." -What this was supposed to mean is that if and only if an object could serve as the value of some variable, we -are committed to recognizing the existence of that object in our ontology. -Obviously, if there ARE no variables, this slogan has to be rethought. +The reason this was important to Quine is similar to the worry that +using non-referring expressions such as Santa Claus might commit one +to believing in non-existant things. Quine's slogan was that "to be +is to be the value of a variable." What this was supposed to mean is +that if and only if an object could serve as the value of some +variable, we are committed to recognizing the existence of that object +in our ontology. Obviously, if there ARE no variables, this slogan +has to be rethought. Quine did not appear to appreciate that Shoenfinkel had already invented combinatory logic, though he later wrote an introduction to Shoenfinkel's key paper reprinted in Jean @@ -232,7 +245,7 @@ Cresswell has also developed a variable-free approach of some philosophical and 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 +from combinatory logic (see especially his 2012 book, Taking Scope). 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. @@ -240,6 +253,23 @@ 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! +The combinators K and S correspond to two well-known axioms of sentential logic: + +###A connection between Combinatory Logic and logic logic### + +One way of getting a feel for the power of the SK basis is to note +that the following two axioms + + AK: A --> (B --> A) + AS: (A --> (B --> C)) --> ((A --> B) --> (A --> C)) + +when combined with modus ponens (from `A` and `A --> B`, conclude `B`) +are complete for the implicational fragment of intuitionistic logic. +The way we'll favor for viewing the relationship between these axioms +and the S and K combinators is that the axioms correspond to type +schemas for the combinators. Thsi will become more clear once we have +a theory of types in view. + Here's more to read about combinatorial logic. Surely the most entertaining exposition is Smullyan's [[!wikipedia To_Mock_a_Mockingbird]]. Other sources include