tweak ml code/instructions
[lambda.git] / using_the_programming_languages.mdwn
index 1c7aae6..1fab79f 100644 (file)
@@ -1,8 +1,86 @@
-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.
+
+1.     The easiest is to use a JavaScript interpreter that Chris wrote. Go [here](/lambda-let.html) and follow the template:
+       
+               let true = (\x (\y x)) in
+               let false = (\x (\y y)) in
+               let and = (\l (\r ((l r) false))) in
+
+               (
+
+                       ((((and false) false) yes) no)
+
+                       ((((and false) true) yes) no)
+
+                       ((((and true) false) yes) no)
+
+                       ((((and true) true) yes) no)
+
+               )
+       
+       will evaluate to:
+       
+               (no no no yes)
+
+       If you try to evaluate a non-terminating form, like `((\x (x x)) (\x (x x)))`, you'll probably have to force-quit your browser and start over. Anything you had earlier typed in the upper box will probably be lost.
+
+       Syntax: you have to fully specify parentheses and separate your lambdas. So for example, you can't write `(\x y. y)`; you have to write `(\x (\y y))`. The parser treats symbols that haven't yet been bound (as `yes` and `no` above) as free variables.
+
+
+2.     A bit more flexibility and robustness can be had by using an OCaml package. This is based on a library on [a Haskell library by Oleg Kiselyov](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) >>;;
+
+               (* now use:
+                       pp FORMULA                              to print a formula, unreduced
+                       pn FORMULA                              to print the normal form of a formula (when possible)
+                       pi FORMULA                              to print the integer which FORMULA is a Church numeral for (when possible)
+
+                       alpha_eq FORM1 FORM2    are FORM1 and FORM2 syntactically equivalent (up to alpha-conversion)?
+                                                                       this does not do reductions on the formulae
+               *)
+
+               pi << $add$ $one$ $two$ >>;;
+               - : int = 3
+
+       To install this package, here's what you need to do. I've tried to explain it in basic terms, but you do need some familiarity with your operating system: for instance, how to open a Terminal window, how to figure out what directory the Terminal is open to (use `pwd`); how to change directories (use `cd`); and so on.
+
+       INCLUDE INSTRUCTIONS
+
+       We assume here that you've already [gotten OCaml installed on your computer](/how_to_get_the_programming_languages_running_on_your_computer/).
+
+       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 add-on 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 `<<fun x->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.
+
+
+<!--
+
 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)
@@ -27,80 +105,95 @@ You can use this by loading into a Scheme interpreter (EXPLAIN HOW...) and then
                                   ((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:
+               
+               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.
+               
+               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 %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. 
+               
+               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 ##
 
+-->
+