Lambek Calculus

Origin. Joachim Lambek (1958). Syntactic calculus for categorial grammar. Non-commutative residuated structure. Types as syntactic categories. Foundation for type-logical grammar.

Models. Types: S (sentence), NP, N, etc. Directional implication: A\B, B/A. Product: A•B (concatenation). Derivations prove grammaticality.

Formalism.

Types (syntactic categories): A ::= atom | A\B | B/A | A•B Atoms: S, NP, N, etc.

Directional implications: A\B: "B if A on left" (e.g., NP\S for intransitive verb) B/A: "B if A on right" (e.g., S/NP, a sentence missing an NP to its right)

Sequent calculus: Γ ⊢ A where Γ is a list (order matters).

Axiom: A ⊢ A

Cut: Γ ⊢ A Δ, A, Δ' ⊢ B ────────────────────────── Δ, Γ, Δ' ⊢ B

Right rules: A, Γ ⊢ B Γ, A ⊢ B ──────── \R ──────── /R Γ ⊢ A\B Γ ⊢ B/A

A\B wants its A on the left, so the A discharged by \R sits at the left end of the premise; B/A wants its A on the right. The two rules follow the direction of the slash.

Left rules: Δ ⊢ A Γ, B, Γ' ⊢ C ─────────────────────── \L Γ, Δ, A\B, Γ' ⊢ C

Δ ⊢ A Γ, B, Γ' ⊢ C ─────────────────────── /L Γ, B/A, Δ, Γ' ⊢ C

Example derivation: "John sleeps": John : NP, sleeps : NP\S ⊢ S

Pentus theorem: Languages recognized by Lambek grammars = context-free.

Symbols.

Metatheory. Lambek (1958) proved cut elimination for the associative calculus, from which the subformula property and decidability follow, since a cut-free proof search on a fixed sequent terminates. The calculus is exactly the logic of residuation in an ordered semigroup: A → C/B, A·B → C and B → A\C are interderivable, and this triple determines the two slashes uniquely, so no further connectives are needed to axiomatize concatenation. Pentus (1993) proved that Lambek grammars generate exactly the context-free languages, settling the Chomsky conjecture of 1963 and fixing the calculus's generative capacity. Derivability is nevertheless not polynomial: Pentus (2006) proved it NP-complete, both with and without the empty antecedent, so the parsing problem for a fixed grammar is easy while the derivability problem is not. Restricted fragments are tractable — Savateev's product-free one-division fragment is polynomial. The non-associative calculus NL, where contexts are bracketed trees, has polynomial derivability (de Groote, Buszkowski) and generates exactly the context-free languages as well.

Applies to. Categorial grammar and parsing as deduction. Montague-style compositional semantics via Curry-Howard. Residuated semigroup and monoid algebra. Base for pregroup, multimodal, displacement and Lambek-Grishin calculi. Ordered resource disciplines in type systems.

Limitations. All three structural rules are absent — exchange, weakening and contraction — so a hypothesis can be neither moved, discarded nor copied, and it is the absence of exchange that forces the two implications. Generative capacity is capped at context-free by Pentus's theorem, so cross-serial dependencies and the other mildly context-sensitive phenomena are outside the calculus, which is why multimodal, displacement and Grishin extensions exist at all. The calculus proves membership of a string in a language, not a reading: derivations that differ produce different semantic terms, and the Lambek calculus does not identify spurious ambiguities, so a sequent may have exponentially many proofs with the same meaning. Associativity is a global commitment: L cannot distinguish constituent structure, while NL can but loses the ability to hypothesize a gap at an unbracketed position, and no single calculus in the family has both.

© 2026 Lingenic LLC