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, and we're still thinking out loud in this space about which method we should recommend you use.
   7
   8 1.      To get started, Chris has a nice [Lambda Tutorial](http://homepages.nyu.edu/~cb125/Lambda)
   9 webpage introducing the untyped lambda calculus. This page has embedded Javascript
  10 code that enables you to type lambda expressions into your web browser page
  11 and click a button to "execute" (that is, reduce or normalize) it.
  12
  13         To do more than a few simple exercises, though, you'll need something more complex.
  14
  15 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).
  16 You can use this by loading into a Scheme interpreter (EXPLAIN HOW...) and then (STEP BY STEP...).
  17
  18         Here's Chris' explanation of the macro:
  19
  20                 (define (reduce f)                                                          ; 1
  21                   ((lambda (value) (if (equal? value f) f (reduce value)))                  ; 2
  22                    (let r ((f f) (g ()))                                                    ; 3
  23                          (cond ((not (pair? f))                                                 ; 4
  24                                         (if (null? g) f (if (eq? f (car g)) (cadr g) (r f (caddr g))))) ; 5
  25                                    ((and (pair? (car f)) (= 2 (length f)) (eq? 'lambda (caar f)))   ; 6
  26                                         (r (caddar f) (list (cadar f) (r (cadr f) g) g)))               ; 7
  27                                    ((and (not (null? g)) (= 3 (length f)) (eq? 'lambda (car f)))    ; 8
  28                                         (cons 'lambda (r (cdr f) (list (cadr f) (delay (cadr f)) g))))  ; 9
  29                                    (else (map (lambda (x) (r x g)) f))))))                          ;10
  30
  31                 If you have a Scheme interpreter, you can call the function like this:
  32
  33                 (reduce '(((lambda x (lambda y (x y))) 2) 3))
  34                 ;Value: (2 3)
  35
  36                 (reduce '((lambda x (lambda y (x y))) 2))
  37                 ;Value: (lambda #[promise 2] (2 #[promise 2]))
  38
  39                 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.
  40
  41
  42 3.      Oleg Kiselyov has a [richer lambda interpreter](http://okmij.org/ftp/Scheme/#lambda-calc) in Scheme. Here's how he describes it:
  43
  44                 A practical Lambda-calculator in Scheme
  45
  46                 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.
  47
  48                 The code also includes a few convenience tools: tracing of all reduction, comparing two terms modulo alpha-renaming, etc.
  49
  50                 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.
  51
  52                 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.
  53                 Examples
  54
  55                 First we define a few shortcuts:
  56
  57                          (X Define %c0 (L f (L x x)))                     ; Church numeral 0
  58                          (X Define %succ (L c (L f (L x (f (c f x))))))   ; Successor
  59                          (X Define* %c1 (%succ %c0))
  60                          (X Define* %c2 (%succ %c1))
  61                          (X Define %add (L c (L d (L f (L x (c f (d f x))))))) ; Add two numerals
  62                          (X Define %mul (L c (L d (L f (c (d f))))))      ; Multiplication
  63
  64                 (%add %c1 %c2)
  65                 REPL reduces the term and prints the answer: (L f (L x (f (f (f x))))).
  66
  67                          (X equal? (%succ %c0) %c1)
  68                          (X equal?* (%succ %c0) %c1)
  69
  70                 The REPL executes the above commands and prints the answer: #f and #t, correspondingly. The second command reduces the terms before comparing them.
  71
  72         See also <http://okmij.org/ftp/Computation/lambda-calc.html>.
  73
  74
  75 4.      Oleg also provides another lambda interpreter [written in
  76 Haskell](http://okmij.org/ftp/Computation/lambda-calc.html#lambda-calculator-haskell).
  77 Jim converted this to OCaml and bundled it with a syntax extension that makes
  78 it easier to write pure untyped lambda expressions in OCaml. You don't have to
  79 know much OCaml yet to use it. Using it looks like this:
  80
  81         let zero = <<fun s z -> z>>
  82         let succ = <<fun n s z -> s (n s z)>>
  83         let one = << $succ$ $zero$ >>
  84         let k = <<fun y _ -> y>>
  85         let id = <<fun x -> x>>
  86         let add = <<fun m n -> n $succ$ m>>
  87         let pred = <<fun n s z -> n (fun u v -> v (u s)) ($k$ z) $id$ >>;;
  88
  89         church_to_int << $pred$ ($add$ $one$ ($succ$ $one$)) >>;;
  90         - : int = 2
  91
  92
  93 5.      To play around with a **typed lambda calculus**, which we'll look at later
  94 in the course, have a look at the [Penn Lambda Calculator](http://www.ling.upenn.edu/lambda/).
  95 This requires installing Java, but provides a number of tools for evaluating
  96 lambda expressions and other linguistic forms. (Mac users will most likely
  97 already have Java installed.)
  98
  99
 100 ## Reading about Scheme ##
 101
 102 [R5RS Scheme](http://people.csail.mit.edu/jaffer/r5rs_toc.html)
 103
 104 ## Reading about OCaml ##
 105
 106