Chart Parsing Lambek Grammars: Modal Extensions and Incrementality

CHART PARSING LAMBEK GRAMMARS: MODAL EXTENSIONS AND INCREMENTALITY Mark Hepple Cambridge University Computer Laboratory, Cambridge, UK. Abstract This paper I describes a method for chart parsing Lam- bek grammars. The method is of particular interest in two regards. Firstly, it allows efficient processing of grammars which use necessity operators, mr extension proposed for handling locality phenomena. Secondly, the method is easily adapted to allow incremental pro- ceasing of Lambek grammars, a possibility that has hitherto been unavailable. Introduction Categorial Grammars (CGs) consist of two compo- nents: (i) a lexicon, which assigns syntactic types (plus an associated meaning) to words, (ii) a calculus which determines the set of admitted type combina- tions. The set of types (T) is defined recursivety in terms of a set of basic types (To) and a set of op- erators ({\,/} for standard bidirectional CG), as the smallest set such that (i) To C T, (ii) /f x,y E T, then x\y, x/y E T. 2 Intuitively, lexical types specify subcategorisation requirements of words, and require- ments on constituent order. We here address a partic- ular flexible CG, the (product-free) Lambek calculus (L: Lambek, 1958). The rules below provide a nat- ural deduction formulation of L (Morrill et al. 1990; Barry et al. 1991), where dots above a type represent a proof of that type. Proofs proceed from a number of initial assumptions, consisting of individual types, some of which may be "discharged" as the proof is constructed. Eact~ type in a proof is associated with a lambda expression, corresponding to its meaning. The elimination rule/E states that proofs of A/B and B may be combined to construct a proof of A. The introduction rule /l indicates that we may discharge an assumption B within a proof of A to construct a proof of A/B (square brackets indicating the assump- tion's discharge). There is a side condition on the in- troduction rules, reflecting the ordering significance of the directional sloshes. For /1 (resp. \1), the assump- t I am grateful to Esther KSnig for discussion of the paper. The work was done under a grant to the Cambridge Univer- ";ty Computer Laboratory, "Unification.based models of lexical •ccvu and incremental interpretation", SPG 893168. ~ln this notation, x/y and x\y are both functions from y into x. A convention of left association is used, Bo that, e.g. ((t~np)/pp)/np may be written s\np/pp/np. tion discharged must be the rightmost (resp. leftmost) undischarged assumption in the proof. Elimination and introduction inferences correspond semantically to steps of functional application and abstraction, re- spectively. Hypothesis rule: Elimination rules: Introduction rules: A:x i i i : A/B:/ B:x B:x A\B:/ -/E - - . \ E A:/x A:/x ... [B:x] i [B:x]i . : . A:/ A:] A/B:)tx.]'/li A\B:),x.____.....~\ I i Each proof demonstrates the po6sibility of combin- ing the types of its undischarged assumptions, in their given order, to yield the type at the bottom of the proof. The following proof of "simple forward compo- sition" illustrates the approach. a/b:= b/c:~ [c:zli …

Content truncated to 500 words