Curry-Howard, take 1 -------------------- 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. 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:
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
`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:
-------  Id
A |- A
---------- Weak
A, B |- A
------------- --> I
A |- B --> A
----------------- --> I
|- A --> B --> A
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:
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
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:
------------  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
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:
------------------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 
With labels, we have
------------------------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 
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`.
-----------------------------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 
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
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.
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`. 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
--------------------------------------Modus Ponens (proved above)
John:e, P:e->t |- (P John):t
--------------------------------- --> I
John:e |- (\P.P John):(e->t)->t
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: --------- 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