# 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