5 Compilation🔗

Today 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 into it.

5.1 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))]))

Let’s load our lambda calculus back into our environment:

> (define-type Lam     [identE (id : Symbol)]     [lamE (arg : Symbol) (body : Lam)]     [appE (e1 : Lam) (e2 : Lam)])

> (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)))]))

> (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))]))

Our goal now is to run IteLang 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:

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.

5.1.1 Church Booleans🔗

Let’s begin trying to implement compile:

(compile : (BoolCalc -> Lam))

(define (compile e)

(type-case BoolCalc e

[(trueE) ...]

...))

\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))))

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 16   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 17   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 18   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 19   expected: (lamV 'x (lamE 'y (identE 'y)))   given: (lamV 'x (lamE 'y (identE 'y)))

5.2 Equality🔗

Our above compiler appears to be working perfectly, but we aren’t quite done because we haven’t finished the compiler square: we don’t yet have a decode function. Why does this matter?

Suppose someone gave you a compiler called mystery-encoder that compiled (trueE) to \lambda a . \lambda b . a. This isn’t syntactically equivalent to Ltrue, and such a compiler would fail our above test cases, since they are testing for syntactic equality. This seems undesirable: we would like compiler writers to have the freedom to use whichever variable names for encodings that they like.

Even worse, your friend has a very creative compiler called mystery-encoder2 that compiles (trueE) to \lambda a . \lambda b . ((\lambda z . z) ~ a). Is this compiler wrong? At first it may seem so, but look closely: this strange encoding behaves identically to Ltrue. So, intuitively, it seems like this compiler should also be correct.

The above discussion motivates one of the most important concepts in the lambda calculus: equality of lambda terms.

The simplest notion of equivalence is syntactic equivalence, also called \alpha-equivalence. Two terms are \alpha-equivalent if they have identical abstract syntax trees. Our above test cases check for \alpha-equivalence. But syntactic equivalence seems too strong: we would like to accept the output of mystery-encoder2 as a valid compiler, since it is intuitively behaving correctly (albeit inefficiently).

5.2.1 Observational Equivalence🔗

What does it mean for two lambda programs to be semantically equivalent? An intuitive notion of equivalence is that two lambda calculus programs should be equivalent if there is no way to tell them apart by calling them.

So, what should be our notion of observable behavior for comparing equivalence of lambda calculus programs? Well, our lambda calculus can do very few things, so we don’t have many choices about what we can or cannot observe. Let’s take a leap of faith: let’s decide that we can observe whether or not a lambda calculus program terminates.

5.2.2 Establishing Inequivalence🔗

How do we know if this is a decent notion of observation? Well, we can use it to check whether or not programs we want to be equivalent or inequivalent are consistent with this choice. Let’s start by looking at two programs we assume should not be semantically equivalent: Ltrue and Lfalse. How can we tell if these two programs are equivalent or not by calling them? We need to find a particular way to call them that exhibits different termination behavior.

To do this, let’s define a function called poison-pill that loops forever when it is called, i.e., it simply calls \Omega:

\texttt{poison-pill} = \lambda z . \Omega = \lambda z . ((\lambda x . x ~ x) ~ (\lambda x . x ~ x))

How can we use this function to distinguish Ltrue from Lfalse? Observe, the following two programs have different terminating behavior (where we’ve shorted \lambda x . x to \texttt{id}):

(\texttt{Ltrue} ~ \texttt{poison-pill} ~ \texttt{id}) ~ \texttt{id} (\texttt{Lfalse} ~ \texttt{poison-pill} ~ \texttt{id}) ~ \texttt{id}

The first one runs forever, and the second one doesn’t. Carefully think about why. So, this establihes that these two programs are observationally inequivalent.

5.3 Normal Forms🔗

We’ve seen how to establish that two programs are observationally inequivalent, but how can we establish that they’re observationally equivalent? Ideally, we would have a way of checking whether or not an arbitrary lambda term is observationally equivalent to \texttt{Ltrue} or \texttt{Lfalse}; then we could finally implement our decoder function.

The key to establishing the observational equivalence of two lambda terms is to turn the question into a search problem by successively transforming one program until it is syntactically equal to the other in a way that preserves termination behavior with each step.

For instance, suppose we want to show that e_1 = \lambda x . ((\lambda y . y)~x) is observationally equivalent to e_2 = \lambda z . z. What can we do to transform e_1 into e_2 without affecting its termination behaivor?

Well, first we can apply a beta reduction under the lambda:

Note that this step of simplification preserves termination behavior: \beta-reduction cannot turn a terminating program into a non-terminating one or vice versa.

Now, e_1{}’ is still not syntactically equal to e_2. But, it is clear that they are \alpha-equivalent to each other. So, we can apply \alpha-renaming to rename the variables in e_1{}’ to be syntactically equal to e_2; it’s clear that \alpha-renaming also preserves termination behavior.

The above suggests the following algorithm for checking whether or not two programs e_1 and e_2 are observationally equivalent, which is called the method of normal forms:

• First, fully simplify both e_1 and e_2 by applying all possible \beta-reductions. If this simplification never terminates for both, then conclude they are equivalent; if it terminates for one but not the other, conclude they are inequivalent.

• Then, try to use \alpha-renaming to relabel the fully-simplified programs so that they are syntactically equivalent. If this succeeds, they are equivalent; if it doesn’t, then they are inequivalent.

There are a few more low-level details about how precisely these two steps are implemented, which you will see in your next homework and we will discuss briefly next lecture.

Bibliography🔗