author Chris Barker Mon, 13 Dec 2010 19:08:11 +0000 (14:08 -0500) committer Chris Barker Mon, 13 Dec 2010 19:08:11 +0000 (14:08 -0500)

index fe861c4..9aa7950 100644 (file)
@@ -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>

-
-
-<!--