Lambek Calculus and Linear Logic: Proof Nets as Parse Structures

Summary

This chapter, a large part of which is a translation of (Retoré, 1996), deals with the connection between Lambek categorial grammar and linear logic, the main objective being the presentation of proof nets which are excellent parse structures, because they identify linguistically equivalent analyses of a given sentence.

This graphical notation for proofs that are parse structures in categorial grammar is a not a mere variation for convenience. On a technical ground, it avoids the so-called spurious ambiguity problem of categorial grammars (the fact that we can find many different proofs/parse structures for what corresponds to a single analysis or lambda term). Conceptually, this proof syntax is a justification of the use of the expression parsing as deduction often associated with categorial grammar. Indeed proof nets only distinguish between proofs which correspond to different syntactic analyses.

We first give a rather complete presentation of the correspondence between the Lambek calculus and variants of multiplicative linear logic, since the Lambek calculus can be defined as non-commutative intuitionistic multiplicative linear logic without empty antecedents.

Next we define proof nets and establish their correspondence with the more traditional sequent calculus, present parsing as proof net construction and present some recent descriptions of non commutative proof nets.

As an evidence of their linguistic relevance, we explain how they provide a formal account of some performance questions, like the complexity of the processing of several intricate syntactic constructs, like center embedded relatives, garden path phenomena and preferred readings.