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 , so that and if then . 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 can be read: a string is of type if it consists of the concatenation of strings of each of the types in . If a type is interpreted as a set of strings, then the ← may be interpreted as ⊇, 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. The Cut rule says that inclusions can be composed. The other rules come in pairs, one pair for each type construction operator, each pair consisting of one rule for the operator in the target, one in the source, of the arrow. The name of a rule consists of the operator and an arrow, with the operator on the side of the arrow on which it occurs in the conclusion. {| class="wikitable" |- !Target !Source |- | | |- | | |- | | |} For an example, here is a derivation of "type raising", which says that . The names of rules and the substitutions used are to the right. Relation to context-free grammars Recall that a context-free grammar is a 4-tuple where is a finite set of non-terminals or variables. is a finite set of terminal symbols. is a finite set of production rules, that is, a finite relation . is the start variable. From the point of view of categorial grammars, a context-free grammar can be seen as a calculus with a set of special purpose axioms for each language, but with no type construction operators and no inference rules except