X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=curry-howard.mdwn;h=183b54ebb463fb1cae33283053dc6703c15860dc;hp=6cd08c10de8cd1f8257bbdb1a2c82bef04adb3d8;hb=1e70b7849153992272e219477464128c8d97789a;hpb=fa3fcd726119256a230682b5125180daefd11235 diff --git a/curry-howard.mdwn b/curry-howard.mdwn index 6cd08c10..183b54eb 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 -
``` -----------------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:

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