Semantics

[Mark Johnson]

> On Fri, 24 May, Avery Andrews wrote:
> 
> But if a powerful `glue language' is going to be used to assemble
> meanings, why not try to do more with it, such as assemble the
> c-structures as well as the meanings?  

This has been one of my projects during my sabbatical here at RXRC in
Grenoble, and I am writing up a paper on my results.

There has been a mini-revolution in logic over the past few years
surrounding ``resource-sensitive'' or ``substructural'' logics.  This
techniques can formalize dynamic notions involving the consumption and
production of objects.

Categorial grammar has been the prime example of the use of such
resource sensitive logics in linguistics: e.g., a category S/NP
is something which _consumes_ an NP to the right to _produce_ an S.

The theory of these logics is quite beautiful, and well-surveyed in
van Benthem's recent MIT Press paperback.  Basically, there is a
hierarchy of logics determined by the amount of ``structural
sensitivity'' one allows.  

System L (Lambek categorial grammar) is towards the bottom of this
hierarchy; the ``resources'' it manipulates are organized as strings
(i.e., the order in which things occur in is significant).

System LP (a subset of linear logic) relaxes this structural
sensitivity by ignoring order; its resources are multisets or bags
(i.e., the number of times something occurs is significant, but where
it appears is not).  Systems based on LP, such as linear logic, are
natural tools to do resource accounting on structures without linear
order, such as f-structures.

System LPC (a subset of intuitionistic logic) relaxes structural
sensitivity still further by ignoring the number of times resources
appear; its resources are sets (i.e., occurence is important, but an
object can be used many times).

There is a strict inclusion between these logics: every proof in L is
also a proof in LP, and every proof in LP is also a proof in LPC.

Now, one very interesting property of LPC is that its proofs are
isomorphic to expressions in the lambda calculus (this is the
Curry-Howard Isomorphism); in fact, it is reasonable to say that its
proofs _are_ just lambda terms.  (Because of the inclusion of L and LP
in LPC, proofs in these are lambda terms as well).  

Now lambda terms are also used to denote semantic interpretations in
model-theoretic natural language semantics, and lo and behold, the
proof lambda terms given by the Curry-Howard isomorphism turn out to
be very close to the terms we want for semantic interpretation.  (Although
surprising at first, this is because the proof records how resources
are consumed and produced, which in linguistic applications is how
predicates combine with their arguments).

My own approach differs from the Dalrymple et. al. approach in that I use
the Curry-Howard isomorphism to build semantic interpretations, so I
can use a purely propositional resource logic.  Second, f-descriptions
are used directly as input to the resource logic; there is no
f-structure construction phase (hence no ``minimal f-structure''
restrictions and no non-monotonic devices).

To be honest, I haven't got as far as I would have liked; learning
about these logics took longer than I expected, and there are a lot of
options to explore in setting up the system, of which I have only
scratched the surface.

I think I have also learnt something about the role of formalization
in linguistics.  What's really important are the central linguistic
ideas.  It can be very useful to express them precisely, i.e.,
formally, but the linguistic ideas, not the formal tools, constitute
the content of a linguistic theory.  I think now that it is possible
to formalize the same linguistic ideas in many different ways.  This
does not mean that one formalization is right and the other wrong,
although the linguistic theory's authors may and should have an
intended model in mind.  (The situation is like the non-standard models
in arithemtic; while the standard interpretation of the axioms of
arithmetic is in terms of numbers and the like, there are also
non-standard models of these axioms that have a completely different
structure).  

The real question that someone like me who works with formalization
should ask is: how informative is this formalization?  

Feature structures can be used to _encode_ things like grammatical
argument structure, but the formal theory of feature structures on its
own says nothing about argument structure or subcategorization.  These
resource conscious logics are much closer to the linguistic action
here.

It seems to me that feature structures are most spectacularly
successful in describing symmetric, transitive, synchonization between
several elements; e.g., several words or phrases which agree by
sharing some feature.  In my resource-sensitive reformulation, such
agreement relationships are formalized by having one element produce
an ``agreement resource'' (e.g., a Case marking entity) that is
consumed by another agreeing element.  Thus in this approach agreement
is essentially _asymmetric_; symmetry does not come for free.
Interestingly, analyses that make crucial use of `=c' (like Avery's
famous analysis of Icelandic quirky case) become easy to state, even
though they never received a good formal treatment in feature
structure terms.

Mark Johnson

---------------------------------------------------------------------
Rank Xerox Research Centre			Tel: (33) 76 61 50 37
6, chemin de Maupertuis				     (33) 76 61 50 50
F38240 Meylan
FRANCE						Fax: (33) 76 61 50 99
---------------------------------------------------------------------