Categorial grammar and type theory (Q909654)

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.