This is a simple implementation of the lambda calculus that converts
expressions in the lambda calculus into expressions in the combinator
logic.  Expressions are reduced into normal form using combinator
reduction techniques.  It's effectively a (very) simple functional
language with static binding and call-by-name semantics.  It's pretty
much Church's pure untyped lambda calculus, where the only syntactic
sugaring has been the addition of let and let rec bindings.

You need Objective Caml version 3.04 or later to build this, but it
might work with an older version.  To build the program, you just have
to do the usual './configure; make' cycle.  The result will be an
executable called 'lazy-l', which you can run.  'make all.opt' will
build a native code optimized version of the interpreter called
'lazy-l.opt', if your Objective Caml installation supports native code
compilation.

The program will optionally read a prelude file of initial definitions
from a file specified on the command line before giving you a
read-eval-print loop.  The system is very simple, and supports
*nothing* but functions for now; you need to express numbers as Church
numerals (the sample prelude file 'Prelude' included here has
definitions for arithmetic with Church numerals).

As an example of the usage of the interpreter, this binding will
calculate the fourth Fibonacci number:

let four = succ (succ two)
in
let rec fib n = cond (or (iszero n) (iszero (pred n))) one (add (fib
(pred n)) (fib (pred (pred n))))
in
fib four;

The interpreter will print the result in combinator form:

((S ((S (K S)) K)) ((S ((S (K S)) K)) ((S ((S (K S)) K)) ((S ((S (K
S)) K)) I))))

By applying f x to this,
((S ((S (K S)) K)) ((S ((S (K S)) K)) ((S ((S (K S)) K)) ((S ((S (K
S)) K)) I)))) f x;

it is readily seen to be a Church numeral, the Church numeral for 5:

(<f> (<f> (<f> (<f> (<f> <x>)))))

It is also possible to create toplevel bindings in the interpreter, by
using let or let rec without an 'in':

> let rec fib n = cond (or (iszero n) (iszero (pred n))) one (add (fib (pred n)) (fib (pred (pred n))));

Which will print the (very very long!) combinator expression this
expands to.  These bindings can then be used as though they were
builtins:

> let four = succ (succ two);
((S ((S (K S)) K)) ((S ((S (K S)) K)) ((S ((S (K S)) K)) I)))
>(fib four) f x;
(<f> (<f> (<f> (<f> (<f> <x>)))))

The Prelude file is actually just a collection of these toplevel
bindings.

These examples will only work if you've loaded the Prelude file
above.

Anonymous functions can also be generated using the lambda or \
keywords:

> let four = \f.\x.f (f (f x));
((S ((S (K S)) ((S (K K)) I))) ((S ((S (K S)) ((S (K K)) I))) ((S ((S (K S)) ((S (K K)) I))) (K I))))

which is a highly unoptimized version of the Church numeral for 4.

To be honest, there still isn't very much you can do with this code
except explore combinator logic and the lambda calculus.  I guess it
would be very useful as a teaching tool for classes in functional
programming and the theory of computation.

If you hack the code a little bit and change line 21 of the file
compiler.ml from:

print_string ((tree_to_string result) ^ "\n");

to read

print_string ((tree_to_unl result) ^ "\n");

it can also be used as a compiler from the lambda calculus into
Unlambda.  Note that because Unlambda intepreters use call-by-value
instead of call-by-name semantics, let rec will not work; it will
generate code that is correct but will cause the eager evaluating
unlambda interpreters to run in an infinite loop.  This is because
the fixed point combinators as I've defined them in the prelude only
work in call-by-name or call-by-need environments.  Beware.

Things to do:

Future versions of this interpreter will probably include
optimizations in the abstraction elimination code, the Turner set of
combinators, and some optimizations.  Right now the code is actually
quite slow.

For more information on combinator logic, the following links will be
useful:

Introduction to Functional Programming:
http://www.cl.cam.ac.uk/Teaching/Lectures/funprog-jrh-1996/

Combinators and Graph Reduction Online Course at Oberlin College:
http://www.cs.oberlin.edu/classes/dragn/labs/combinators/combinators.html

Unlambda:
http://www.eleves.ens.fr:8080/home/madore/programs/unlambda/

John's Combinatory Logic Playground:
http://www.cwi.nl/~tromp/cl/cl.html

TIGRE home page:
http://www-2.cs.cmu.edu/~koopman/tigre/index.html

Another similar lambda calculus interpreter, written in Java, that
doesn't use combinator logic:
http://drcjt.freeyellow.com/Lambda.html

Let me know what you think, and let me know of any bugs or suggestions
for improvement.

Rafael R. Sevilla, <dido@imperium.ph>

$Id: README,v 1.1.1.1 2002/04/29 07:07:48 didosevilla Exp $