From d773dfc0b5aab6bc79f9a6990af79aed988648f4 Mon Sep 17 00:00:00 2001 From: Jim Pryor Date: Tue, 24 Aug 2010 11:01:24 -0400 Subject: [PATCH] whitespace, formatting Signed-off-by: Jim Pryor --- ...ramming_languages_running_on_your_computer.mdwn | 4 +- index.mdwn | 8 +-- schedule_of_topics.mdwn | 2 +- using_the_programming_languages.mdwn | 72 ++++++++++++++++------ 4 files changed, 59 insertions(+), 27 deletions(-) diff --git a/how_to_get_the_programming_languages_running_on_your_computer.mdwn b/how_to_get_the_programming_languages_running_on_your_computer.mdwn index 8de3b703..063957a5 100644 --- a/how_to_get_the_programming_languages_running_on_your_computer.mdwn +++ b/how_to_get_the_programming_languages_running_on_your_computer.mdwn @@ -26,7 +26,7 @@ you'll be in one of two subgroups: Then you'll need pre-packaged (and usually pretty GUI) installers for everything. These are great when they're available and kept up-to-date; however those conditions aren't always met. - + If you're using **Windows**, you'll be in one of two subgroups: @@ -173,7 +173,7 @@ However, if you're not able to get that working, don't worry about it much. This will build an installer package which you should be able to double-click and install. - + * **To install on Mac with MacPorts** You can install the previous version of OCaml (3.11.2, diff --git a/index.mdwn b/index.mdwn index 79538456..877ff47e 100644 --- a/index.mdwn +++ b/index.mdwn @@ -81,7 +81,7 @@ Other keywords: the Curry-Howard isomorphism(s) monads in category theory and computation --> - + ## Who Can Participate? ## The course will not presume previous experience with programming. We @@ -90,12 +90,12 @@ languages, and we will encourage experimentation with running, modifying, and writing computer programs. The course will not presume lots of mathematical or logical background, either. -However, it will demand a certain amount of comfort working with such material; as a result, +However, it will demand a certain amount of comfort working with such material; as a result, it will not be especially well-suited to be a first graduate-level course in formal semantics or philosophy of language. If you have concerns about your background, come discuss them with us. -It hasn't yet been decided whether this course counts for satisfying the logic requirement for +It hasn't yet been decided whether this course counts for satisfying the logic requirement for Philosophy PhD students. Faculty and students from outside of NYU Linguistics and Philosophy are welcome @@ -138,7 +138,7 @@ other. [[Using the programming languages]] - + ## Recommended Books ## * *An Introduction to Lambda Calculi for Computer Scientists*, by Chris diff --git a/schedule_of_topics.mdwn b/schedule_of_topics.mdwn index eb7cf80a..50a9c33b 100644 --- a/schedule_of_topics.mdwn +++ b/schedule_of_topics.mdwn @@ -52,7 +52,7 @@ This is very sketchy at this point, but it should give a sense of our intended s 15. The types of continuations; continuations as first-class values 16. [Phil/ling application] Partee on whether NPs should be uniformly interpreted as generalized quantifiers, or instead "lifted" when necessary. Lifting = a CPS transform. 17. [Phil/ling application] Expletives

-18. Some references: +18. Some references: * [de Groote on the lambda-mu calculus in linguistics](http://www.loria.fr/%7Edegroote/papers/amsterdam01.pdf) * [on donkey anaphora and continuations](http://dx.doi.org/10.3765/sp.1.1) * [Wadler on symmetric sequent calculi](http://homepages.inf.ed.ac.uk/wadler/papers/dual-reloaded/dual-reloaded.pdf) 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 -- 2.11.0