Project 2: Untyped lambda-calculus

• Due: 09/30 at 11:59pm
• 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 = t1 in t2
      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 opaque like <fun> 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.

1. Big-step evaluation with substitution

   The big-step evaluation rules are given in the solution to Exercise 5.3.8 and in the notes.

   Implement these 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 [x↦s](λy. t1) where y ≠ x and y ∈ FV(s). But it can be shown 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.

2. Big-step evaluation with environments

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

   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 <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.

1. Syntactic sugar

   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⟧
   
                  T⟦x⟧ = x
              T⟦λx. t⟧ = λx. T⟦t⟧
              T⟦t1 t2⟧ = T⟦t1⟧ T⟦t2⟧

   and so on.

   Write a function called desugar_term that takes an argument t and returns T⟦t⟧. It should be called before eval_term.

2. Evaluation rules

   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 error:. Run test/test.sh lam to test your interpreter.

Submission

To submit your code, please:

• Push your work to GitHub.
• Create a release in GitHub by clicking on “Releases” on the right-hand side, then “Create a new release” or “Draft a new release”.
• Fill in “Tag version” and “Release title” with pp2 if you’re submitting the whole assignment, pp2-1 if you’re submitting part 1, pp2-2 if you’re submitting part 2, etc.
• Finally, click “Publish Release”.

If you submit the same part more than once, we will grade the latest release for that part.

Rubric

Part	Points
λ	3
application	3
variable binding	6
let	3
fix	3
REPL	6
Total	30