3 Lambda Calculus🔗

3.1 Environments [40 Points]🔗

Substitution is an elegant way of describing semantics, but its implementation can be quite slow: repeated substitutions require scanning over the whole program, which does not scale in practice.

Consider the following grammar for a simple let language:

(define-type LetExpr

[numL (n : Number)]

[addL (l : LetExpr) (r : LetExpr)]

[varL (s : Symbol)]

[letL (var : Symbol)

(assignment : LetExpr)

(body : LetExpr)])

Implement a definitional interpreter interp-let-env of type ((Hashof Symbol Number) LetExpr -> Number) that uses an immutable hashmap to store the values of variables. This function should not use substitution. Your interpreter should behave identically to the usual semantics for the let language and respect lexical scope.

Examples:

(test (interp-let-env (hash '()) (letL 'x (numL 10)

(addL (varL 'x) (varL 'x))))

20)

(test (interp-let-env (hash (list (pair 'y 20))) (letL 'x (numL 10)

(addL (varL 'y) (varL 'x))))

30)

You may need to read the documentation on hashmaps by following the links in the above code blocks.

3.2 Compiling to the Lambda Calculus [60 Points]🔗

Recall the definition of the IteLang. In this problem, we will compile a variant of this language into the lambda calculus:

> (define-type IteLang     (numE [n : Number])     (boolE [b : Boolean])     (addE [e1 : IteLang] [e2 : IteLang])     (iteE [guard : IteLang] [thn : IteLang] [els : IteLang])     (letE [id : Symbol] [body : IteLang])     (varE [id : Symbol])     (read-numberE))

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

Each of these grammars has a new syntactic form, read-numberE and read-numberL, that read a number from the environment.

Your Church encoding should satisfy the following compiler correctness square:

For this problem you will need to manipulate Church numerals, encodings of numbers into the lambda calculus. The Church numerals are defined as follows:

• 0 is encoded as \lambda f . \lambda x . x

• 1 is encoded as \lambda f . \lambda x . (f~x)

• 2 is encoded as \lambda f . \lambda x . (f (f~x))

• 3 is encoded as \lambda f . \lambda x . (f (f (f~x)))

• ...

To warm up, see what happens when you run the following encodings by running the equivalent lambda calculus programs, either by hand or by using the lambda calculus interpreter:

• \texttt{add1}~1

• \texttt{add}~2~1

To model the environment, the interpreters we give you have an additional argument called env; it’s simply a function that, when you call it, you get back a number. You can think of this like asking the user for a number.

We have given you some helper functions in the provided starter code to make it so you can test your Church encoder:

• (church-decode-bool : (Lam -> Boolean)), which converts a Church Boolean into a Plait Boolean, or raises an error if it’s not a valid Church Boolean

• (church-decode-number : (Lam -> Number)), which converts a Church Numeral into a Plait number, or raises an error if it’s not a valid Church Numeral

• (church-numeral n), which generates the nth Church numeral for you.

Implement a function (church-encode e) of type (IteLang -> Lam) that satisfies the above compiler correctness square. We’ve given you a function test-church-encoding that tests whether or your Church encoder is correct for a particular term, with the constant environment that always returns 0. You should not assume that we will test your programs under the same environment.

Here are some example tests:

(test-church-encoding (numE 5))

(test-church-encoding (addE (numE 2) (numE 3)))

(test-church-encoding (letE 'x (numE 5) (varE 'x)))

(test-church-encoding

(letE 'x (numE 2)

(addE (varE 'x) (numE 3))))

You can assume that we will only give you valid IteLang programs, so you don’t need to worry about what happens if you try to perform illegal operations like adding Booleans and numbers.