3 The Lambda Calculus & Compilation
Today we will see a phase transition in programming language design. So far, the languages we’ve seen – LetLang, IteLang, CalcLang – are tiny, and seem unrepresentative of the kinds of languages that we would actually prgram in. Today, we will see the smallest interesting programming language, the lambda calculus. We will see that the lambda calculus is a Turing-complete language: it is capable – more or less – of representing all of the programs that your computer can run. Despite this expressive power, we will see that the lambda calculus has a very small number of rules that determine its behavior. This combination of expressivity and simplicity has made it the historical and intellectual starting point for much of programming languages.
3.1 Syntax of the Lambda Calculus
identifiers,
lambda abstractions (also called "functions"), and
lambda application (also called "function calls").
Notice what this language doesn’t have: no numbers, no Booleans, no conditionals. Only functions and function calls. Essentially, the lambda calculus is the untyped fragment of Plait restricted to only these three syntactic forms.
Let’s see some examples. First, the identity function:
> (lambda (x) x) - ('_a -> '_a)
#<procedure>
Syntactically, a lambda expression has two parts: an argument, which is a variable name; and a body, which is an expression. In the lambda calculus, functions are the only kind of values. We can of course call a function:
> ((lambda (x) x) (lambda (y) (lambda (z) y))) - ('_a -> ('_b -> '_a))
#<procedure>
Syntactically, an application has two parts: a callee, the function being called, and a argument, which is the argument being being passed to the callee. In the above, (lambda (x) x) is the callee and (lambda (y) (lambda (z) y)) is the argument.
That’s it: that’s the entire language. Just functions and function calls. So, let’s design an abstract syntax datastructure for representing programs like these:
> (define-type Lam [identE (id : Symbol)] [lamE (arg : Symbol) (body : Lam)] [appE (e1 : Lam) (e2 : Lam)])
3.1.1 Surface Syntax
In this class we will be writing a lot of lambda calculus terms, so it’s important that we have good and concise notation for representing them. We will use the following surface syntax grammar:
‹expr›
::=
( ‹expr› )
|
λ ‹ident› . ‹expr›
|
‹expr› ‹expr›
|
‹ident›
The parenthesis in this surface syntax act like in infix notation: they disambiguate binding order. The surface syntax λ ‹ident› . ‹expr› denotes a lambda abstraction with argument ‹ident› and body ‹expr›; the . separates the two. The surface syntax ‹expr› ‹expr› denotes an application. Note that this application rule is ambiguous, similar to addition in infix grammars, so we specify a left-associate binding order, i.e. x~y~z is equivalent surface syntax to (x~y)~z. This is likely an unfamiliar grammar to you, so let’s see some examples by seeing some surface syntax and corresponding abstract syntax datastructures:
Surface syntax |
| Abstract syntax datastructure |
x |
| (identE 'x) |
\lambda x . x |
| |
\lambda x . \lambda y . x |
| |
x~y |
| |
(x~y)~z |
| |
x~y~z |
| |
(\lambda x . x)~(\lambda y . y) |
| |
(\lambda x . x~x)~(\lambda y . y) |
| (appE (lamE 'x (appE (identE 'x) (identE 'x))) (lamE 'y (identE 'y))) |
\lambda x . (x~(\lambda y . y)) |
|
3.2 Semantics of the Lambda Calculus
This is a very critical section, read it carefully. Several concept check questions will involve stepping and parsing \lambda-calculus terms.
Next, let’s consider how to step function calls. Similar to how we implemented LetLang, we will use substitution:
(\lambda x . x)~(\lambda y . \lambda z . y) \xrightarrow[]{\text{substitute } (\lambda y . \lambda z . y) \text{ for }x} (\lambda y . \lambda z . y)
The above step is so important that it has a very esoteric-sounding name: \beta-reduction.
A critical property of substitution is that it respects lexical scope, just like in LetLang. So, in a lambda term like (\lambda x . (\lambda x . x)), the identifier x refers to its inner-most binding. Plait works similarly, observe that the first argument 10 is ignored in the following snippet:
> (((lambda (x) (lambda (x) (+ x 10))) 10) 200) - Number
210
Let’s see some examples.
(\lambda x . (\lambda x . x)) ~ (\lambda z . z~z) \rightarrow (\lambda x . x)
Recall that, in our calculator language, if we had an expression like (+ (+ 1 2) (+ 3 4)), we would start by stepping the left argument to the outer-most addition, so this would step to (+ 3 (+ 3 4)). A similar thing happens here: in order to call a function, might sometimes need to simplify it first. Consider the following: \Big((\lambda x . x) ~ (\lambda y . y~y) \Big) ~ (\lambda z . z) \xrightarrow{\text{Step } (\lambda x . x) ~ (\lambda y . y~y)} (\lambda y . y~y) ~ (\lambda z . z)
So, one of our rules is that to step (appE e1 e2), first fully simplify e1.
Now, let’s consider the other case: what happens if for an application like (appE (lamE 'id body) e2), we have that e2 is not yet fully simplified? Here we have a design decision: we can either substitute without simplifying e2 first, or we can first simplify e2 and then substitute it. Similar to what we did with LetLang, we will opt to first simplify e2 before substituting it; this is called the call-by-value semantics of the \lambda-calculus. So, we have the following step in the call-by-value semantics:
(\lambda x . x) ~ ((\lambda y . y)~(\lambda z . z~z)) \xrightarrow{\text{Step }((\lambda y . y)~(\lambda z . z~z))} (\lambda x . x) ~ (\lambda z . z~z)
It is sometimes the case that the body of a lambda is not fully simplified, for instance in the following lambda term: \lambda x . (x~(\lambda y . y))
There are variants of the lambda calculus that do simplify the bodies of lambdas even if they are not called. This is sometimes called full-\beta-reduction. Our language does not do this.
\lambda x . (x~(\lambda y . y)) \rightarrow \lambda x . (x~(\lambda y . y))
Lambda abstractions are values and they immediately step to themselves without performing any further simplification.
To step an application e1 e2, first fully simplify e1 to a lambda \lambda x . e, then fully simplify e2 to a value v, then perform beta reduction and substitute x with v in e.
3.3 A Definitional Interpreter
Now we are ready to implement an interpreter for the lambda calculus. First, substitution, which looks a lot like LetLang.
> (define-type Value [lamV (id : Symbol) (body : Lam)]) > (subst : (Symbol Value Lam -> Lam))
> (define (subst id assignment body) (type-case Lam body [(identE x) (if (equal? id x) (lamE (lamV-id assignment) (lamV-body assignment)) (identE x))] [(appE e1 e2) (appE (subst id assignment e1) (subst id assignment e2))] [(lamE x body) (if (equal? x id) (lamE x body) (lamE x (subst id assignment body)))]))
Note how we handle shadowing by checking to see if x and id are equal in the (lamE x body) case. Now, we can make a definitional interpreter that runs lambda calculus programs using substitution:
> (interp-lam : (Lam -> Value))
> (define (interp-lam e) (type-case Lam e [(identE x) (error 'runtime "free variable")] [(lamE id body) (lamV id body)] [(appE e1 e2) (let* [(v1 (interp-lam e1)) (v2 (interp-lam e2)) (id (lamV-id v1)) (body (lamV-body v1)) (subst-body (subst id v2 body))] (interp-lam subst-body))]))
> (test (interp-lam (lamE 'x (identE 'x))) (lamV 'x (identE 'x)))
- Void
good (interp-lam (lamE (quote x) (identE (quote x)))) at line 11
expected: (lamV 'x (identE 'x))
given: (lamV 'x (identE 'x))
> (test (interp-lam (lamE 'x (appE (identE 'x) (lamE 'y (identE 'y))))) (lamV 'x (appE (identE 'x) (lamE 'y (identE 'y)))))
- Void
good (interp-lam (lamE (quote x) (appE (identE (quote x)) (lamE (quote y) (identE (quote y)))))) at line 12
expected: (lamV 'x (appE (identE 'x) (lamE 'y (identE 'y))))
given: (lamV 'x (appE (identE 'x) (lamE 'y (identE 'y))))
3.4 Programming in the Lambda Calculus
I told you in the beginning that the lambda calculus is a very expressive language. It might not seem that way since it consists of so little syntax. So, let’s see how we might encode a richer feature into the lambda calculus. In future lectures, we will see even more examples of how to program effectively in the lambda calculus, including how to compile many expressive high-level language features into it.
3.4.1 Multiple arguments
Plait lets us write functions with multiple arguments like this:
> (define (callx x y) (x y))
How do we do this in the lambda calculus? Well, it’s easy enough: we can write a function that returns another function, like so:
(\lambda x . (\lambda y . x~y))
The process of transforming a function that takes multiple arguments into a sequence of functions that each takes a single argument is called currying. In some languages, like OCaml and Haskell, all functions are automatically "curried" by default.
3.4.2 Non-termination
One thing the lambda calculus seems to be lacking is loops or any form of recursion. Let’s conclude by seeing that, even though the lambda calculus does not have an explicit looping construct, it is nonetheless possible to make lambda calculus programs that run forever!
Let’s make a program that runs forever. First, let’s define a lambda calculus term \omega that takes a function as an argument and calls that function with itself as an argument:
\omega ::= \lambda x . x~x
Clearly, \omega doesn’t run forever: running it immediately terminates because lambdas are values. The magic happens when we call \omega with itself as an argument. Look what happens when we perform one step of \beta-reduction on this:
(\lambda x . x~x) ~ (\lambda x . x~x) \xrightarrow{\text{Substitute }x \text{ for }(\lambda x . x~x)} (\lambda x . x~x) ~ (\lambda x . x~x)
"I am the Alpha and the Omega, the Beginning and the End, the First and the Last." King James Bible. Revelation 22:13.
Observe: The program did not change after one step of computation! So, this program will run forever, repeatedly stepping to itself. This program is usually called \Omega: it is the while (true) {} of the lambda calculus.
Next, we begin to understand how the lambda calculus can be a fully-featured programming language. To see this, we will use it as a compilation target: we will compile richer, higher-level languages into the lambda calculus.
3.5 Compiling To the Lambda Calculus
Let’s consider a tiny simple calculator language with Booleans, along with a definitional interpreter for it:
> (define-type BoolCalc (trueE) (falseE) (notE [e : BoolCalc]) (andE [e1 : BoolCalc] [e2 : BoolCalc])) > (interp-bool : (BoolCalc -> Boolean))
> (define (interp-bool e) (type-case BoolCalc e [(trueE) #t] [(falseE) #f] [(notE e) (not (interp-bool e))] [(andE e1 e2) (and (interp-bool e1) (interp-bool e2))]))
The notion of compiler correctness we focus on here is sometimes called whole-program compiler correctness. There are many notions of compiler correctness in the literature; if you’re curious, see (??? ???).
Our goal now is to run BoolCalc programs using our lambda calculus interpreter. We will need two functions to do this:
A function encode of type (BoolCalc -> Lam) that compiles BoolCalc programs into "equivalent" lambda calculus programs;
A function decode of type (LamValue -> Boolean) that converts lambda calculus values back into Booleans, so that we can interpret the results.
Then, we will say our compiler is correct if, for any BoolCalc program e, it is the case that (interp-bool e) = (decode (interp-lam (encode e))). Sometimes, this correctness criteria is summarized as the following compiler correctness square:
BoolCalc prog --------------------> lambda calc prog |
| encode | |
| | |
| interp-bool | iterp-lam |
| | |
| | |
\/ decode \/ |
BoolCalc value <------------------- lambda calc value |
The language on the left-hand side of the compiler square is called the source language, and the language on the right-hand side of the square is called the target language.
3.5.1 Church Booleans
Let’s begin trying to implement encode:
(encode : (BoolCalc -> Lam)) (define (encode e) (type-case BoolCalc e [(trueE) ...] ...))
"In physics and mathematics, an ansatz ... is an educated guess or an additional assumption made to help solve a problem, and which may later be verified to be part of the solution by its results."
\texttt{Ltrue} = \lambda x . \lambda y . x \texttt{Lfalse} = \lambda x . \lambda y . y
First, note that Ltrue and Lfalse are functions! They can be called. The function Ltrue is a function that takes two arguments and returns the first; similarly, Lfalse takes two arguments and returns the second. We call these the first and second projections. We can define these:
> (define Ltrue (lamE 'x (lamE 'y (identE 'x)))) > (define Lfalse (lamE 'x (lamE 'y (identE 'y))))
(encode : (BoolCalc -> Lam)) (define (encode e) (type-case BoolCalc e [(trueE) Ltrue] [(falseE) Lfalse] [(notE e) ...]))
Now for the critical moment: how do we compile (notE e)? Well, first, we should probably compile e:
(encode : (BoolCalc -> Lam)) (define (encode e) (type-case BoolCalc e [(trueE) Ltrue] [(falseE) Lfalse] [(notE e) (let [(encodedE (encode e))] ...)]))
Now what? Now, we have to make use of our inductive assumption about how compile behaves: we assume that compiledE is either Ltrue or Lfalse. So, the approach is to call compiledE in a special way so that if it is Ltrue it evaluates to Lfalse, and if it’s Lfalse then it evaluates to Ltrue. Looking at the definitions of these two functions, there’s a way to do this: ((\texttt{Ltrue} ~ \texttt{Lfalse}) ~\texttt{Ltrue}) runs to \texttt{Lfalse}, and ((\texttt{Lfalse} ~ \texttt{Lfalse}) ~\texttt{Ltrue}) runs to \texttt{Ltrue}. Using this, we can fill in our compiler:
(encode : (BoolCalc -> Lam)) (define (encode e) (type-case BoolCalc e [(trueE) Ltrue] [(falseE) Lfalse] [(notE e) (let [(encodedE (encode e))] (appE (appE encodedE Lfalse) Ltrue))] [(andE e1 e2) ...]))
Finally we need to compile (andE e1 e2). Again, we make use of the fact that Ltrue and Lfalse behave like projections to get our final compile implementation (think about why this works!):
> (encode : (BoolCalc -> Lam))
> (define (encode e) (type-case BoolCalc e [(trueE) Ltrue] [(falseE) Lfalse] [(notE e) (let [(encodedE (encode e))] (appE (appE encodedE Lfalse) Ltrue))] [(andE e1 e2) (let [(encoded-e1 (encode e1)) (encoded-e2 (encode e2))] (appE (appE encoded-e1 encoded-e2) Lfalse))]))
> (define (lam->value v) (lamV (lamE-arg v) (lamE-body v)))
> (test (interp-lam (encode (trueE))) (lam->value Ltrue))
- Void
good (interp-lam (encode (trueE))) at line 22
expected: (lamV 'x (lamE 'y (identE 'x)))
given: (lamV 'x (lamE 'y (identE 'x)))
> (test (interp-lam (encode (andE (trueE) (trueE)))) (lam->value Ltrue))
- Void
good (interp-lam (encode (andE (trueE) (trueE)))) at line 23
expected: (lamV 'x (lamE 'y (identE 'x)))
given: (lamV 'x (lamE 'y (identE 'x)))
> (test (interp-lam (encode (andE (falseE) (trueE)))) (lam->value Lfalse))
- Void
good (interp-lam (encode (andE (falseE) (trueE)))) at line 24
expected: (lamV 'x (lamE 'y (identE 'y)))
given: (lamV 'x (lamE 'y (identE 'y)))
> (test (interp-lam (encode (andE (andE (trueE) (falseE)) (trueE)))) (lam->value Lfalse))
- Void
good (interp-lam (encode (andE (andE (trueE) (falseE)) (trueE)))) at line 25
expected: (lamV 'x (lamE 'y (identE 'y)))
given: (lamV 'x (lamE 'y (identE 'y)))
Suppose your friend gave you a compiler but the output was not what you expected. They swear it is correct. How would you trust their compiler was doing the right thing? Next class we will understand how to recover trust in these systems.