Displacement Calculus

Origin. Morrill, Valentín and Fadda introduced the displacement calculus D (2011), developing a line of work by Morrill from 2010. It is a conservative extension of the Lambek calculus with connectives for discontinuity. Where Lambek's calculus is the logic of concatenation, D is the logic of concatenation together with intercalation — the operation that inserts one expression into a marked position inside another. Foundation for type-logical treatments of discontinuous constituency.

Models. Expressions are tuples of strings rather than single strings. A sort-0 expression is one string; a sort-n expression is n+1 strings with n gaps between them, each gap marked by a distinguished separator. Concatenation combines sort-0 expressions; intercalation plugs an expression into a gap. Types are sorted accordingly, and every connective is typed by the sorts of its arguments, so the calculus is a family of residuated structures rather than a single one. Discontinuity is thus phonological rather than derivational: nothing moves, and a constituent is simply permitted to be a tuple.

Formalism.

Sorts: 0: continuous (strings) 1: one discontinuity (string pairs) n: n discontinuities

Sort 0 types: Standard Lambek: A • B, A \ B, A / B

Sort 1 types: A ⊙ B: discontinuous product A ↑ B: right wrap A ↓ B: left wrap

Discontinuous product: ⟨s₁, s₂⟩ : A ⊙ B s₁ and s₂ separated.

Wrap: ⟨s₁, s₂⟩ : A ↑ B s₁ "wraps around" s₂. Result: s₁ + s₂_before + s₂_after

Intercalation: ⟨s₁, s₂⟩ ⊙ t = s₁ + t + s₂ Fill the gap.

Residuation (continuous): A • B → C iff A → C / B iff B → A \ C

Residuation (discontinuous): A ⊙ B → C iff A → C ↑ B iff B → A ↓ C

The same triple, one level up: ⊙ residuates to ↑ and ↓ exactly as • residuates to / and .

Sort discipline: Every connective is typed by the sorts of its arguments. s(A • B) = s(A) + s(B) s(A ⊙ B) = s(A) + s(B) − 1 A ⊙ B is well formed only when s(A) ≥ 1.

Hypersequent: Γ ⊢ᵢ A (sort i sequent) Track discontinuities.

Linguistics: "the person... that I saw" "give... up": particle verbs Extraction: ⟨wh, gap⟩

Focusing: Structured proof search. Complexity control.

Symbols.

Symbol	Unicode	Name	Meaning
⊙	U+2299	Circled dot / Discontinuous product	Intercalation of one expression into a gap
↑	U+2191	Upwards arrow / Extract	Right residual of ⊙
↓	U+2193	Downwards arrow / Infix	Left residual of ⊙
•	U+2022	Bullet / Continuous product	Concatenation, inherited from the Lambek calculus
/	U+002F	Solidus / Over	Right residual of •
\	U+005C	Reverse solidus / Under	Left residual of •
⟨	U+27E8	Mathematical left angle bracket	Opens a string tuple
⟩	U+27E9	Mathematical right angle bracket	Closes a string tuple
⊢	U+22A2	Turnstile	Derivability; subscripted by the sort
Γ	U+0393	Gamma	A configuration of hypotheses
+	U+002B	Plus sign / Concatenation	Joining strings in the semantics
s	—	Sort function	s(A) is the number of gaps in an expression of type A
D	—	Displacement calculus	Morrill, Valentín and Fadda's system
L	—	Lambek calculus	The sort-0 fragment of D

Metatheory. Morrill, Valentín and Fadda (2011) proved cut elimination for the displacement calculus, and derivability is decidable because cut-free search on a sequent is finite: the subformula property holds and the sort discipline bounds the configurations that can occur. D is a conservative extension of the Lambek calculus — the sort-0 fragment is exactly L, so nothing new is derivable about continuous types — and the two residuation triples are structurally identical, which is what makes the extension modular rather than ad hoc. Derivability is NP-hard, since L embeds in D and Pentus proved derivability in L NP-complete. Displacement grammars generate languages that are not context-free, so the extension does increase generative capacity beyond the bound Pentus established for L, and the intended linguistic applications — cross-serial dependency, particle verbs, medial extraction, in-situ quantification — are exactly the cases where a constituent must be a tuple rather than a string.

Applies to. Type-logical categorial grammar. Discontinuous constituency: in-situ quantification, medial extraction, gapping, particle verbs, cross-serial dependency. CatLog and related parsers. Curry-Howard semantics for natural language.

Limitations. The sort discipline is a real constraint, not bookkeeping: ⊙ and its residuals are defined only when the sorts match, so a type of sort 0 has no gap to fill and cannot be intercalated, and there is no rule that raises the sort of a type. Discontinuity is bounded by the sort, so a fixed grammar admits only a fixed number of simultaneous gaps in one constituent; unbounded discontinuity would need infinitely many sorts. The extension does not restore exchange — the calculus is still ordered, and D wraps rather than permutes — so genuinely free word order remains outside it. Derivability is NP-hard by the embedding of L, so no polynomial decision procedure exists unless P = NP, and the claim of polynomial parsing that circulates in informal accounts is false for the general problem. The exact generative class of displacement grammars is not settled, so the system's position relative to the standard mildly context-sensitive classes is not fixed by a theorem.