X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=using_the_programming_languages.mdwn;h=2097dea239a5069e01e38cba1f749314dd013e18;hp=1c7aae6d8a3e852bce2986d3c997850290a12897;hb=613752800cab2472cbf8a751241ba3106f0acbbb;hpb=718c35b8eef781aef8bbd63e2c5ccebf6f5352dd diff --git a/using_the_programming_languages.mdwn b/using_the_programming_languages.mdwn index 1c7aae6d..2097dea2 100644 --- a/using_the_programming_languages.mdwn +++ b/using_the_programming_languages.mdwn @@ -27,47 +27,79 @@ 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. - - -3. Oleg Kiselyov has a [richer lambda interpreter](http://okmij.org/ftp/Scheme/#lambda-calc) in Scheme. Here's how he describes it: + + 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 +(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 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. + + 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. + 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. + + 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,35 @@ 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 = << fun s z -> z >>;; + let succ = << fun n s z -> s (n s z) >>;; + let one = << $succ$ $zero$ >>;; + let two = << $succ$ $one$ >>;; + let add = << fun m n -> n $succ$ m >>;; + (* or *) + let add = << fun m n -> fun s z -> m s (n s z) >>;; + + church_to_int << $add$ $one$ $two$ >>;; + - : int = 3 + + To install Jim's OCaml bundle, DO THIS... + + Some notes: + + * When you're talking to the interactive OCaml program, you have to finish complete statements with a ";;". Sometimes these aren't necessary, but rather than learn the rules yet about when you can get away without them, it's easiest to just use them consistently, like a period at the end of a sentence. + + * What's written betwen the `<<` and `>>` is parsed as an expression in the pure untyped lambda calculus. The stuff outside the angle brackets is regular OCaml syntax. Here you only need to use a very small part of that syntax: `let var = some_value;;` assigns a value to a variable, and `function_foo arg1 arg2` applies the specified function to the specified arguments. `church_to_int` is a function that takes a single argument --- the lambda expression that follows it, `<< $add$ $one$ $two$ >>` -- and, if that expression when fully reduced or "normalized" has the form of a "Church numeral", it converts it into an "int", which is OCaml's (and most language's) primitive way to represent small numbers. The line `- : int = 3` is OCaml telling you that the expression you just had it evaluate simplifies to a value whose type is "int" and which in particular is the int 3. + + * If you call `church_to_int` with a lambda expression that doesn't have the form of a Church numeral, it will complain. If you call it with something that's not even a lambda expression, it will complain in a different way. + + * The `$`s inside the `<<` and `>>` are essentially corner quotes. If we do this: `let a = << x >>;; let b = << a >>;; let c = << $a$ >>;;` then the OCaml variable `b` will have as its value an (atomic) lambda expression, consisting just of the variable `a` in the untyped lambda calculus. On the other hand, the OCaml variable `c` will have as its value a lambda expression consisting just of the variable `x`. That is, here the value of the OCaml variable `a` is spliced into the lambda expression `<< $a$ >>`. + + * The expression that's spliced in is done so as a single syntactic unit. In other words, the lambda expression `<< w x y z >>` is parsed via usual conventions as `<< (((w x) y) z) >>`. Here `<< x y >>` is not any single syntactic constituent. But if you do instead `let a = << x y >>;; let b = << w $a$ z >>`, then what you get *will* have `<< x y >>` as a constituent, and will be parsed as `<< ((w (x y)) z) >>`. + + * `<< fun x y -> something >>` is equivalent to `<< fun x -> fun y -> something >>`, which is parsed as `<< fun x -> (fun y -> (something)) >>` (everything to the right of the arrow as far as possible is considered together). At the moment, this only works for up to five variables, as in `<< fun x1 x2 x3 x4 x5 -> something >>`. + + * The `<< >>` and `$`-quotes aren't part of standard OCaml syntax, they're provided by this add-on bundle. For the most part it doesn't matter if other expressions are placed flush beside the `<<` and `>>`: you can do either `<< fun x -> x >>` or `<x>>`. But the `$`s *must* be separated from the `<<` and `>>` brackets with spaces or `(` `)`s. It's probably easiest to just always surround the `<<` and `>>` with spaces. - 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