Categorial grammar

Categorial grammar is a family of formalisms in natural language syntax which share the central assumption that syntactic constituents combine as functions and arguments. Categorial grammar posits a close relationship between the syntax and semantic composition, since it typically treats syntactic categories as corresponding to semantic types. Categorial grammars were developed in the 1930s by Kazimierz Ajdukiewicz, Yehoshua Bar-Hillel, and Joachim Lambek. It saw a surge of interest in the 1970s following the work of Richard Montague, whose Montague grammar assumed a similar view of syntax. It continues to be a major paradigm, particularly within formal semantics.
Basics.
A categorial grammar consists of two parts: a lexicon, which assigns a set of types (also called categories) to each basic symbol, and some type inference rules, which determine how the type of a string of symbols follows from the types of the constituent symbols. It has the advantage that the type inference rules can be fixed once and for all, so that the specification of a particular language grammar is entirely determined by the lexicon.
A categorial grammar shares some features with the simply typed lambda calculus.
Whereas the lambda calculus has only one function type formula_1,
a categorial grammar typically has two function types, one type which is applied on the left,
and one on the right. For example, a simple categorial grammar might have two function types formula_2 and formula_3.
The first, formula_2, is the type of a phrase that results in a phrase of type
formula_5 when followed (on the right) by a phrase of type formula_6.
The second, formula_7, is the type of a phrase that results
in a phrase of type formula_5 when preceded (on the left) by a phrase of type 
formula_6. 
The notation is based upon algebra. A fraction when multiplied by (i.e. concatenated with) its denominator yields its numerator. As concatenation is not commutative, it makes a difference whether the denominator occurs to the left or right. The concatenation must be on the same side as the denominator for it to cancel out.
The first and simplest kind of categorial grammar is called a basic categorial grammar, or sometimes an AB-grammar (after Ajdukiewicz and Bar-Hillel ).
Given a set of primitive types formula_10, let 
formula_11 be the set of types constructed from primitive types. In the basic case, this is the least set such that formula_12
and if formula_13
then formula_14.
Think of these as purely formal expressions freely generated from the primitive types; any semantics will be added later. Some authors assume a fixed infinite set of primitive types used by all grammars, but by making the primitive types part of the grammar, the whole construction is kept finite.
A basic categorial grammar is a tuple formula_15
where formula_16 is a finite set of symbols,
formula_10 is a finite set of primitive types, and formula_18.
The relation formula_19 is the lexicon, which relates types to symbols formula_20.
Since the lexicon is finite, it can be specified by listing a set of pairs like formula_21.
Such a grammar for English might have three basic types formula_22, assigning count nouns the type formula_23, complete noun phrases the type
formula_24, and sentences the type formula_25.
Then an adjective could have the type formula_26, because if it is followed by a noun then the whole phrase is a noun. 
Similarly, a determiner has the type formula_27,
because it forms a complete noun phrase when followed by a noun.
Intransitive verbs have the type formula_28, and transitive verbs the type formula_29.
Then a string of words is a sentence if it has overall type formula_25.
For example, take the string "the bad boy made that mess". Now "the" and "that" are determiners, "boy" and "mess" are nouns, "bad" is an adjective, and "made" is a transitive verb, so the lexicon is
formula_32,
formula_33,
formula_34,
formula_35,
formula_36}.
and the sequence of types in the string is
formula_37
now find functions and appropriate arguments and reduce them according to the two inference rules
formula_38 and
formula_39:
formula_40<br>
formula_41<br>
formula_42<br>
formula_43<br>
formula_44<br>
formula_45
The fact that the result is formula_25 means that the string is a sentence, while the sequence of reductions shows that it must be parsed as ((the (bad boy)) (made (that mess))).
Categorial grammars of this form (having only function application rules) are equivalent in generative capacity to context-free grammars and are thus often considered inadequate for theories of natural language syntax. Unlike CFGs, categorial grammars are lexicalized, meaning that only a small number of (mostly language-independent) rules are employed, and all other syntactic phenomena derive from the lexical entries of specific words.
Another appealing aspect of categorial grammars is that it is often easy to assign them a compositional semantics, by first assigning interpretation types to all the basic categories, and then associating all the derived categories with appropriate function types. The interpretation of any constituent is then simply the value of a function at an argument. With some modifications to handle intensionality and quantification, this approach can be used to cover a wide variety of semantic phenomena.
Lambek calculus.
A Lambek grammar is an elaboration of this idea that has a
concatenation operator for types, and several other inference rules.
Mati Pentus has shown that these still have the generative capacity of
context-free grammars.
For the Lambek calculus, there is a type concatenation
operator formula_47, so
that formula_12
and if formula_13
then formula_50.
The Lambek calculus consists of several deduction rules, which specify
how type inclusion assertions can be derived. In the following
rules, upper case roman letters stand for types, upper case Greek
letters stand for sequences of types. A sequent of the form
formula_51
can be read: a string is of type formula_52 if it consists of the concatenation
of strings of each of the types in formula_53. If a type is
interpreted as a set of strings, then the
formula_54 may be interpreted as formula_55,
that is, "includes as a subset". 
A horizontal line means that the inclusion above the line
implies the one below the line.
The process is begun by the Axiom rule, which has no antecedents and
just says that any type includes itself.
<math>
(Axiom)\quad