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	Product	Concatenation
⊕	U+2295	Coproduct	Alternative
/, \	—	Over/under	Right/left residual
⟍, ⟋	—	Difference	Coproduct residuals

Metatheory. Decidable. Cut elimination. Symmetric proof theory. Focusing.

Applies to. Linguistics. Extraction phenomena. Continuation semantics. Symmetric grammars.

Limitations. Complex interactions. Many connectives. Linguistic fit debated. Specialized.