From: Jim Pryor
Date: Tue, 24 Aug 2010 14:52:59 +0000 (0400)
Subject: moved programming resources to new page, expanded
XGitUrl: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=718c35b8eef781aef8bbd63e2c5ccebf6f5352dd
moved programming resources to new page, expanded
Signedoffby: Jim Pryor

diff git a/index.mdwn b/index.mdwn
index eb61fb70..79538456 100644
 a/index.mdwn
+++ b/index.mdwn
@@ 171,11 +171,6 @@ This covers some of the same introductory ground as The Little Schemer, but
this time in ML. The dialect of ML used is SML, not OCaml, but there are only
superficial syntactic differences between these languages.
# Other resources #

* [Barker's Lambda Tutorial](http://homepages.nyu.edu/~cb125/Lambda): tutorial with embedded Javascript code that enables a user to type a lambda form into a web browser page and click to execute (reduce) it.
* [Penn Lambda Calculator](http://www.ling.upenn.edu/lambda/): requires installing Java, but provides a number of tools for evaluating lambda expressions and other linguistic forms.

##[[Schedule of Topics]]##
##[[Lecture Notes]]##
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/#lambdacalc) in Scheme. Here's how he describes it:
+
+ A practical Lambdacalculator in Scheme
+
+ The code below implements a normalorder interpreter for the untyped lambdacalculus. The interpret permits "shortcuts" of terms. The shortcuts are not first class and do not alter the semantics of the lambdacalculus. 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 alpharenaming, etc.
+
+ This calculator implements a normalorder evaluator for the untyped lambdacalculus 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 lambdacalculus remarkably more convenient.
+
+ Besides terms to reduce, this lambdacalculator accepts a set of commands, which add even more convenience. Commands define new shortcuts, activate tracing of all reductions, compare terms modulo alphaconversion, print all defined shortcuts and evaluation flags, etc. Terms to evaluate and commands are entered at a readevalprintloop (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 .
+
+
+4. Oleg also provides another lambda interpreter [written in
+Haskell](http://okmij.org/ftp/Computation/lambdacalc.html#lambdacalculatorhaskell).
+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 k = < y>>
+ let id = < x>>
+ let add = < n $succ$ m>>
+ let pred = < 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 ##
+
+