Comments on Martin Emms’

“Some Applications of Categorial Polymorphism”

Johan van Benthem (University of Amsterdam)

This Report contains a lot of interesting material, but unfortunately it is suboptimally organised, and in a very preliminary state. Also, the technical presentation is cumbersome at times, owing to a lack of attention to the existing technical literature on categorial logics (e.g., laborious non-derivability arguments occur where a simple type-count would have sufficed). The main contribution concerns a polymorphic version of the Lambek Calculus with type variables, as a logical system driving so-called ’categorial unification grammars’. This is indeed an important and timely subject of investigation, and the author has quite a few interesting points to contribute. Such a polymorphic calculus involves a mixture of linguistic and logical concerns, which may be sorted out in the following way.

There have been several descriptive empirical arguments in favour of admitting variable polymorphism into a description of natural language (cf. Calder, Klein, Zeevat & 1987). This Report adds several considerations, mainly concerning quantification and coordination, continuing earlier discussions in the categorial literature. It seems obvious that this alternative track is worth investigating in further formal detail. Even so, the paper contains no sustained discussion of pros and cons for the variable move. For instance, the ’open-endedness’ in initial lexical categorization, which plagues standard categorial grammar, is even aggravated once variable types are admitted. Moreover, no systematic tradeoffs are studied between the ’derivational’ polymorphism provided by standard categorial grammars vis-a-vis ’variable polymorphism’. Van Benthem 1990 discusses the latter issue, while also adducing additional arguments in favour of variable types (having to do, amongst others, with learning algorithms for categorial grammars; cf. Buszkowksi & Penn 1990, Kanazawa 1993). From a logical point of view, the next obvious question is which categorial calculus would be needed to handle variable polymorphism. There are at least two issues here. Which typed terms are relevant, and which deductive system will describe their laws of combination? In the strongest possible format, one arrives at a full-fledged second-order type theory but presumably, the intended linguistic applications require less power than this. Again, there is no very sustained discussion of the options here, but the author passes on to a particular, rather powerful ’Polymorphic Lambek Calculus’. (Van Benthem 1990, 1991 propose a weaker system, being a Lambek Calculus with an added Substitution Rule, which does not allow manipulation of higher nested types.) Presumably, there is a range of possibilities here, whose systematic ’parametrization’ would be of interest. In particular, there is the question which additional type forming operations are needed, such as various conjunctions in the style of Moortgat & Morrill 1992, over and above the Lambek slashes. Next, several obvious technical questions arise. Along the lines of Lambek’s original results, there is the question of Cut Elimination and Decidability for the new calculi. For the particular calculus considered here, the former result is established in Emms & Leiss 1993 (one would like to understand its connection to Girard’s celebrated similar result for l2). The latter problem remains open (it was posed in van Benthem 1990, who notes the decidability of the related problem for Ajdukiewicz grammars, and its undecidability for intuitionistic logic and it has withstood solution so far). Moreover, the Lambek Calculus has Strong Normalization: every reduction sequence terminates (as may be seen quite easily via its proof semantics in the typed lambda calculus): how is this with the polymorphic system? In addition to the proof theory, there are obvious questions of semantics. There are well-known difficulties in providing a perspicuous modelling for second-order lambda calculus, partly because the new machinery of variable types seems to be of a combinatorial, rather than a genuinely semantic nature. This Report considers various options, extending existing semantics for standard categorial logics (’string semantics’, ’polymorphic type semantics’), ascending up to the mainstream work of Girard 1986. From a more linguistic point of view, it would be of interest to see how far one can get by using some low-level form of ’general models’ here, avoiding all more esotheric issues of self-reference. Another obvious mathematical question (which is not treated in this Report), given the initial motivation of the categorial paradigm, concerns the recognizing power of these polymorphic calculi. There has been an early conjecture that they go up to beyond context-free (Zeevat, Moortgat, around 1988), but no definite results have been published so far. What is the additional power inherent in variable types: does one get all recursively enumerable languages? Finally, one further issue raised in van Benthem 1990 might be worth repeating here. Through the use of variable types, one enters the well-known area of theorem proving with Unification and Resolution. Interestingly, there are calculi in the latter field whose rules resemble those of Categorial Unification Grammar (cf. Mints 1993). Thus, existing work on resolution theorem proving might be enlisted for the purposes of polymorphic categorial deduction. Moreover, through this connection, existing work on normal forms of deduction and typing algorithms for partially variable categories (cf. Hindley & Seldin 198x) may be brought to bear as well.

References J. van Benthem, 1990, ”Categorial Grammar Meets Unification”, Report CSLI-90-142, Center for the Study of Language and Information, Stanford University. To appear in J. Wedekind, ed, Proceedings Titisee Workshop on Unification Formalisms, Stuttgart. J. van Benthem, 1991, Language in Action. Categories, Lambdas and Dynamic Logic, North-Holland, Amsterdam.

W. Buszkowski & G. Penn, 1990, ”Categorial Grammars Determined from Linguistic Data by Unification”, Studia Logica 49, 431-454. J. Calder, E. Klein & H. Zeevat, 1987, ’An Introduction to Unification Categorial Grammar’, in N. Haddock et al., eds., Categorial Grammar, Unification Grammar and Parsing, Edinburgh Working Papers in Cognitive Science 1, Center for Cognitive Science, University of Edinburgh. M. Emms and H. Leiss, 1993, ”The Cut-Elimination Theorem for the Second-Order Lambek Calculus”, Zentrum fur Informations- und Sprachforschung (CIS), University of Munich. J-Y Girard, 1986, ’The System F of variable Types. Fifteen Years later’, Theoretical Computer Science 45, 159-192.. J. Hindley & J. Seldin, 1986, Introduction to Combinators and Lambda Calculus, Cambridge University Press, Cambridge. M. Kanazawa, 1993, ”Identification in the Limit of Categorial Grammars”, Center for the Study of Language and Information, Stanford University. G. Mints, 1993, ’Resolution Strategies for Intuitionistic Logic’, Department of Philosophy, Stanford University. M. Moortgat & G. Morrill, 1992, ’A Calculus of Headed Trees’, to appear in the Journal of Logic, Language and Information.

Institute for Logic, Language and Computation, ILLC University of Amsterdam, 30 Juni 1993