Merge branch 'pryor'

diff --git a/using_the_programming_languages.mdwn b/using_the_programming_languages.mdwn
index 9faaad4..bfb97ae 100644 (file)
--- a/using_the_programming_languages.mdwn
+++ b/using_the_programming_languages.mdwn
@@ -53,18 +53,19 @@ You can use this by loading into a Scheme interpreter (EXPLAIN HOW...) and then
                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:
+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
@@ -73,31 +74,30 @@ You can use this by loading into a Scheme interpreter (EXPLAIN HOW...) and then
                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 %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 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)
+                        (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.
 
@@ -113,13 +113,13 @@ 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 two = << $succ$ $one$ >>
                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
+               (* or *)
+               let add = <<fun m n -> 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