# Project 2: Untyped lambda-calculus

- Due: 02/22 at 11:55pm
- Points: 30

In this project, we’ll extend the arithmetic expression interpreter from PP1 into an untyped lambda calculus interpreter.

```
> let f = λx. succ (succ x) in f (f 0)
succ (succ (succ (succ 0)))
```

## 0. Getting started

The repository contains the following files (among others):

```
solution/
lam.darwin Reference implementation (MacOS)
lam.linux Reference implementation (Linux)
test/
test.sh Test script
lam.input Test cases
submit/ Please place your code here
```

Try running the reference implementation and have a look at the test cases to see how it works.

## 1. Syntax

The syntax rules are, in addition to all the rules from PP1:

```
t ::= x
λx. t
t t
let x = t
```_{1} in t_{2}
fix t

where `x`

can be any string that:

does not contain whitespace

does not contain any of the symbols

`( ) λ \ . = : ->`

is not any of the reserved words

`0 succ pred iszero true false if then else let in fix`

The term `λx. x x`

would be represented as

```
["lambda" "x" ["app", ["var", "x"], ["var", "x"]]] (Python)
(lambda "x" (app (var "x") (var "x"))) (Scheme)
Lambda ("x", App (Var "x", Var "x")) (OCaml)
```

The term `let g = fix f in g 0`

would be

```
["let", "g", ["fix", ["var", "f"]], ["app", ["var", "g"], "zero"]] (Python)
(let "g" (fix (var "f")) (app (var "g") zero)) (Scheme)
Let ("g", Fix (Var "f"), App (Var "g", Zero)) (OCaml)
```

## 2. Core

Write a function called `eval_term`

(or something similar) that takes a term and returns its value (if any). The following requirements should be met:

You may assume that the input term is closed (has no free variables), and raise an error if it is not.

The return value should agree with the call-by-value semantics for λNB in Figures 3-1, 3-2, and 5-3 (pages 34, 41, and 72).

If a term diverges according to the semantics, it’s okay for

`eval_term`

never to return.If a term gets stuck according to the semantics, then

`eval_term`

should raise an exception with an appropriate error message.If the result value is an abstraction, it’s okay for

`eval_term`

to return something that says “the result is an abstraction” instead of the abstraction itself.

Note that you don’t have to literally implement the small-step semantics; in fact, I’d recommend implementing the big-step semantics (Exercise 5.3.8), using either substitution or environments, as detailed below.

Big-step evaluation with substitution

The big-step evaluation rules are given in the solution to Exercise 5.3.8:

`————————————— (B-Abs) λx. t ⇓ λx. t t`

_{1}⇓ λx. t_{1}_{2}t_{2}⇓ v_{2}[x↦v_{2}]t_{1}_{2}⇓ v ——————————————————————————————————————— (B-App) t_{1}t_{2}⇓ vImplement the above rules, and the substitution operation as defined in TAPL at the top of page 71:

`[x↦s]y = s if y = x y if y ≠ x [x↦s](λy. t`

_{1}) = λy. t_{1}if y = x λy. [x↦s]t_{1}if y ≠ x and y ∉ FV(s) [x↦s](t_{1}t_{2}) = [x↦s]t_{1}[x↦s]t_{2}As discussed on that page, this definition is missing a case, for

`[x↦s](λy. t`

where_{1})`y ≠ x`

and`y ∈ FV(s)`

. But in HW3, you showed that if`t`

is closed, then this missing case will never be needed. So, one way to proceed is: Before evaluation, check whether`t`

has any free variables, and print an error message if so. Otherwise, evaluate`t`

using the definition of substitution above.Big-step evaluation with environments

A more efficient alternative is to use environments, as described in the notes.

`———————————— B-Var ρ ⊢ x ⇓ ρ(x) —————————————————————— B-Abs ρ ⊢ λx. t ⇓ [ρ](λx. t) ρ ⊢ t`

_{1}⇓ [ρ'](λx. t_{1}_{2}) ρ ⊢ t_{2}⇓ v_{2}ρ', x↦v_{2}⊢ t_{1}_{2}⇓ v —————————————————————————————————————————————————————————— B-App ρ ⊢ t_{1}t_{2}⇓ vWhen you print out a closure, you can choose how they should appear; the tests don’t depend on it. You can invent a textual representation of a closure, or do as most implementations do and print something opaque like

`<fun>`

.

## 3. Extensions

In this part, you’ll extend the interpreter to handle `let`

and `fix`

. The language doesn’t need them in order to be Turing-complete, but they are convenient, and in PP3, `fix`

will be necessary; if you went on to implement let-polymorphism, then `let`

would become necessary as well.

There are two ways of implementing them; you only need to do one.

Syntactic sugar

You can implement them as syntactic sugar:

`T⟦let x = t`

_{1}in t_{2}⟧ = (λx. T⟦t_{2}⟧) T⟦t_{1}⟧ T⟦fix t⟧ = λf. (λx. f (λv. x x v)) (λx. f (λv. x x v)) T⟦t⟧The rest of the equations defining

`T⟦·⟧`

are trivial.Write a function called

`desugar_term`

that takes an argument`t`

and returns`T⟦t⟧`

. It should be called before`eval_term`

.Evaluation rules

Or you can write new evaluation rules for them (here, using big-step evaluation with substitution):

`t`

_{1}⇓ v_{1}[x↦v_{1}]t_{2}⇓ v_{2}―――――――――――――――――――――――― (B-Let) let x = t_{1}in t_{2}⇓ v_{2}t ⇓ v ――――――――――――――――――――――― x ∉ FV(v) (B-Fix) fix t ⇓ λx. v (fix v) x

## 4. Read-eval-print loop

Your interpreter should be named `submit/lam`

. It should read lines from stdin, each containing exactly one term. For each term, it should desugar and evaluate it. It should write a single line to stdout, which is either the resulting value or an error message, which must begin with the string `error:`

. Run `test/test.sh lam`

to test your interpreter.

Please submit your code by pushing to your private repository and creating a tag `pp2`

. If you’re submitting a single part, tag it `pp2-2`

, `pp2-3`

, etc.

## Rubric

Part | Points |
---|---|

λ | 3 |

application | 3 |

variable binding | 6 |

`let` |
3 |

`fix` |
3 |

REPL | 6 |

Total | 30 |