update .gitignore

[lambda.git] / curry-howard.mdwn

diff --git a/curry-howard.mdwn b/curry-howard.mdwn
index fe861c4..183b54e 100644 (file)
--- a/curry-howard.mdwn
+++ b/curry-howard.mdwn
@@ -1,12 +1,12 @@
-Curry-Howard, take 1
---------------------
+Curry-Howard
+------------

 
 

-We will return to the Curry-Howard correspondence a number of times
-during this course.  It expresses a deep connection between logic,
-types, and computation.  Today we'll discuss how the simply-typed
-lambda calculus corresponds to intuitionistic logic.  This naturally
-give rise to the question of what sort of computation classical logic
-corresponds to---as we'll see later, the answer involves continuations.
+The Curry-Howard correspondence expresses a deep connection between
+logic, types, and computation.  Today we'll discuss how the
+simply-typed lambda calculus corresponds to intuitionistic logic.
+This naturally give rise to the question of what sort of computation
+classical logic corresponds to---as we'll see later, the answer
+involves continuations.

 
 So at this point we have the simply-typed lambda calculus: a set of
 ground types, a set of functional types, and some typing rules, given
 
 So at this point we have the simply-typed lambda calculus: a set of
 ground types, a set of functional types, and some typing rules, given


@@ -270,8 +270,6 @@ The answer involves reasoning about what it means to be an individual.
 Let the type of *or* in this example be `Q -> Q -> Q`, where
 `Q` is the type of a generalized quantifier, i.e, `Q = ((e->t)->t`.
 
 Let the type of *or* in this example be `Q -> Q -> Q`, where
 `Q` is the type of a generalized quantifier, i.e, `Q = ((e->t)->t`.
 

-John:e |- John:e, or:(Q->Q->Q) |- , everyone:Q, left:e->t
-

 <pre>
 -----------------Ax  -----------------Ax
 John:e |- John:e     P:e->t |- P:e->t
 <pre>
 -----------------Ax  -----------------Ax
 John:e |- John:e     P:e->t |- P:e->t


@@ -291,13 +289,12 @@ from verb phrase meanings to truth values, just as we would need.
 
 beta reduction = normal proof.
 
 
 beta reduction = normal proof.
 

-
-

 [To do: add pairs and destructors; unit and negation...]
 
 Excercise: construct a proof whose labeling is the combinator S,
 something like this:
 
 [To do: add pairs and destructors; unit and negation...]
 
 Excercise: construct a proof whose labeling is the combinator S,
 something like this:
 

+<pre>

            --------- Ax  --------- Ax   ------- Ax
            !a --> !a     !b --> !b      c --> c
            ----------------------- L->  -------- L!
            --------- Ax  --------- Ax   ------- Ax
            !a --> !a     !b --> !b      c --> c
            ----------------------- L->  -------- L!


@@ -320,9 +317,9 @@ something like this:
        ! (!a->!b) --> ! (!a->!b->!c)->!a->!c
        --------------------------------------- R->
         --> ! (!a->!b)->! (!a->!b->!c)->!a->!c
        ! (!a->!b) --> ! (!a->!b->!c)->!a->!c
        --------------------------------------- R->
         --> ! (!a->!b)->! (!a->!b->!c)->!a->!c

+</pre>

 
 

-
-
-<!--
-http://en.wikibooks.org/wiki/Haskell/The_Curry-Howard_isomorphism
--->
+See also
+[Wadler's symmetric
+calculus](http://homepages.inf.ed.ac.uk/wadler/papers/dual/dual.pdf), and
+[[http://en.wikibooks.org/wiki/Haskell/The_Curry-Howard_isomorphism]].