From 2ee0d2918d40efc78e75ce8fbc6ae90f8edf6541 Mon Sep 17 00:00:00 2001 From: Jim Pryor Date: Thu, 23 Sep 2010 06:13:25 -0400 Subject: [PATCH] cleanup Signed-off-by: Jim Pryor --- code/{ => caml-lambda}/lambda.ml | 0 code/{ => caml-lambda}/q_lambda.ml | 0 code/sample.html | 91 ---------------- index.mdwn | 19 ++-- offsite_reading.mdwn | 1 + using_the_programming_languages.mdwn | 199 ----------------------------------- 6 files changed, 14 insertions(+), 296 deletions(-) rename code/{ => caml-lambda}/lambda.ml (100%) rename code/{ => caml-lambda}/q_lambda.ml (100%) delete mode 100644 code/sample.html delete mode 100644 using_the_programming_languages.mdwn diff --git a/code/lambda.ml b/code/caml-lambda/lambda.ml similarity index 100% rename from code/lambda.ml rename to code/caml-lambda/lambda.ml diff --git a/code/q_lambda.ml b/code/caml-lambda/q_lambda.ml similarity index 100% rename from code/q_lambda.ml rename to code/caml-lambda/q_lambda.ml diff --git a/code/sample.html b/code/sample.html deleted file mode 100644 index 0f44885b..00000000 --- a/code/sample.html +++ /dev/null @@ -1,91 +0,0 @@ - - - - - - Top Down Operator Precedence - - -

Top Down Operator Precedence

- -

Douglas Crockford

- -

2007-08-05

- -

Demonstration

The text that follows is the parse tree that the parser generated by - parsing itself.

- - - - - - - -

- - - diff --git a/index.mdwn b/index.mdwn index 7c752238..28fc8c49 100644 --- a/index.mdwn +++ b/index.mdwn @@ -10,11 +10,21 @@ This course will be co-taught by [Chris Barker](http://homepages.nyu.edu/~cb125/ The seminar meets on Mondays from 4-6, in the Linguistics building at 10 Washington Place, in room 104 (back of the first floor). -We've sent around an email to those who left their email addresses on the roster we passed around. But it's clear that the roster didn't make its way to everyone. So if you didn't receive our email this evening, please email with your email address, and if you're a student, say whether you expect to audit or take the class for credit. - Student sessions will be held on Tuesdays from 11-12 and Wednesdays from 3-4. (You only need attend one session.) You should see these sessions as opportunities to clear up lingering issues from material we've discussed, and help get a better footing for what we'll be doing the next week. It would be smart to make a serious start on that week's homework, for instance, before the session. -Lots of lecture notes summarizing and expanding on last Monday's seminar now posted. Also, lecture notes for upcoming session have been posted. (Click "Notes and Schedule".) +We've sent around an email to those who left their email addresses on the roster we passed around. But it's clear that the roster didn't make its way to everyone. So if you're not receiving our seminar emails, please email with your email address, and if you're a student, say whether you expect to audit or take the class for credit. + +There is now a [[lambda evaluator]] you can use in your browser (no need to install any software). +It can help you check whether your answer to some of the homework questions works correctly. + + + ## Lecture Notes and Assignments ## @@ -26,9 +36,6 @@ Topics: Applications; Basics of Lambda Calculus; Comparing Different Languages Topics: Reduction and Convertibility; Combinators; Evaluation Strategies and Normalization; Decidability; Lists and Numbers -There is now a [[lambda evaluator]] you can use in your browser (no need to install any software). -It can help you check whether your answer to some of the homework questions works correctly. - (27 Sept) ...(Notes to come) Topics: Recursion with Fixed Point Combinators diff --git a/offsite_reading.mdwn b/offsite_reading.mdwn index 0c6a19da..d9c7f826 100644 --- a/offsite_reading.mdwn +++ b/offsite_reading.mdwn @@ -46,6 +46,7 @@ get more out of. (Rinse and repeat.) ## Untyped lambda calculus and combinatory logic ## * [[!wikipedia Lambda calculus]] +* Our [[Lambda evaluator]] * [Chris Barker's Lambda Tutorial](http://homepages.nyu.edu/~cb125/Lambda) * [Lambda Animator](http://thyer.name/lambda-animator/) * [Penn lambda calculator](http://www.ling.upenn.edu/lambda/) Pedagogical software developed by Lucas Champollion, Josh Tauberer and Maribel Romero.

diff --git a/using_the_programming_languages.mdwn b/using_the_programming_languages.mdwn deleted file mode 100644 index 6952e499..00000000 --- a/using_the_programming_languages.mdwn +++ /dev/null @@ -1,199 +0,0 @@ - -## 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) >>;; - . - (* now use: - pp FORMULA to print a formula, unreduced - pn FORMULA to print the normal form of a formula (when possible) - pi FORMULA to print the integer which FORMULA is a Church numeral for (when possible) - . - alpha_eq FORM1 FORM2 are FORM1 and FORM2 syntactically equivalent (up to alpha-conversion)? - this does not do reductions on the formulae - *) - . - pi << $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 - - We assume here that you've already [gotten OCaml installed on your computer](/how_to_get_the_programming_languages_running_on_your_computer/). - - 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. - - - - - -- 2.11.0