X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=using_the_programming_languages.mdwn;fp=using_the_programming_languages.mdwn;h=9faaad4f34de5b53d4778cb8e6ea003b2a305f04;hp=1c7aae6d8a3e852bce2986d3c997850290a12897;hb=d773dfc0b5aab6bc79f9a6990af79aed988648f4;hpb=718c35b8eef781aef8bbd63e2c5ccebf6f5352dd diff --git a/using_the_programming_languages.mdwn b/using_the_programming_languages.mdwn index 1c7aae6d..9faaad4f 100644 --- a/using_the_programming_languages.mdwn +++ b/using_the_programming_languages.mdwn @@ -27,29 +27,60 @@ You can use this by loading into a Scheme interpreter (EXPLAIN HOW...) and then ((and (not (null? g)) (= 3 (length f)) (eq? 'lambda (car f))) ; 8 (cons 'lambda (r (cdr f) (list (cadr f) (delay (cadr f)) g)))) ; 9 (else (map (lambda (x) (r x g)) f)))))) ;10 - + If you have a Scheme interpreter, you can call the function like this: - + (reduce '(((lambda x (lambda y (x y))) 2) 3)) ;Value: (2 3) (reduce '((lambda x (lambda y (x y))) 2)) ;Value: (lambda #[promise 2] (2 #[promise 2])) - - 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. + + 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. 3. Oleg Kiselyov has a [richer lambda interpreter](http://okmij.org/ftp/Scheme/#lambda-calc) in Scheme. Here's how he describes it: 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 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. + 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 + 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. + + 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. - 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: @@ -67,7 +98,8 @@ You can use this by loading into a Scheme interpreter (EXPLAIN HOW...) and then (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. + The REPL executes the above commands and prints the answer: #f and #t, + correspondingly. The second command reduces the terms before comparing them. See also . @@ -78,16 +110,16 @@ Jim converted this to OCaml and bundled it with a syntax extension that makes it easier to write pure untyped lambda expressions in OCaml. You don't have to 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 add = < n $succ$ m>> - let pred = < n (fun u v -> v (u s)) ($k$ z) $id$ >>;; + let zero = < z>> + let succ = < s (n s z)>> + let one = << $succ$ $zero$ >> + let k = < y>> + let id = < x>> + 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 + church_to_int << $pred$ ($add$ $one$ ($succ$ $one$)) >>;; + - : int = 2 5. To play around with a **typed lambda calculus**, which we'll look at later