From d3336a1a5f222802c44b5a827428a4968b7d39c0 Mon Sep 17 00:00:00 2001
From: Jim Pryor
Date: Tue, 24 Aug 2010 11:14:23 0400
Subject: [PATCH] tweaks to using page
Signedoffby: Jim Pryor

using_the_programming_languages.mdwn  44 ++++++++++++++++++
1 file changed, 22 insertions(+), 22 deletions()
diff git a/using_the_programming_languages.mdwn b/using_the_programming_languages.mdwn
index 9faaad4f..bfb97ae4 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.
@@ 113,13 +113,13 @@ 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 two = << $succ$ $one$ >>
let add = < n $succ$ m>>
 let pred = < n (fun u v > v (u s)) ($k$ z) $id$ >>;;

 church_to_int << $pred$ ($add$ $one$ ($succ$ $one$)) >>;;
  : int = 2
+ (* or *)
+ let add = < 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

2.11.0