We assume here that you've already gotten [Schema and OCaml installed on your computer](/how_to_get_the_programming_languages_running_on_your_computer/).
## Programming in the pure untyped lambda calculus ##
There are several ways to do this, and we're still thinking out loud in this space about which method we should recommend you use.
1. To get started, Chris has a nice [Lambda Tutorial](http://homepages.nyu.edu/~cb125/Lambda)
webpage introducing the untyped lambda calculus. This page has embedded Javascript
code that enables you to type lambda expressions into your web browser page
and click a button to "execute" (that is, reduce or normalize) it.
To do more than a few simple exercises, though, you'll need something more complex.
2. One option is to use a short Scheme macro, like the one [linked at the bottom of Chris' webpage](http://homepages.nyu.edu/~cb125/Lambda/lambda.scm).
You can use this by loading into a Scheme interpreter (EXPLAIN HOW...) and then (STEP BY STEP...).
Here's Chris' explanation of the macro:
(define (reduce f) ; 1
((lambda (value) (if (equal? value f) f (reduce value))) ; 2
(let r ((f f) (g ())) ; 3
(cond ((not (pair? f)) ; 4
(if (null? g) f (if (eq? f (car g)) (cadr g) (r f (caddr g))))) ; 5
((and (pair? (car f)) (= 2 (length f)) (eq? 'lambda (caar f))) ; 6
(r (caddar f) (list (cadar f) (r (cadr f) g) g))) ; 7
((and (not (null? g)) (= 3 (length f)) (eq? 'lambda (car f))) ; 8
(cons 'lambda (r (cdr f) (list (cadr f) (delay (cadr f)) g)))) ; 9
(else (map (lambda (x) (r x g)) f)))))) ;10
If you have a Scheme interpreter, you can call the function like this:
(reduce '(((lambda x (lambda y (x y))) 2) 3))
;Value: (2 3)
(reduce '((lambda x (lambda y (x y))) 2))
;Value: (lambda #[promise 2] (2 #[promise 2]))
Comments: f is the form to be evaluated, and g is the local assignment
function; g has the structure (variable value g2), where g2 contains the rest
of the assignments. The named let function r executes one pass through a form.
The arguments to r are a form f, and an assignment function g. Line 2: continue
to process the form until there are no more conversions left. Line 4
(substitution): If f is atomic [or if it is a promise], check to see if matches
any variable in g and if so replace it with the new value. Line 6 (beta
reduction): if f has the form ((lambda variable body) argument), it is a lambda
form being applied to an argument, so perform lambda conversion. Remember to
evaluate the argument too! Line 8 (alpha reduction): if f has the form (lambda
variable body), replace the variable and its free occurences in the body with a
unique object to prevent accidental variable collision. [In this implementation
a unique object is constructed by building a promise. Note that the identity of
the original variable can be recovered if you ever care by forcing the
promise.] Line 10: recurse down the subparts of f.
3. Oleg Kiselyov has a [richer lambda interpreter](http://okmij.org/ftp/Scheme/#lambda-calc) in Scheme. Here's how he describes it
(I've made some trivial changes to the text):
A practical Lambda-calculator in Scheme
The code below implements a normal-order interpreter for the untyped
lambda-calculus. The interpret permits "shortcuts" of terms. The shortcuts are
not first class and do not alter the semantics of the lambda-calculus. Yet they
make complex terms easier to define and apply.
The code also includes a few convenience tools: tracing of all reduction,
comparing two terms modulo alpha-renaming, etc.
This calculator implements a normal-order evaluator for the untyped
lambda-calculus with shortcuts. Shortcuts are distinguished constants that
represent terms. An association between a shortcut symbol and a term must be
declared before any term that contains the shortcut could be evaluated. The
declaration of a shortcut does not cause the corresponding term to be
evaluated. Therefore shortcut's term may contain other shortcuts -- or even yet
to be defined ones. Shortcuts make programming in lambda-calculus remarkably
more convenient.
Besides terms to reduce, this lambda-calculator accepts a set of commands,
which add even more convenience. Commands define new shortcuts, activate
tracing of all reductions, compare terms modulo alpha-conversion, print all
defined shortcuts and evaluation flags, etc. Terms to evaluate and commands are
entered at a read-eval-print-loop (REPL) "prompt" -- or "included" from a file
by a special command.
Examples
First we define a few shortcuts:
(X Define %c0 (L s (L z z))) ; Church numeral 0
(X Define %succ (L n (L s (L z (s (n z z)))))) ; Successor
(X Define* %c1 (%succ %c0))
(X Define* %c2 (%succ %c1))
(X Define %add (L m (L n (L s (L z (m s (n s z))))))) ; Add two numerals
(%add %c1 %c2)
REPL reduces the term and prints the answer: (L f (L x (f (f (f x))))).
(X equal? (%succ %c0) %c1)
(X equal?* (%succ %c0) %c1)
The REPL executes the above commands and prints the answer: #f and #t,
correspondingly. The second command reduces the terms before comparing them.
See also .
4. Oleg also provides another lambda interpreter [written in
Haskell](http://okmij.org/ftp/Computation/lambda-calc.html#lambda-calculator-haskell).
Jim converted this to OCaml and bundled it with a syntax extension that makes
it easier to write pure untyped lambda expressions in OCaml. You don't have to
know much OCaml yet to use it. Using it looks like this:
let zero = < z>>
let succ = < s (n s z)>>
let one = << $succ$ $zero$ >>
let two = << $succ$ $one$ >>
let add = < n $succ$ m>>
(* or *)
let add = < fun s z -> m s (n s z)>>
church_to_int << $add$ $one$ $two$ >>;;
- : int = 3
5. To play around with a **typed lambda calculus**, which we'll look at later
in the course, have a look at the [Penn Lambda Calculator](http://www.ling.upenn.edu/lambda/).
This requires installing Java, but provides a number of tools for evaluating
lambda expressions and other linguistic forms. (Mac users will most likely
already have Java installed.)
## Reading about Scheme ##
[R5RS Scheme](http://people.csail.mit.edu/jaffer/r5rs_toc.html)
## Reading about OCaml ##