a bound on the size of the types and sequents that are needed. The heart of Pentus's proof is to show that there is such a finite bound. Notation The notation in this field is not standardized. The notations used in formal language theory, logic, category theory, and linguistics, conflict with each other. In logic, arrows point to the more general from the more particular, that is, to the conclusion from the hypotheses. In this article, this convention is followed, i.e. the target of the arrow is the more general (inclusive) type. In logic, arrows usually point left to right. In this article this convention is reversed for consistency with the notation of context-free grammars, where the single non-terminal symbol is always on the left. We use the symbol in a production rule as in Backus–Naur form. Some authors use an arrow, which unfortunately may point in either direction, depending on whether the grammar is thought of as generating or recognizing the language. Some authors on categorial grammars write instead of . The convention used here follows Lambek and algebra. Historical notes The basic ideas of categorial grammar date from work by Kazimierz Ajdukiewicz (in 1935) and Yehoshua Bar-Hillel (in 1953). In 1958, Joachim Lambek introduced a syntactic calculus that formalized the function type constructors along with various rules for the combination of functions. This calculus is a forerunner of linear logic in that it is a substructural logic. Montague grammar uses an ad hoc syntactic system for English that is based on the principles of categorial grammar. Although Montague's work is sometimes regarded as syntactically uninteresting, it helped to bolster interest in categorial grammar by associating it with a highly successful formal treatment of natural language semantics. More recent work in categorial grammar has focused on the improvement of syntactic coverage. One formalism that has received considerable attention in recent years is Steedman and Szabolcsi's combinatory categorial grammar, which builds on combinatory logic invented by Moses Schönfinkel and Haskell Curry. There are a number of related formalisms of this kind in linguistics, such as type logical grammar and abstract categorial grammar. Some definitions Derivation A derivation is a binary tree that encodes a proof. Parse tree A parse tree displays a derivation, showing the syntactic structure of a sentence. Functor and argument In a right (left) function application, the node of the type A\B (B/A) is called the functor,