using_the_programming_languages.mdwn

   1 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/).
   2
   3
   4 ## Programming in the pure untyped lambda calculus ##
   5
   6 There are several ways to do this.
   7
   8 1.      The easiest is to use a JavaScript interpreter that Chris wrote. Go [here](/lambda-let.html) and follow the template:
   9
  10                 let true = (\x (\y x)) in
  11                 let false = (\x (\y y)) in
  12                 let and = (\l (\r ((l r) false))) in
  13
  14                 (
  15
  16                         ((((and false) false) yes) no)
  17
  18                         ((((and false) true) yes) no)
  19
  20                         ((((and true) false) yes) no)
  21
  22                         ((((and true) true) yes) no)
  23
  24                 )
  25
  26         will evaluate to:
  27
  28                 (no no no yes)
  29
  30         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.
  31
  32         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.
  33
  34
  35 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).
  36
  37         Jim converted this to OCaml and bundled it with a syntax extension that makes
  38 it easier to write pure untyped lambda expressions in OCaml. You don't have to
  39 know much OCaml yet to use it. Using it looks like this:
  40
  41                 let zero = << fun s z -> z >>;;
  42                 let succ = << fun n s z -> s (n s z) >>;;
  43                 let one = << $succ$ $zero$ >>;;
  44                 let two = << $succ$ $one$ >>;;
  45                 let add = << fun m n -> n $succ$ m >>;;
  46                 (* or *)
  47                 let add = << fun m n -> fun s z -> m s (n s z) >>;;
  48
  49                 church_to_int << $add$ $one$ $two$ >>;;
  50                 - : int = 3
  51
  52         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.
  53
  54         INCLUDE INSTRUCTIONS
  55
  56         Some notes:
  57
  58         *       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.
  59
  60         *       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.
  61
  62         *       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.
  63
  64         *       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$ >>`.
  65
  66         *       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) >>`.
  67
  68         *       `<< 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 >>`.
  69
  70         *       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.
  71
  72
  73 <!--
  74
  75 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.
  76
  77 1.      To get started, Chris has a nice [Lambda Tutorial](http://homepages.nyu.edu/~cb125/Lambda)
  78 webpage introducing the untyped lambda calculus. This page has embedded Javascript
  79 code that enables you to type lambda expressions into your web browser page
  80 and click a button to "execute" (that is, reduce or normalize) it.
  81
  82         To do more than a few simple exercises, though, you'll need something more complex.
  83
  84 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).
  85 You can use this by loading into a Scheme interpreter (EXPLAIN HOW...) and then (STEP BY STEP...).
  86
  87         Here's Chris' explanation of the macro:
  88
  89                 (define (reduce f)                                                          ; 1
  90                   ((lambda (value) (if (equal? value f) f (reduce value)))                  ; 2
  91                    (let r ((f f) (g ()))                                                    ; 3
  92                          (cond ((not (pair? f))                                                 ; 4
  93                                         (if (null? g) f (if (eq? f (car g)) (cadr g) (r f (caddr g))))) ; 5
  94                                    ((and (pair? (car f)) (= 2 (length f)) (eq? 'lambda (caar f)))   ; 6
  95                                         (r (caddar f) (list (cadar f) (r (cadr f) g) g)))               ; 7
  96                                    ((and (not (null? g)) (= 3 (length f)) (eq? 'lambda (car f)))    ; 8
  97                                         (cons 'lambda (r (cdr f) (list (cadr f) (delay (cadr f)) g))))  ; 9
  98                                    (else (map (lambda (x) (r x g)) f))))))                          ;10
  99
 100                 If you have a Scheme interpreter, you can call the function like this:
 101
 102                 (reduce '(((lambda x (lambda y (x y))) 2) 3))
 103                 ;Value: (2 3)
 104
 105                 (reduce '((lambda x (lambda y (x y))) 2))
 106                 ;Value: (lambda #[promise 2] (2 #[promise 2]))
 107
 108                 Comments: f is the form to be evaluated, and g is the local assignment
 109                 function; g has the structure (variable value g2), where g2 contains the rest
 110                 of the assignments. The named let function r executes one pass through a form.
 111                 The arguments to r are a form f, and an assignment function g. Line 2: continue
 112                 to process the form until there are no more conversions left. Line 4
 113                 (substitution): If f is atomic [or if it is a promise], check to see if matches
 114                 any variable in g and if so replace it with the new value. Line 6 (beta
 115                 reduction): if f has the form ((lambda variable body) argument), it is a lambda
 116                 form being applied to an argument, so perform lambda conversion. Remember to
 117                 evaluate the argument too! Line 8 (alpha reduction): if f has the form (lambda
 118                 variable body), replace the variable and its free occurences in the body with a
 119                 unique object to prevent accidental variable collision. [In this implementation
 120                 a unique object is constructed by building a promise. Note that the identity of
 121                 the original variable can be recovered if you ever care by forcing the
 122                 promise.] Line 10: recurse down the subparts of f.
 123
 124
 125 3.      Oleg Kiselyov has a [richer lambda interpreter](http://okmij.org/ftp/Scheme/#lambda-calc) in Scheme. Here's how he describes it
 126 (I've made some trivial changes to the text):
 127
 128                 A practical Lambda-calculator in Scheme
 129
 130                 The code below implements a normal-order interpreter for the untyped
 131                 lambda-calculus. The interpret permits "shortcuts" of terms. The shortcuts are
 132                 not first class and do not alter the semantics of the lambda-calculus. Yet they
 133                 make complex terms easier to define and apply.
 134
 135                 The code also includes a few convenience tools: tracing of all reduction,
 136                 comparing two terms modulo alpha-renaming, etc.
 137
 138                 This calculator implements a normal-order evaluator for the untyped
 139                 lambda-calculus with shortcuts. Shortcuts are distinguished constants that
 140                 represent terms. An association between a shortcut symbol and a term must be
 141                 declared before any term that contains the shortcut could be evaluated. The
 142                 declaration of a shortcut does not cause the corresponding term to be
 143                 evaluated. Therefore shortcut's term may contain other shortcuts -- or even yet
 144                 to be defined ones. Shortcuts make programming in lambda-calculus remarkably
 145                 more convenient.
 146
 147                 Besides terms to reduce, this lambda-calculator accepts a set of commands,
 148                 which add even more convenience. Commands define new shortcuts, activate
 149                 tracing of all reductions, compare terms modulo alpha-conversion, print all
 150                 defined shortcuts and evaluation flags, etc. Terms to evaluate and commands are
 151                 entered at a read-eval-print-loop (REPL) "prompt" -- or "included" from a file
 152                 by a special command.
 153
 154                 Examples
 155
 156                 First we define a few shortcuts:
 157
 158                          (X Define %c0 (L s (L z z)))                     ; Church numeral 0
 159                          (X Define %succ (L n (L s (L z (s (n z z))))))   ; Successor
 160                          (X Define* %c1 (%succ %c0))
 161                          (X Define* %c2 (%succ %c1))
 162                          (X Define %add (L m (L n (L s (L z (m s (n s z))))))) ; Add two numerals
 163
 164                         (%add %c1 %c2)
 165                 REPL reduces the term and prints the answer: (L f (L x (f (f (f x))))).
 166
 167                          (X equal? (%succ %c0) %c1)
 168                          (X equal?* (%succ %c0) %c1)
 169
 170                 The REPL executes the above commands and prints the answer: #f and #t,
 171                 correspondingly. The second command reduces the terms before comparing them.
 172
 173         See also <http://okmij.org/ftp/Computation/lambda-calc.html>.
 174
 175
 176 5.      To play around with a **typed lambda calculus**, which we'll look at later
 177 in the course, have a look at the [Penn Lambda Calculator](http://www.ling.upenn.edu/lambda/).
 178 This requires installing Java, but provides a number of tools for evaluating
 179 lambda expressions and other linguistic forms. (Mac users will most likely
 180 already have Java installed.)
 181
 182 ## Reading about Scheme ##
 183
 184 [R5RS Scheme](http://people.csail.mit.edu/jaffer/r5rs_toc.html)
 185
 186 ## Reading about OCaml ##
 187
 188 -->
 189
 190