1 # Encoding Booleans, Tuples, Lists, and Numbers #
3 The lambda calculus can represent any computable function?
5 We need to do some work to show how to represent some of the functions
6 we've become acquainted with.
9 ## Booleans ##
11 We'll start with the `if ... then
12 ... else...` construction we saw last week:
14     if M then N else L
16 For a boolean-valued expression `M`, the displayed expression should evaluate to whatever `N` does
17 if `M` evaluates to `'true`, and to whatever `L` does if `M` evaluates to `'false.
18 In order to encode or simulate such an `if` clause in the Lambda Calculus, we
19 need to settle on a way to represent `'true` and `'false`.
21 We could simply add the constants `'true` and `'false` to the
22 language, since it does make sense to extend the Lambda Calculus by adding constants.
23 However, that would also require complicating the
24 interpretation of the language; at the very least, we would need more
25 than just beta-reduction as our engine of computation.  In the spirit
26 of computational minimalism, let's see how far we can get with the
27 "pure" lambda calculus, without any special constants.
29 Let's get rid of the parts of the `if` statement that are
30 just syntactic window-dressing.  That is, let's get rid of the
31 `if`, the `then`, and the `else`:
33     M  N  L
35 Recall that our convention is that values associate left to right, so
36 this series of terms would be evaluated as:
38     ((M N) L)
40 If this expression is supposed to have the meaning of `if M then N
41 else L`, then we need to find a value for `'true` such that when it is
42 substituted in place of `M`, the expression evaluates to `N`.  The
43 function we're looking for should take two arguments: first `N`, then `L`,
44 and it should throw away `L` and return `N`.
46 We've already seen such a function.  We called it **K**: `(\x y. x)`.
47 Let's test:
49     ((K N) L) == (((\x y. x) N) L) ~~> ((\y. N) L) ~~> N
51 Sucess! In the same spirit, `'false` could be **K I**, which reduces to `(\y x. x)`:
53     (((K I) N) L) == ((((\x y. x) (\x x)) N) L)
54                      ~~> (((\y. (\x x)) N) L)
55                      ~~> ((\x x) L)
56                      ~~> L
58 So have seen our first major encoding in the lambda calculus:
59 "true" is represented by **K**, and "false" is represented by **K I**.
60 We'll be building up a lot of representations in the weeks to come,
61 and they will all maintain the discipline that if a expression is
62 meant to be interpreted as a truth value (i.e. as a Boolean), it will
63 be equivalent to (convertible with) **K** or **K I**.
65 In class, we explained how "and" could be thought of as the function, here written
66 in Kapulet syntax:
68     lambda p q. if p then q else false
70 or:
72     lambda p q. if p then q else q
74 Given that we know how to express `if ... then ...` in terms of our encoded Booleans,
75 we can represent this easily in the Lambda Calculus as either:
77     \p q. p q (\y x. x)
79 or:
81     \p q. p q p
83 Typically there will be more than one way to encode a given function into the Lambda Calculus, even holding fixed
84 all your other decisions about how to encode other functions. In this case, we can use either representation
85 because we're assuming that the `p` only gets bound to arguments that are either `\x y. x` or `\y x. x`. We don't make any
86 promises about what will happen if our encodings are abused, that is, supplied with arguments they weren't designed to accept.
87 If `p` is bound to `\x y. x`, then the result of both of the above displayed expressions will be whatever `q` is bound to.
88 If on the other hand, `p` is bound to `\y x. x`, then the two dislayed expressions will be the same. Despite this, they are
89 two different lambda expressions, and are not convertible. It's only within the frame of our assumptions about the restricted
90 arguments we're thinking of supplying them that they behave exactly the same.
92 You can try out these expressions in the [[lambda evaluator|code/lambda evaluator]]:
94     let true = \x y. x in
95     let false = \y x. x in
96     let and = \p q. p q p in
97     and true false
99 will reduce or "normalize" to `\y x. x`, or false, just as you'd predict. The `let true =` stuff isn't officially part of the Lambda Calculus language. It's just a convenient shorthand that lets you use the lambda evaluator more efficiently. Behind the scenes, the displayed expression above gets translated to:
101     (\true.
102       (\false.
103         (\and. and true false)))
104         (\x y. x) ; this gets bound to variable "true"
105         (\y x. x) ; this gets bound to variable "false"
106         (\p q. p q p) ; this gets bound to variable "and"
108 We expect you'll agree that the first is easier to write and to read.
110 In Scheme (Racket), all of these notions can be defined like this:
112     (define true  (lambda (x) (lambda (y) x)))
113     (define false (lambda (y) (lambda (x) x)))
114     (define lambda-and (lambda (p) (lambda (q) ((p q) p))))
116 and then used like this:
118     ((lambda-and true) false)
120 which will evaluate to a function, that happens to be the true function. Most Scheme interpreters like Racket will helpfully display the function with the name, if any, that was first defined to be bound to it. So we'll see the result as:
122     #<procedure:false>
124 The funny calling pattern, where we write `((lambda-and true) false)` instead of just `(lambda-and true false)`, is because that's how you have to write curried functions in Scheme. Similarly for why we have `(lambda (x) (lambda (y) x))` instead of just `(lambda (x y) x)`.
126 It's possible to do the next few weeks of assignment without using a Scheme interpreter, however
127 we do recommend you [get Scheme installed on your
128 computer](/how_to_get_the_programming_languages_running_on_your_computer), and
129 [get started learning Scheme](/learning_scheme). It will help you understand the ideas better to experiment with it.
131 There's also a (slow, bare-bones, but perfectly adequate) version of Scheme available for online use at <http://tryscheme.sourceforge.net/>.
133 You should also be experimenting with this site's [[lambda evaluator|code/lambda evaluator]].
136 ## Tuples ##
138 In class, we also showed you how to encode a tuple in the Lambda Calculator. We did it with an ordered triple, but the strategy generalizes in a straightforward way. (Some authors just use this strategy to define pairs, then define triples as pairs whose second member is another pair, and so on. Yech. If you keep a firm grip on your wits, that can also be made to work, but it's extremely likely that people who code in that way are going to lose their grip at some point and get themselves in a corner where they'll regret having made that decision about how to encode triples. The strategy presented here is elegant and will help you program more hygienically even when your attention lapses.)
140 Our proposal was to define the triple `(a, b, c)` as:
142     \f. f a b c
144 To extract the first element of this, you'd write:
146     (\f. f a b c) fst_of_three
148 where `fst_of_three` is the function `\x y z. x`:
150     (\f. f a b c) (\x y z. x) ~~>
151     (\x y z. x) a b c ~~>
152     (\y z. a) b c ~~>
153     (\z. a) c ~~>
154     a
156 Here are the corresponding definitions in Scheme (Racket):
158     (define make-triple (lambda (a) (lambda (b) (lambda (c)
159                           (lambda (f) (((f a) b) c))))))
161     (define fst_of_three (lambda (x) (lambda (y) (lambda (z) x))))
162     (define snd_of_three (lambda (x) (lambda (y) (lambda (z) y))))
163     (define trd_of_three (lambda (x) (lambda (y) (lambda (z) z))))
165 Then:
167     (define p (((make-triple 10) 20) 30))
168     (p fst_of_three)  ; will evaluate to 10
169     (p snd_of_three)  ; will evaluate to 20
171 If you're puzzled by having the triple to the left and the function that "uses" or "consumes" or operates on it to the right, think about why it's being done this way: the triple is a package that will be used in coordination with some function for operating on its elements. We don't know in advance what that function will be. And it's not obvious how to make the triple be some structure that the function can "look inside" and extract the elements from. We're still trying to *figure out* how to define such structures! But what we can do is make *the triple take the function as an argument*, and return *the result of* operating on its elements with that function. In other words, the triple is a higher-order function: a function that expects another function as an argument.
173 (Consider the similarities between this definition of a triple and a generalized quantifier. This is in fact our first taste of "continuations" in the course, which are a systematic pattern for inverting the naive order of who-is-the-argument? and who-is-the-operator?)
175 If you really want to, you can disguise what's going on like this:
177     (define lifted-fst_of_three (lambda (p) (p fst_of_three)))
179 Then you could say:
181     (lifted-fst_of_three p)