Axiom: --------- @@ -116,7 +119,7 @@ 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 proof. +used in the (sub)proof up to that point. Using these labeling rules, we can label the proof just given: @@ -134,8 +137,161 @@ x:A |- (\y.x):(B --> A) 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: + ++------------------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...]