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
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.
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