the Curry-Howard isomorphism(s)
monads in category theory and computation
-->
-
+
## Who Can Participate? ##
The course will not presume previous experience with programming. We
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
[[Using the programming languages]]
-
+
## Recommended Books ##
* *An Introduction to Lambda Calculi for Computer Scientists*, by Chris
((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:
(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>.
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