+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 <http://okmij.org/ftp/Computation/lambda-calc.html>.
+
+
+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 = << fun s z -> z >>;;
+ let succ = << fun n s z -> s (n s z) >>;;
+ let one = << $succ$ $zero$ >>;;
+ let two = << $succ$ $one$ >>;;
+ let add = << fun m n -> n $succ$ m >>;;
+ (* or *)
+ let add = << fun m n -> fun s z -> m s (n s z) >>;;
+
+ church_to_int << $add$ $one$ $two$ >>;;
+ - : int = 3
+
+ To install Jim's OCaml bundle, DO THIS...
+
+ Some notes:
+
+ * When you're talking to the interactive OCaml program, you have to finish complete statements with a ";;". Sometimes these aren't necessary, but rather than learn the rules yet about when you can get away without them, it's easiest to just use them consistently, like a period at the end of a sentence.
+ * The expressions inside the << and >> are an expression in the pure untyped lambda calculus. The stuff outside the angle brackets is regular OCaml syntax. Here you only need to use a very small part of that syntax: "let var = some_value;;" assigns a value to a variable, and "function_foo arg1 arg2" applies the specified function to the specified arguments. "church_to_int" is a function that takes a single argument --- the lambda expression that follows it, << $add$ $one$ $two$ >> -- and, if that expression has the form of a "Church numeral", it converts it into an "int", which is OCaml's (and most language's) primitive way to represent small numbers. The line "- : int = 3" is OCaml telling you that the expression you just had it evaluate simplifies to a value whose type is "int" and which in particular is the int 3.
+ * If you call church_to_int with a lambda expression that doesn't have the form of a Church numeral, it will complain. If you call it with something that's not even a lambda expression, it will complain in a different way.
+ * The $s inside the << and >> are essentially corner quotes. If we do this: "let a = << x >>;; let b = << a >>;; let c = << $a$ >>;;" then the OCaml variable b will have as its value an (atomic) lambda expression, consisting just of the variable "a" in the untyped lambda calculus. On the other hand, the OCaml variable c will have as its value a lambda expression consisting just of the variable "*x*". That is, here the OCaml variable "a" is spliced into the lambda expression << $a$ >>.
+ * The expression that's spliced in is done so as a single syntactic unit. In other words, the lambda expression << w x y z >> is parsed via usual conventions as << (((w x) y) z) >>. Here << x y >> is not any single syntactic constituent. But if you do instead "let a = << x y >>;; let b = << w $a$ z >>", then what you get *will* have << x y >> as a constituent, and will be parsed as << ((w (x y)) z) >>.
+ * << fun x y -> something >> is equivalent to << fun x -> fun y -> something >>, which is parsed as << fun x -> (fun y -> something) >> (everything to the right of the arrow as far as possible is considered together). At the moment, this only works for up to five variables, as in << fun x1 x2 x3 x4 x5 -> something >>.
+ * The << >> and $-quotes aren't part of standard OCaml syntax, they're provided by this add-on bundle. For the most part it doesn't matter if other expressions are run together with the << and >>: you can do either << fun x -> x >> or <<fun x->x>>. But the $s *must* be separated from the << >> brackets with spaces or ( )s.
+
+
+
+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 ##
+
+