XGitUrl: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=using_the_programming_languages.mdwn;h=2097dea239a5069e01e38cba1f749314dd013e18;hp=9faaad4f34de5b53d4778cb8e6ea003b2a305f04;hb=00b6e7be50487a25a1d96ec239f04271f0be53a6;hpb=d773dfc0b5aab6bc79f9a6990af79aed988648f4
diff git a/using_the_programming_languages.mdwn b/using_the_programming_languages.mdwn
index 9faaad4f..2097dea2 100644
 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/#lambdacalc) in Scheme. Here's how he describes it:
+3. Oleg Kiselyov has a [richer lambda interpreter](http://okmij.org/ftp/Scheme/#lambdacalc) in Scheme. Here's how he describes it
+(I've made some trivial changes to the text):
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
@@ 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 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 %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.
@@ 110,16 +110,35 @@ 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$ >>;;
+ 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.
+
+ * What's written betwen the `<<` and `>>` is parsed as 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 when fully reduced or "normalized" 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 value of 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 addon bundle. For the most part it doesn't matter if other expressions are placed flush beside the `<<` and `>>`: you can do either `<< fun x > x >>` or `<x>>`. But the `$`s *must* be separated from the `<<` and `>>` brackets with spaces or `(` `)`s. It's probably easiest to just always surround the `<<` and `>>` with spaces.
 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