X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=using_the_programming_languages.mdwn;h=1c7aae6d8a3e852bce2986d3c997850290a12897;hp=e69de29bb2d1d6434b8b29ae775ad8c2e48c5391;hb=c73fc6712f46c9ffc3450bb6f4e12b707e6eec32;hpb=c5c1236e4deb5ef61e2f1624d82e59a881604484

diff --git a/using_the_programming_languages.mdwn b/using_the_programming_languages.mdwn
index e69de29b..1c7aae6d 100644
--- a/using_the_programming_languages.mdwn
+++ b/using_the_programming_languages.mdwn
@@ -0,0 +1,106 @@
+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:
+
+		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 f (L x x)))                     ; Church numeral 0
+			 (X Define %succ (L c (L f (L x (f (c f x))))))   ; Successor
+			 (X Define* %c1 (%succ %c0))
+			 (X Define* %c2 (%succ %c1))
+			 (X Define %add (L c (L d (L f (L x (c f (d f x))))))) ; Add two numerals
+			 (X Define %mul (L c (L d (L f (c (d f))))))      ; Multiplication
+
+		(%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 k = <<fun y _ -> y>>
+	let id = <<fun x -> x>>
+	let add = <<fun m n -> n $succ$ m>>
+	let pred = <<fun n s z -> n (fun u v -> v (u s)) ($k$ z) $id$ >>;;
+
+	church_to_int << $pred$ ($add$ $one$ ($succ$ $one$)) >>;;
+	- : int = 2
+
+
+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 ##
+
+