Categorial Grammar - Lambek Calculus

Lambek Calculus

A Lambek grammar is an elaboration of this idea which has a concatenation operator for types, and several other inference rules. 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 as no antecedents and just says that any type includes itself.

(Axiom)\quad {{}\over X \leftarrow X}

The Cut rule says that inclusions can be composed.

(Cut) \quad {Z \leftarrow \Delta X \Delta' \qquad X \leftarrow \Gamma \over Z \leftarrow \Delta \Gamma \Delta'}

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.

Target Source
(\backslash \leftarrow) \quad {Y\leftarrow X \Gamma \over X\backslash Y\leftarrow\Gamma} (\leftarrow \backslash) \quad {Z \leftarrow \Delta Y \Delta' \qquad X\leftarrow\Gamma \over Z \leftarrow \Delta \Gamma(X\backslash Y) \Delta'}
(/\leftarrow) \quad {Y\leftarrow \Gamma X \over Y/X\leftarrow\Gamma} (\leftarrow/) \quad {Z\leftarrow \Delta Y \Delta' \qquad X\leftarrow\Gamma \over Z\leftarrow \Delta (Y/X)\Gamma \Delta'}
(\star\leftarrow) \quad {X\leftarrow \Gamma \qquad Y \leftarrow \Gamma' \over X \star Y \leftarrow \Gamma\Gamma'} (\leftarrow\star) \quad {Z\leftarrow \Delta X Y \Delta' \over Z\leftarrow \Delta (X \star Y) \Delta'}

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.

\dfrac {\dfrac{}{B \leftarrow B} \qquad \dfrac{}{A \leftarrow A} } {\dfrac {B \leftarrow (B/A), \;\; A} {(B/A)\backslash B \leftarrow A} } \qquad \begin{matrix} \mbox{(Axioms)}\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad{ }\\ {(\leftarrow/)\,\,}\\ {(\backslash\leftarrow)\,\,}\qquad\qquad\qquad{ }\\ \end{matrix}

Read more about this topic:  Categorial Grammar

Famous quotes containing the word calculus:

    “I try to make a rough music, a dance of the mind, a calculus of the emotions, a driving beat of praise out of the pain and mystery that surround me and become me. My poems are meant to make your mind get up and shout.”
    —Judith Johnson Sherwin (b. 1936)