+++ /dev/null
-Curry-Howard
-------------
-
-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
-roughly as follows:
-
-If a variable `x` has type σ and term `M` has type τ, then
-the abstract `\xM` has type σ `-->` τ.
-
-If a term `M` has type σ `-->` τ, and a term `N` has type
-σ, then the application `MN` has type τ.
-
-These rules are clearly inverse of one another (in some sense to be
-made precise): the functional types that abstract builds up are taken
-apart by application. The intuition that abstraction and application
-are dual to each other is the heart of the Curry-Howard
-correspondence.
-
-The next step in making sense out of the Curry-Howard corresponence is
-to present a logic. It will be a part of intuitionistic logic. We'll
-start with the implicational fragment, that is, the part of
-intuitionistic logic that only involves axioms and implications:
-
-<pre>
-Axiom: ---------
- A |- A
-
-Structural Rules:
-
- Γ, A, B, Δ |- C
-Exchange: ---------------------------
- Γ, B, A, Δ |- C
-
- Γ, A, A |- B
-Contraction: -------------------
- Γ, A |- B
-
- Γ |- B
-Weakening: -----------------
- Γ, A |- B
-
-Logical Rules:
-
- Γ, A |- B
---> I: -------------------
- Γ |- A --> B
-
- Γ |- A --> B Γ |- A
---> E: -----------------------------------
- Γ |- B
-</pre>
-
-`A`, `B`, etc. are variables over formulas.
-Γ, Δ, etc. are variables over (possibly empty) sequences
-of formulas. Γ `|- A` is a sequent, and is interpreted as
-claiming that if each of the formulas in Γ is true, then `A`
-must also be true.
-
-This logic allows derivations of theorems like the following:
-
-<pre>
-------- Id
-A |- A
----------- Weak
-A, B |- A
-------------- --> I
-A |- B --> A
------------------ --> I
-|- A --> B --> A
-</pre>
-
-Should remind you of simple types. (What was `A --> B --> A` the type
-of again?)
-
-The easy way to grasp the Curry-Howard correspondence is to *label*
-the proofs. Since we wish to establish a correspondence between this
-logic and the lambda calculus, the labels will all be terms from the
-simply-typed lambda calculus. Here are the labeling rules:
-
-<pre>
-Axiom: -----------
- x:A |- x:A
-
-Structural Rules:
-
- Γ, x:A, y:B, Δ |- R:C
-Exchange: -------------------------------
- Γ, y:B, x:A, Δ |- R:C
-
- Γ, x:A, x:A |- R:B
-Contraction: --------------------------
- Γ, x:A |- R:B
-
- Γ |- R:B
-Weakening: ---------------------
- Γ, x:A |- R:B [x chosen fresh]
-
-Logical Rules:
-
- Γ, x:A |- R:B
---> I: -------------------------
- Γ |- \xM:A --> B
-
- Γ |- f:(A --> B) Γ |- x:A
---> E: -------------------------------------
- Γ |- (fx):B
-</pre>
-
-In these labeling rules, if a sequence Γ in a premise contains
-labeled formulas, those labels remain unchanged in the conclusion.
-
-What is means for a variable `x` to be chosen *fresh* is that
-`x` must be distinct from any other variable in any of the labels
-used in the (sub)proof up to that point.
-
-Using these labeling rules, we can label the proof
-just given:
-
-<pre>
------------- Id
-x:A |- x:A
----------------- Weak
-x:A, y:B |- x:A
-------------------------- --> I
-x:A |- (\y.x):(B --> A)
----------------------------- --> I
-|- (\x y. x):A --> B --> A
-</pre>
-
-We have derived the *K* combinator, and typed it at the same time!
-
-In order to make use of the dual rule, the one for `-->` elimination,
-we need a context that will entail both `A --> B` and `A`. Here's
-one, first without labels:
-
-<pre>
-------------------Axiom
-A --> B |- A --> B
----------------------Weak ---------Axiom
-A --> B, A |- A --> B A |- A
----------------------Exch -----------------Weak
-A, A --> B |- A --> B A, A --> B |- A
--------------------------------------------------- --> E
-A, A --> B |- B
-</pre>
-
-With labels, we have
-
-<pre>
-------------------------Axiom
-f:A --> B |- f:A --> B
-----------------------------Weak -------------Axiom
-f:A --> B, x:A |- f:A --> B x:A |- x:A
-----------------------------Exch ------------------------Weak
-x:A, f:A --> B |- f:A --> B x:A, f:A --> B |- x:A
--------------------------------------------------------------- --> E
-x:A, f:A --> B |- (fx):B
-</pre>
-
-Note that in order for the `--> E` rule to apply, the left context and
-the right context (the material to the left of each of the turnstiles)
-must match exactly, in this case, `x:A, f:A --> B`.
-
-At this point, an application to natural language will help provide
-insight.
-Instead of labelling the proof above with the kinds of symbols we
-might use in a program, we'll label it with symbols we might use in an
-English sentence. Instead of a term `f` with type `A --> B`, we'll
-have the English word `left`; and instead of a term `x` with type `A`,
-we'll have the English word `John`.
-
-<pre>
------------------------------Axiom
-left:e --> t |- left:e --> t
---------------------------------------Weak -------------------Axiom
-left:e --> t, John:e |- left:e --> t John:e |- John:e
---------------------------------------Exch --------------------------------Weak
-John:e, left:e --> t |- left:e --> t John:e, left:e --> t |- John:e
----------------------------------------------------------------------------------- --> E
-John:e, left:e --> t |- (left John):t
-</pre>
-
-This proof illustrates how a logic can
-provide three things that a complete grammar of a natural language
-needs:
-
-* It characterizes which words and expressions can be combined in
-order to form a more complex expression. For instance, we've
-just seen a proof that "left" can combine with "John".
-
-* It characterizes the type (the syntactic category) of the result.
-In the example, an intransitive verb phrase of type `e --> t` combines
-with a determiner phrase of type `e` to form a sentence of type `t`.
-
-* It characterizes the semantic recipe required to compute the meaning
- of the complex expression based on the meanings of the parts: the
- way to compute to meaning of the expression "John left" is to take
- the function denoted by "left" and apply it to the individual
- denoted by "John", viz., "(left John)".
-
-This last point is the truly novel and beautiful part, the part
-contributed by the Curry-Howard result.
-
-[Incidentally, note that this proof also suggests that if we have the
-expressions "John" followed by "left", we also have a determiner
-phrase of type `e`. If you want to make sure that the contribution of
-each word counts (no weakening), you have to use a resource-sensitive
-approach like Linear Logic or Type Logical Grammar.
-
-In this trivial example, it may not be obvious that anything
-interesting is going on, so let's look at a slightly more complicated
-example, one that combines abstraction with application.
-
-Linguistic assumptions (abundently well-motivated, but we won't pause
-to review the motivations here):
-
-Assumption 1:
-Coordinating conjunctions like *and*, *or*, and *but* require that
-their two arguments must have the same sytnactic type. Thus we can
-have
-
-<pre>
-1. [John left] or [Mary left] coordination of t
-2. John [left] or [slept] coordination of e -> t
-3. [John] or [Mary] left coordination of e
-etc.
-
-4. *John or left.
-5. *left or Mary slept.
-etc.
-</pre>
-
-If the two disjuncts have the same type, the coordination is perfectly
-fine, as (1) through (3) illustrate. But when the disjuncts don't
-match, as in (4) and (5), the result is ungrammatical (though there
-are examples that may seem to work; each usually has a linguistic
-story that needs to be told).
-
-In general, then, *and* and *or* are polymorphic, and have the type
-`and:('a -> 'a -> 'a)`. In the discussion below, we'll use a more
-specific instance to keep the discussion concrete, and to abstract
-away from polymorphism.
-
-Assumption 2:
-Some determiner phrases do not denote an indivdual of type `e`, and
-denote only functions of a higher type, typically `(e -> t) -> t` (the
-type of an (extensional) generalized quantifier). So *John* has type
-`e`, but *everyone* has type `(e -> t) -> t`.
-
-[Excercise: prove using the logic above that *Everyone left* can have
-`(everyone left)` as its Curry-Howard labeling.]
-
-The puzzle, then, is how it can be possible to coordinate generalized
-quantifier determiner phrases with non-generalized quantifier
-determiner phrases:
-
-1. John and every girl laughed.
-2. Some boy or Mary should leave.
-
-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`.
-
-<pre>
------------------Ax -----------------Ax
-John:e |- John:e P:e->t |- P:e->t
---------------------------------------Modus Ponens (proved above)
-John:e, P:e->t |- (P John):t
---------------------------------- --> I
-John:e |- (\P.P John):(e->t)->t
-</pre>
-
-This proof is very interesting: it says that if *John* has type `e`,
-then *John* automatically can be used as if it also has type
-`(e->t)->t`, the type of a generalized quantifier.
-The Curry-Howard labeling is the term `\P.P John`, which is a function
-from verb phrase meanings to truth values, just as we would need.
-
-[John and everyone left]
-
-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,!a->!b --> !b !c --> c
---------- Ax ---------------------------------- L->
-!a --> !a !a,!b->!c,!a->!b --> c
------------------------------------------- L->
- !a,!a,!a->!b->!c,!a->!b --> c
- ----------------------------- C!
- !a,!a->!b->!c,!a->!b --> c
- ------------------------------ L!
- !a,!a->!b->!c,! (!a->!b) --> c
- ---------------------------------- L!
- !a,! (!a->!b->!c),! (!a->!b) --> c
- ----------------------------------- R!
- !a,! (!a->!b->!c),! (!a->!b) --> !c
- ------------------------------------ R->
- ! (!a->!b->!c),! (!a->!b) --> !a->!c
- ------------------------------------- R->
- ! (!a->!b) --> ! (!a->!b->!c)->!a->!c
- --------------------------------------- R->
- --> ! (!a->!b)->! (!a->!b->!c)->!a->!c
-</pre>
-
-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]].