From: Jim Date: Thu, 12 Feb 2015 17:24:19 +0000 (-0500) Subject: combinatory tweaks and formatting X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=47c3ae827c38c1edf331ffacf75cb3849aba8e49 combinatory tweaks and formatting --- diff --git a/topics/week3_combinatory_logic.mdwn b/topics/week3_combinatory_logic.mdwn index a176603c..53c2cd67 100644 --- a/topics/week3_combinatory_logic.mdwn +++ b/topics/week3_combinatory_logic.mdwn @@ -12,34 +12,33 @@ 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` +> **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`. -> **S** is defined to be `\f g x. f x (g x)`. This is a more - complicated operation, but is extremely versatile and useful - (see below): it copies its third argument and distributes it - over the first two arguments. +> **S** is defined to be `\f g x. f x (g x)`. This is a more +complicated operation, but is extremely versatile and useful +(see below): it copies its third argument and distributes it +over the first two arguments. -> **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-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`. +> **get-second** was our function for extracting the second element of an ordered pair: `\fst snd. snd`. Compare this to our definition of `false`. -> **B** is defined to be: `\f g x. f (g x)`. (So `B f g` is the composition `\x. f (g x)` of `f` and `g`.) +> **B** is defined to be: `\f g x. f (g x)`. (So `B f g` is the composition `\x. f (g x)` of `f` and `g`.) -> **C** is defined to be: `\f x y. f y x`. (So `C f` is a function like `f` except it expects its first two arguments in flipped order.) +> **C** is defined to be: `\f x y. f y x`. (So `C f` is a function like `f` except it expects its first two (curried) arguments in flipped order.) -> **W** is defined to be: `\f x . f x x`. (So `W f` accepts one argument and gives it to `f` twice. What is the meaning of `W multiply`?) - -> **ω** (that is, lower-case omega) is defined to be: `\x. x x` - - +> **W** is defined to be: `\f x . f x x`. (So `W f` accepts one argument and gives it to `f` twice. What is the meaning of `W multiply`?) +> **ω** (that is, lower-case omega) is defined to be: `\x. x x`. Sometimes this combinator is called **M**. 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: S, K, and I. -(Though we'll see shortly that the behavior of I can be exactly -simulated by a combination of S's and K's.) But it's possible to be +the standard base is just three combinators: `S`, `K`, and `I`. +(Though we'll see shortly that the behavior of `I` can be exactly +simulated by a combination of `S`'s and `K`'s.) But it's possible to be even more minimalistic, and get by with only a single combinator (see links below for details). (And there are different single-combinator -bases you can choose.) +bases you can choose.) There are some well-known linguistic applications of Combinatory Logic, due to Anna Szabolcsi, Mark Steedman, and Pauline Jacobson. @@ -96,38 +96,38 @@ 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, +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, IX ~~> X Thinking of this as a reduction rule, we can perform the following computation - II(IX) ~~> IIX ~~> IX ~~> X + II(IX) ~~> I(IX) ~~> IX ~~> X -The reduction rule for K is also straightforward: +The reduction rule for `K` is also straightforward: KXY ~~> X -That is, K throws away its second argument. The reduction rule for S can be constructed by examining +That is, `K` throws away its second argument. The reduction rule for `S` can be constructed by examining the defining lambda term:
``S ≡ \fgx.fx(gx)``