Lambek Theorem Proving and Feature Unification

LAMBEK THEOREM PROVING AND FEATURE UNIFICATION Erik-Jan van der Linden* Institute for Language Technology and Artificial Intelligence Tilburg University PO Box 90153, 5000 LE Tilburg, The Netherlands 1 ABSTRACT Feature Unification can be integrated with Lam- bek Theorem Proving in a simple and straightfor- ward way. Two principles determine all distribu- tion of features in LTP. It is not necessary to stip- ulate other principles or include category-valued features where other theories do. The structure of categories is discussed with respect to the notion of category structure of Gazdar et al. (1988). 2 INTRODUCTION A tendency in current linguistic theory is to shift the 'explanatory burden' from the syntactic com- ponent to the lexicon. Within Categorial Gram- mar (CG), this so-cailed lexicalist principle is im- plemented in a radical fashion: syntactic infor- mation is projected entirely from category struc- ture assigned to lexical items (Moortgat, 1988). A small set of rules like (1) constitutes the gram- mar. The rules reduce sequences of categories to one category. (1) X:a X\Y:b => Y:b(a) CG implements the Compositionality Principle by stipulating a correspondence between syntac- tic operations and semantic operations (Van Ben- them 1986). An approach to the analysis of natural language in CG is to view the categorial reduction system, the set of reduction rules, as a calculus, where parsing of a syntagm is an attempt to prove that * Part of the research described in this paper was carried out within the 'Categorial Parser Project' at ITI-TNO. I wish to thank the people whom I had the pleasure to coop- erate with within this project: Brigit van Berkel, Michael Moortgat and Adriaan van Paassen. Gosse Bourns, Harry Bunt, Bart Geurts, Elias Thijsse, Ton van der Wouden, and three anonymous ACL reviewers made stlmu18ting comments on earlier versions of this paper. Michael Moortgat generously supplied a copy of the interpreter described in his 1988 dissertstion it follows as a theorem from a set of axioms and inference rules. Especially by the work of Van Benthem (1986) and Moortgat (1988) this view, which we will name with Moortgat (1987a) Lam- bek Theorem Proving (LTP; Lambek, 1958), has become popular among a number of linguists. The descriptive power of LTP can be extended if unification (Shieber, 1986) is added. Several the- ories have been developed that combine catego- rial formalisms and unification based formalisms. Within Unification Categorial Grammar (UCG, Calder et al., 1988, Zeevat et al., 1986) unification "is the only operation over grammatical objects" (Calder et al. 1988, p. 83), and this includes syntactic and semantic operations. Within Cat- egorial Unification Grammar (Uszkoreit, 1986; Bouma, 1988a), reduction rules are the main op- eration over grammatical objects, but semantic operations are reformulated within the unification formalism, as properties oflexemes (Bouma et al., 1988). These formalisms thus lexicalize semantic operations. The addition of unification to the LTP formalism described in this paper maintains the rules of the syntactic and semantic calculus as primary opera- tions, and adds unification to deal with syntactic features only. We …

Content truncated to 500 words