If a term `M` has type σ `-->` τ, and a term `N` has type
σ, then the application `MN` has type τ.
-These rules are clearly obverses of one another: the functional types
-that abstract builds up are taken apart by application.
+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):
+start with the implicational fragment, that is, the part of
+intuitionistic logic that only involves axioms and implications:
<pre>
Axiom: ---------
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 proof.
+used in the (sub)proof up to that point.
Using these labeling rules, we can label the proof
just given:
We have derived the *K* combinator, and typed it at the same time!
-Need a proof that involves application, and a proof with cut that will
-show beta reduction, so "normal" proof.
+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`.
+
+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
+--------------------------------------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...]
! (!a->!b) --> ! (!a->!b->!c)->!a->!c
--------------------------------------- R->
--> ! (!a->!b)->! (!a->!b->!c)->!a->!c
+
+
+
+<!--
+http://en.wikibooks.org/wiki/Haskell/The_Curry-Howard_isomorphism
+-->