Memoisation for Glue Language Deduction and Categorial Parsing

Memoisation for Glue Language Deduction and Categorial Parsing Mark Hepple Department of Computer Science University of Sheffield Regent Court, 211 Portobello Street Sheffield S1 4DP, UK hepple@dcs, shef. ac. uk Abstract The multiplicative fragment of linear logic has found a number of applications in computa- tional linguistics: in the "glue language" ap- proach to LFG semantics, and in the formu- lation and parsing of various categorial gram- mars. These applications call for efficient de- duction methods. Although a number of de- duction methods for multiplicative linear logic are known, none of them are tabular meth- ods, which bring a substantial efficiency gain by avoiding redundant computation (c.f. chart methods in CFG parsing): this paper presents such a method, and discusses its use in relation to the above applications. 1 Introduction The multiplicative fragment of linear logic, which includes just the linear implication (o-) and multiplicative (®) operators, has found a number of applications within linguistics and computational linguistics. Firstly, it can be used in combination with some system of la- belling (after the 'labelled deduction' method- ology of (Gabbay, 1996)) as a general method for formulating various categorial grammar sys- tems. Linear deduction methods provide a com- mon basis for parsing categorial systems formu- lated in this way. Secondly, the multiplicative fragment forms the core of the system used in work by Dalrymple and colleagues for handling the semantics of LFG derivations, providing a 'glue language' for assembling the meanings of sentences from those of words and phrases. Although there are a number of deduction methods for multiplicative linear logic, there is a notable absence of tabular methods, which, like chart parsing for CFGs, avoid redundant com- putation. Hepple (1996) presents a compilation method which allows for tabular deduction for implicational linear logic (i.e. the fragment with only o--). This paper develops that method to cover the fragment that includes the multiplic- ative. The use of this method for the applica- tions mentioned above is discussed. 2 Multiplicative Linear Logic Linear logic is a 'resource-sensitive' logic: in any deduction, each assumption ('resource') is used precisely once• The formulae of the multiplicat- ive fragment of (intuitionistic) linear logic are defined by ~" ::= A I ~'o-~" J 9 v ® ~ (A a nonempty set of atomic types). The following rules provide a natural deduction formulation: Ao--B : a B:b o-E A: (ab) [B : v] A:a o--I Ao-B : ),v.a [B: x],[C : y] B®C: b A:a A:a B:b ®E ®I A" @ • E.,~(b, a) A®B: (a ® b) The elimination (E) and introduction (I) rules for o-- correspond to steps of functional ap- plication and abstraction, respectively, as the term labelling reveals. The o--I rule dis- charges precisely one assumption (B) within the proof to which it applies. The ®I rule pairs together the premise terms, whereas ®E has a substitution like meaning. 1 Proofs that Wo--(Xo--Z), Xo--Y, Yo--Z =~ W and that Xo-Yo-Z, Y@Z =v X follow: Wo-(Xo-Z) : w Xo-Y:x Yo-Z:y [Z:z] Y: (yz) x: Xo--Z …

Content truncated to 500 words