whitespace, formatting

Signed-off-by: Jim Pryor <profjim@jimpryor.net>

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 8de3b70..063957a 100644 (file)
--- 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.
        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:
 
 
 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.
 
        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,
 *      **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 7953845..877ff47 100644 (file)
--- a/index.mdwn
+++ b/index.mdwn
@@ -81,7 +81,7 @@ Other keywords:
        the Curry-Howard isomorphism(s)
        monads in category theory and computation
 -->
        the Curry-Howard isomorphism(s)
        monads in category theory and computation
 -->

-       
+

 ## Who Can Participate? ##
 
 The course will not presume previous experience with programming.  We
 ## 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.
 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 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
 Philosophy PhD students.
 
 Faculty and students from outside of NYU Linguistics and Philosophy are welcome


@@ -138,7 +138,7 @@ other.
 
 [[Using the programming languages]]
 
 
 [[Using the programming languages]]
 

-       
+

 ## Recommended Books ##
 
 *      *An Introduction to Lambda Calculi for Computer Scientists*, by Chris
 ## 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 eb7cf80..50a9c33 100644 (file)
--- 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<p>
 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<p>

-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)
        * [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 1c7aae6..9faaad4 100644 (file)
--- 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
                                   ((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:
                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]))
                (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
 
 
 
 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:
                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)
 
                         (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 <http://okmij.org/ftp/Computation/lambda-calc.html>.
 
 
        See also <http://okmij.org/ftp/Computation/lambda-calc.html>.
 


@@ -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:
 
 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 k = <<fun y _ -> y>>
-       let id = <<fun x -> x>>
-       let add = <<fun m n -> n $succ$ m>>
-       let pred = <<fun n s z -> 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 k = <<fun y _ -> y>>
+               let id = <<fun x -> x>>
+               let add = <<fun m n -> n $succ$ m>>
+               let pred = <<fun n s z -> 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
 
 
 5.     To play around with a **typed lambda calculus**, which we'll look at later