From: Chris Barker 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;hp=945835525c1a4f9d8210693af0b60ecf957ba8be 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 -
``` -----------------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,9 +317,7 @@ something like this:
! (!a->!b) --> ! (!a->!b->!c)->!a->!c
--------------------------------------- R->
--> ! (!a->!b)->! (!a->!b->!c)->!a->!c
+

-
-
-