Lambek-Grishin Calculus

Origin. Grishin (1983), Moortgat and Kurtonina. Symmetric Lambek. Both products and coproducts. Interaction principles. Foundation for symmetric categorial grammar.

Models. Residuated lattice with both operations. ⊗ and ⊕ interact. Grishin postulates. Symmetric to non-associative.

Formalism.

Two families: Product family: ⊗, , / Coproduct family: ⊕, ⟍, ⟋

Residuation (product): A ⊗ B ⊢ C iff A ⊢ C / B iff B ⊢ A \ C

Residuation (coproduct): C ⊢ A ⊕ B iff C ⟍ B ⊢ A iff A ⟋ C ⊢ B

Grishin interaction: (A ⊕ B) ⊗ C ⊢ A ⊕ (B ⊗ C) (Grishin 1) (A ⊗ B) ⊕ C ⊢ A ⊗ (B ⊕ C) (Grishin 2) Mixed distributivity.

Symmetry: − : types → types (negation) (A ⊗ B)⁻ = B⁻ ⊕ A⁻ (A / B)⁻ = B⁻ ⟍ A⁻

Linear distributivity: A ⊗ (B ⊕ C) ⊢ (A ⊗ B) ⊕ C Not full distribution.

Semantic dualization: Continuation semantics. CPS translation. Focus and polarity.

Categorial grammar: Left and right extraction. Symmetric movement. In-situ interpretation.

Symbols.

Symbol	Unicode	Name	Meaning
⊗	U+2297	Circled times / Product	Concatenation
⊕	U+2295	Circled plus / Coproduct	Dual of ⊗; not the additive disjunction of linear logic
/	U+002F	Solidus / Over	Right residual of ⊗
\	U+005C	Reverse solidus / Under	Left residual of ⊗
⟍	U+27CD	Mathematical falling diagonal / Right difference	Right co-residual of ⊕
⟋	U+27CB	Mathematical rising diagonal / Left difference	Left co-residual of ⊕
⊢	U+22A2	Turnstile	Derivability between types
−	U+2212	Minus sign	Names the dualizing map on types
⁻	U+207B	Superscript minus	Postfix dual, as in (A ⊗ B)⁻
LG	—	Lambek-Grishin calculus	The symmetric system
NL	—	Non-associative Lambek calculus	The residuation-only base LG extends

Metatheory. The two residuation triples are independent: without Grishin's principles LG is just NL and its mirror image side by side, and is conservative over each. The interaction principles are what make the system more than the sum of its halves — they are the weakest linear distributivities that let a coproduct connective pass a product connective without collapsing ⊗ and ⊕ into a distributive lattice, which is why Grishin (1983) stated them in that particular one-directional form. Cut elimination holds, and derivability is decidable: Moortgat's display and focused presentations give a terminating proof search, and Bransen (2010) proved derivability in LG NP-complete. Bernardi and Moortgat gave a continuation-passing interpretation under which the coproduct family denotes contexts rather than values, so scope construal and extraction are read off the CPS translation rather than stipulated. Melissen (2009) placed the generative capacity of LG grammars above the tree-adjoining languages — containment in LCFRS is conjectured, the only proved upper bound being decidability — so LG is strictly stronger than the context-free bound Pentus proved for L.

Applies to. Symmetric categorial grammar. Continuation semantics for quantifier scope and scope ambiguity. Type-logical accounts of extraction and displacement. Non-context-free syntactic phenomena. Bilinear and weakly distributive algebraic semantics.

Limitations. The Grishin principles are one-directional entailments, not equivalences, so the calculus has no normal form for mixed formulas and the two families remain asymmetric in what they can be moved past. Adding the converses collapses the system: with distributivity in both directions ⊗ and ⊕ become a lattice and the calculus degenerates. Structural rules are still absent — LG is non-associative and non-commutative — so associativity must be reintroduced by modalities exactly as in the multimodal Lambek family, and LG does not by itself license reassociation. Derivability is NP-complete, so no polynomial procedure exists unless P = NP, and the connective count makes proof search expensive in practice even within that bound. The generative capacity has upper and lower bounds but no exact characterization, so unlike L, whose class Pentus fixed at context-free, LG's language class is not identified with any standard family.