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 for verb phrase missing object)

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

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

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

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

Symbols.

Symbol	Unicode	Name	Meaning
\	—	Under	Left residual
/	—	Over	Right residual
•	—	Product	Concatenation
⊢	U+22A2	Turnstile	Derives
NP, S	—	Categories	Syntactic types

Metatheory. Cut elimination. Decidable (polynomial). Pentus: equals CFG. Extensions: modalities, discontinuity.

Applies to. Categorial grammar. Computational linguistics. Type-logical semantics. Natural language parsing.

Limitations. Only context-free power. Limited word order handling. Extensions needed for natural language. Parsing ambiguity.