Maximal Incrementality in Linear Categorial Deduction

Maximal Incrementality in Linear Categorial Deduction Mark Hepple Dept. of Computer Science University of Sheffield Regent Court, Portobello Street Sheffield S1 4DP, UK hepple©dcs, shef. ac. uk Abstract Recent work has seen the emergence of a common framework for parsing categorial grammar (CG) formalisms that fall within the 'type-logical' tradition (such as the Lambek calculus and related systems), whereby some method of linear logic the- orem proving is used in combination with a system of labelling that ensures only de- ductions appropriate to the relevant gram- matical logic are allowed. The approaches realising this framework, however, have not so far addressed the task of incremental parsing -- a key issue in earlier work with 'flexible' categorial grammars. In this pa- per, the approach of (Hepple, 1996) is mod- ified to yield a linear deduction system that does allow flexible deduction and hence in- cremental processing, but that hence also suffers the problem of 'spurious ambiguity'. This problem is avoided via normalisation. 1 Introduction A key attraction of the class of formalisms known as 'flexible' categorial grammars is their compatibility with an incremental style of processing, in allow- ing sentences to be assigned analyses that are fully or primarily left-branching. Such analyses designate many initial substrings of a sentence as interpretable constituents, allowing its interpretation to be gener- ated 'on-line' as it is presented. Incremental inter- pretation has been argued to provide for efficient language processing, by allowing early filtering of implausible readings. 1 This paper is concerned with the parsing of cat- egorial formalisms that fall within the 'type-logical' 1Within the categorial field, the significance of incre- mentality has been emphasised most notably in the work of Steedman, e.g. (Steedman, 1989). tradition, whose most familiar representative is the associative Lambek calculus (Lambek, 1958). Re- cent work has seen proposals for a range of such systems, differing in their resource sensitivity (and hence, implicitly, their underlying notion of 'lin- guistic structure'), in some cases combining differ- ing resource sensitivities in one system. 2 Many of these proposals employ a 'labelled deductive sys- tem' methodology (Gabbay, 1996), whereby types in proofs are associated with labels which record proof information for use in ensuring correct inferencing. A common framework is emerging for parsing type-logical formalisms, which exploits the labelled deduction idea. Approaches within this framework employ a theorem proving method that is appropri- ate for use with linear logic, and combine it with a labelling system that restricts admitted deductions to be those of a weaker system. Crucially, linear logic stands above all of the type-logical formalisms pro- posed in the hierarchy of substructural logics, and hence linear logic deduction methods can provide a common basis for parsing all of these systems. For example, Moortgat (1992) combines a linear proof net method with labelling to provide deduction for several categorial systems. Morrill (1995) shows how types of the associative Lambek calculus may be translated to labelled implicational linear types, with deduction implemented via a version of SLD resolution. Hepple (1996) introduces a linear …

Content truncated to 500 words