X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=curry-howard.mdwn;h=183b54ebb463fb1cae33283053dc6703c15860dc;hp=f3c1be7590eb348711cee3bd4d25e993f1272749;hb=27ce0d45d4ab28840605ec2130f6ba4ecd9d6213;hpb=a738121a17239d9b723d64d2497b13c664465924 diff --git a/curry-howard.mdwn b/curry-howard.mdwn index f3c1be75..183b54eb 100644 --- a/curry-howard.mdwn +++ b/curry-howard.mdwn @@ -1,12 +1,12 @@ -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 @@ -18,13 +18,16 @@ 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 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: 
 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,14 +137,164 @@ 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`.
+
+
+-----------------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!
@@ -164,3 +317,9 @@ something like this:
        ! (!a->!b) --> ! (!a->!b->!c)->!a->!c
        --------------------------------------- R->
         --> ! (!a->!b)->! (!a->!b->!c)->!a->!c
+

+
+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]].