Lambek calculus

Categorial grammar is a term used for a family of formalisms in natural language syntax motivated by the principle of compositionality and organized according to the view that syntactic constituents should generally combine as functions or according to a function-argument relationship. Most versions of categorial grammar analyze sentence structure in terms of constituencies (as opposed to dependencies) and are therefore phrase structure grammars (as opposed to dependency grammars).

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 ${\displaystyle A\rightarrow B}$, 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 ${\displaystyle B/A\,\!}$ and ${\displaystyle A\backslash B}$. The first, ${\displaystyle B/A\,\!}$, is the type of a phrase that results in a phrase of type ${\displaystyle B\,\!}$ when followed (on the right) by a phrase of type ${\displaystyle A\,\!}$. The second, ${\displaystyle A\backslash B\,\!}$, is the type of a phrase that results in a phrase of type ${\displaystyle B\,\!}$ when preceded (on the left) by a phrase of type ${\displaystyle A\,\!}$.

...
Wikipedia