From d3336a1a5f222802c44b5a827428a4968b7d39c0 Mon Sep 17 00:00:00 2001 From: Jim Pryor Date: Tue, 24 Aug 2010 11:14:23 -0400 Subject: [PATCH 1/1] tweaks to using page Signed-off-by: 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/#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 @@ -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 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. @@ -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