Assignment 3 (Lambda Calculus)

Due Date: April 17, 2000 before class

The goal is to encode the following programming constructs in the call-by-value lambda calculus:

booleans and conditional expressions (true, false, if-then-else),
natural numbers and associated operations (increment, decrement, addition, multiplication, equality to zero),
pairs with associated operations (cons, car, cdr)
recursion

The encoding is such that given any function on the natural numbers (for example, factorial), then we can find an expression FACT in the lambda calculus such that applying FACT to the encoding of a number N evaluates to the encoding of the result. Here is an example with my solution:

Encoding of the number 3: 

  (fun (f,x) (f (f (f x))))

Encoding of the function factorial:

  ((fun (f)
     ((fun (x) (f (fun (a) ((x x) a)))) (fun (x) (f (fun (a) ((x x) a))))))
    (fun (fact)
      (fun (nn)
        ((((fun (x) (x (fun (y) (fun (x,y) y)) (fun (x,y) x))) nn)
           (fun () (fun (f,x) (f x)))
          (fun ()
            ((fun (m,n,f,x) (m (n f) x))
              nn
             (fact
               ((fun (x,f,y)
                  (x (fun (p,q) (q (p f))) ((fun (x,y) x) y) (fun (x) x)))
                 nn)))))
          ))))

Result of applying the encoding of factorial to the encoding of 3:

  (fun (f,x) (f (f (f (f (f (f x)))))))

which is the encoding of 6.

This provides empirical evidence that the lambda calculus is a Turing-complete programming language. Your actual homework is to write the encoding. The source language grammar is:

datatype prim = Inc | Dec | Add | Mult | IsZero | Cons | Car | Cdr

datatype exp = 
    Num of int
  | Bool of bool
  | Var of string
  | Prim of prim
  | If of exp * exp * exp 
  | Fun of string list * exp
  | App of exp * exp list
  | Letrec of string * exp * exp

You should write a function encode that takes an expression in the above language and produces an expression that only uses the constructs of the lambda-calculus:

  Var of string
  Fun of string list * exp
  App of exp * exp list

I will hand out a paper about encoding numerical systems in the lambda calculus.

HELP FILES

For testing your program, there are some help files in the directory help3. I have also include the beginnings of the encode.sml that uses ML structures.

Page visited

times since November 18, 1996.

sabry@cs.uoregon.edu