-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
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
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!
! (!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]].