From: Jim Pryor Date: Mon, 20 Sep 2010 16:07:20 +0000 (-0400) Subject: start linking to lambda calculators X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=85bd77d2f5fc08beca4d2d65ccf9a6cf81b4a658;hp=327c2d4e885b7ba7a56e92e39b77940fb345aaf1 start linking to lambda calculators Signed-off-by: Jim Pryor --- diff --git a/assignment2.mdwn b/assignment2.mdwn index 066f1b1f..85f63f36 100644 --- a/assignment2.mdwn +++ b/assignment2.mdwn @@ -1,3 +1,6 @@ +For these assignments, you'll probably want to use a "lambda calculator" to check your work. This accepts any grammatical lambda expression and reduces it to normal form, when possible. See the page on [[using the programming languages]] for instructions and links about setting this up. + + More Lambda Practice -------------------- diff --git a/using_the_programming_languages.mdwn b/using_the_programming_languages.mdwn index 2097dea2..bdba8d09 100644 --- a/using_the_programming_languages.mdwn +++ b/using_the_programming_languages.mdwn @@ -3,6 +3,75 @@ We assume here that you've already gotten [Schema and OCaml installed on your co ## Programming in the pure untyped lambda calculus ## +There are several ways to do this. + +1. The easiest is to use a JavaScript interpreter that Chris wrote. Go [here](/lambda-let.html) and follow the template: + + let true = (\x (\y x)) in + let false = (\x (\y y)) in + let and = (\l (\r ((l r) false))) in + + ( + + ((((and false) false) yes) no) + + ((((and false) true) yes) no) + + ((((and true) false) yes) no) + + ((((and true) true) yes) no) + + ) + + will evaluate to: + + (no no no yes) + + If you try to evaluate a non-terminating form, like `((\x (x x)) (\x (x x)))`, you'll probably have to force-quit your browser and start over. Anything you had earlier typed in the upper box will probably be lost. + + Syntax: you have to fully specify parentheses and separate your lambdas. So for example, you can't write `(\x y. y)`; you have to write `(\x (\y y))`. The parser treats symbols that haven't yet been bound (as `yes` and `no` above) as free variables. + + +2. A bit more flexibility and robustness can be had by using an OCaml package. This is based on a library on [a Haskell library by Oleg Kiselyov](http://okmij.org/ftp/Computation/lambda-calc.html#lambda-calculator-haskell). + + 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 = << 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 this package, here's what you need to do. I've tried to explain it in basic terms, but you do need some familiarity with your operating system: for instance, how to open a Terminal window, how to figure out what directory the Terminal is open to (use `pwd`); how to change directories (use `cd`); and so on. + + INCLUDE INSTRUCTIONS + + 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. + + + +