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 = 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   [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 [x↦s](λ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   ρ', 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 <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   [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.

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