Categorial grammar and type theory. (English) Zbl 0695.03016

This is a survey of logical properties of categorial grammars. These are parsing devices for natural language driven by weak implicational logics lacking the usual structural rules of standard logic. There are various options, forming a Categorial Hierarchy similar to the Chomsky Hierarchy of rewrite grammars. It is shown how questions of recognizing power can be settled by proof-theoretic methods, combining general cut elimination with the use of special invariants. These calculi have a semantics through the formulas-as-types correspondence, and hence there is a matching hierarchy of fragments of lambda calculus. It is shown how various model-theoretic properties from linguistic and logical semantics (such as Boolean monotonicity) can be formulated here, with preservation theorems changing across-fragments. Finally, the resulting theory is related to more procedurally oriented dynamic logics, such as linear logic.
Reviewer: J.van Benthem


03B65 Logic of natural languages
03B40 Combinatory logic and lambda calculus
68Q45 Formal languages and automata
03F05 Cut-elimination and normal-form theorems
Full Text: DOI