Continuation semantics for the Lambek–Grishin calculus

Categorial grammars in the tradition of Lambek are asymmetric: sequent statements are of the form Γ⇒A, where the succedent is a single formula A, the antecedent a structured configuration of formulas A1,…,An. The absence of structural context in the succedent makes the analysis of a number of phenomena in natural language semantics problematic. A case in point is scope construal: the different possibilities to build an interpretation for sentences containing generalized quantifiers and related expressions. In this paper, we explore a symmetric version of categorial grammar, based on work by Grishin [14]. In addition to the Lambek product, left and right division, we consider a dual family of type-forming operations: coproduct, left and right difference. Communication between the two families is established by means of structure-preserving distributivity principles. We call the resulting system LG. We present a Curry-Howard interpretation for LG derivations, based on Curien and Herbelin’s lambda mu comu calculus. We discuss continuation-passing-style (CPS) translations mapping LG derivations to proofs/terms of Intuitionistic Multiplicative Linear Logic — the categorial system LP which serves as the logic for natural language meaning assembly. We show how LG, thus interpreted, associates sentences with quantifier phrases with the appropriate range of meanings, thus overcoming the expressive limitations of asymmetric categorial grammars in this area.