From: Chris Barker <barker@kappa.linguistics.fas.nyu.edu>
Date: Mon, 13 Dec 2010 19:08:11 +0000 (-0500)
Subject: edits
X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=6ab1e3696ca3e88acf79a52ba2841bc8c66f7c98

edits
---

diff --git a/curry-howard.mdwn b/curry-howard.mdwn
index fe861c4d..9aa79504 100644
--- 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
@@ -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`.
 
-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
@@ -291,13 +289,12 @@ from verb phrase meanings to truth values, just as we would need.
 
 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:
 
+<pre>
            --------- Ax  --------- Ax   ------- Ax
            !a --> !a     !b --> !b      c --> c
            ----------------------- L->  -------- L!
@@ -320,9 +317,7 @@ something like this:
        ! (!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
+[[http://en.wikibooks.org/wiki/Haskell/The_Curry-Howard_isomorphism]].