Summary: Coordination in Categorial Grammar

[Carl Pollard]

Hi Ash,

Thanks for the helpful summary. A few comments:

>
What was behind the question was a paper written by Dick Crouch and me for
the LFG02 proceedings on coordination in Glue Semantics (available at
www.stanford.edu/~asudeh). What we came up with is related to the CG
approaches. However, it solves the n-ary coordination problem by using
non-linear lambda expressions in the meaning language.
>>

Here the meaning type theory is just ordinary (nonlinear)
intuitionistic propositional logic, so the meaning language (= the
proof terms for the meaning type theory) is just ordinary (nonlinear)
Church/Henkin/Gallin-style typed lambda calculus -- this is a fact
that has nothing to do especially with coordination.

>
A non-linear lamba expression is one that has more than one occurrence
of the lambda bound variable in it (e.g. \x.P(x,x)). Such lambda
expressions are allowed freely in the meaning language of Glue, but
not in the proof terms, since we assume linear logic as our proof
logic. If the last three sentences made no sense, I apologize; I just
wanted to put them in for people who might be interested.
>>

There are two different logics here, each with its own proof theory:
the linear glue logic, whose proof terms are terms of the linear
lambda calculus, and the logic whose formulas are semantic types and
whose proofs are terms of the ordinary typed lambda calculus (the
terms which are interpreted as meanings of linguistic expressions).  I
know, this is not how linguistic semanticists are used to thinking of
it, but this is really the essence of the Curry-Howard view that types
are formulas and the things that inhabit the types are (equivalence
classes of) proofs.

I point this out because most linguists first hear about Curry-Howard
in the setting of the syntax-semantics interface for categorial
grammar, either directly or indirectly via van Benthem, and emerge
with the (to put it charitably, simplistic; to put it uncharitably,
erroneous) view that the Montague-style (nonlinear) meaning terms are
the Curry-Howard proof terms for Lambek's logic of syntactic
types. They are not, though; in fact the proof terms for Lambek
calculus are terms of the "two-sided" linear lambda calculus (see
Wansing 1992).  To get from these to meaning terms, you need to
(literally) supply a translation from a linear lambda calculus to a
nonlinear one.  This translation is (categorically) equivalent in a
precise sense to Lambek's synatx-semantics interface functor (see next
paragraph).  The fact that in this translation, constants of the
linear calculus are translated into terms of the nonlinear one is the
reason why it appears from the outside that word meanings in glue
semantics are allowed to violate the general principle of linear
lambda calculus that each lambda binds a unique variable occurrence.
In the actual linear proof term, this principle is not really
violated, but in the translation, constants representing words (qua
syntactic entities) are replaced by their translations, which are
terms in the meaning lambda calculus and not subject to the that
principle.

If you handle f-structures logically too (along the lines I proposed
in an earlier message), then that logic too is nonlinear (in fact
classical), and so f-structures (including the setty ones used by Mary
and Ron in their analysis of coordination) also become terms of a
(nonlinear) classical typed lambda calculus. However, if one goes this
route, then one would probably abandon the glue logic to handle the
syntax-semantics interface, and instead treat it as a functor (in the
categorical sense, not the categorial one) from the syntactic type
theory to the semantic type theory. This is what Lambek has
consistently advocated -- see, e.g. his paper in the Oehrle, Bach, and
Wheeler volume -- though of course for him the syntactic type logic is
noncommutative linear intuitionistic, not (commutative nonlinear)
classical.

Carl