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

  lam.darwin  Reference implementation (MacOS)
  lam.linux   Reference implementation (Linux)
test/     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 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.

  1. 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   [xv2]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:

           [xs]y = s                 if y = x
                     y                 if y ≠ x
    [xs](λy. t1) = λy. t1            if y = x
                     λy. [xs]t1      if y ≠ x and y ∉ FV(s)
     [xs](t1 t2) = [xs]t1 [xs]t2

    As discussed on that page, this definition is missing a case, for [xs](λy. t1) where 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.

  2. 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   ρ', xv2 ⊢ 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 <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⟧

    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.

  2. Evaluation rules

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

    t1 ⇓ v1   [xv1]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/ 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.


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