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.
The syntax rules are, in addition to all the rules from PP1:
t ::= x λx. t t t let x = t1 in t2 fix t
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
λ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)
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)
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_termnever to return.
If a term gets stuck according to the semantics, then
eval_termshould raise an exception with an appropriate error message.
If the result value is an abstraction, it’s okay for
eval_termto 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 t1 ⇓ λx. t12 t2 ⇓ v2 [x↦v2]t12 ⇓ v ——————————————————————————————————————— (B-App) t1 t2 ⇓ v
Implement 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. t1) = λy. t1 if y = x λy. [x↦s]t1 if y ≠ x and y ∉ FV(s) [x↦s](t1 t2) = [x↦s]t1 [x↦s]t2
As discussed on that page, this definition is missing a case, for
y ≠ xand
y ∈ FV(s). But in HW3, you showed that if
tis closed, then this missing case will never be needed. So, one way to proceed is: Before evaluation, check whether
thas any free variables, and print an error message if so. Otherwise, evaluate
tusing 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) ρ ⊢ t1 ⇓ [ρ'](λx. t12) ρ ⊢ t2 ⇓ v2 ρ', x↦v2 ⊢ t12 ⇓ v —————————————————————————————————————————————————————————— B-App ρ ⊢ t1 t2 ⇓ v
When 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
In this part, you’ll extend the interpreter to handle
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.
You can implement them as syntactic sugar:
T⟦let x = t1 in t2⟧ = (λx. T⟦t2⟧) T⟦t1⟧ T⟦fix t⟧ = λf. (λx. f (λv. x x v)) (λx. f (λv. x x v)) T⟦t⟧
The rest of the equations defining
Write a function called
desugar_termthat takes an argument
T⟦t⟧. It should be called before
Or you can write new evaluation rules for them (here, using big-step evaluation with substitution):
t1 ⇓ v1 [x↦v1]t2 ⇓ v2 ―――――――――――――――――――――――― (B-Let) let x = t1 in t2 ⇓ v2 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
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