lambda calculus implementation

Quote:

> I would like to implement for fun an interpreter for lambda calculus terms

> (with

> different reduction strategies).

> I know at least two solutions to represent my terms (as inductive

> datatypes). The easiest one would

> be to represent variables as string, but i'd need to deal with explicit

> renaming of bound variables.

> The other solution would be to use De Bruijn indices which make subtitution

> far more easy than

> in the first solution.

Even easier substitution can be made by using higher-order abstract

syntax, e.g.:

data lam t = APP (lam, lam) | LAM (t -> lam) | VAR t

You would then represent, e.g., the term \a.\b.(b a) as

LAM (\x-> LAM (\y-> APP (VAR y, VAR x)))

You can write a term using the show function:

show t = show1 t "x"

show1 (VAR x) v = x

For the above example, this yields

"(\x.(\xx.xx x))"

The show function can be refined to avoid redundant parenthesis and to

use better names (instead of "x", "xx", "xxx", etc.).

A call-by-name reducer (to WHNF) can then be written as

cbn (APP (e1, e2)) = let (LAM f) = cbn e1 in f e2

cbn (LAM f) = LAM f

cbn (VAR x) = cbn x

A call-by-value reducer (to WHNF) can be written as

cbv (APP (e1, e2)) = let (LAM f) = cbv e1 in f (cbv e2)

cbv (LAM f) = LAM f

cbv (VAR x) = x

Torben Mogensen