cs-4400-sp26

hw3: Binding and Scope

Instructions:

• Due date: Tuesday, Feb 3 (11:59pm)
• Upload your solutions to GradeScope. You should upload a single file called code.rkt. Be sure to check that your uploaded solution is valid; you will receive 0 points if your solution does not run.
• Your programs will be evaluated on the fraction of tests that they pass. We will show you some tests, but not all tests. You should test your code thoroughly. After the submission deadline, we will reveal the hidden tests.
• Starter code: hw3-starter.rkt

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))))`
• (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.

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. This means we need two different language definitions:

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

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

Your compiler should be a Church encoding that satisfies the following compiler correctness square:

ITE prog --------------------> lambda calc prog
|          church encode           |
|                                  |
| interp-ite                       | interp-lam
|                                  |
|                                  |
\/         church decode           \/
ITE value <------------------- lambda calc value

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 \f. \x. x
• 1 is encoded as \f. \x. f x
• 2 is encoded as \f. \x. f (f x)
• 3 is encoded as \f. \x. f (f (f x))
• And so on. (In general, n is encoded \f. f^n (x).)

Using this encoding, we can define operations on Church numerals, just like how we defined operations on Church Booleans in class:

• Adding one to m: add1 = \m . \f . \x . f ((m f) x)
• Add m to n:
  • add = \m. \n. \f. \x. (m f) ((n 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:

• add1 1
• add 2 1

To model the environment, the interpreters we give you have an additional argument called env. It’s 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.

2.1 church-encode

Implement a function church-encode e of type (IteLang -> Lam) which satisfies the compiler correctness square.

We’ve given you a function (test-church-encoding e) 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.