Stanojević & Steedman 2021: Formal Basis of a Language Universal

Formalisation of the central result of [SS21]: over a natural order of dominance — a chain of first-order categories X₁|X₂, X₂|X₃, …, Xₙ|Xₙ₊₁, each realizable with either slash direction — CCG derives all and only the separable permutations of the canonical linearization. The two excluded four-element patterns, 2413 and 3142, are exactly the noun-phrase and verb-cluster orders unattested in the typological record ([SS21] §1, after Cinque 2005), so the combinatorics of CCG is proposed as the formal basis of the universal.

The dominance chain is realized as a Grammar.multimodal lexicon over atoms ℕ (word i carries both Xᵢ/Xᵢ₊₁ and Xᵢ\Xᵢ₊₁; the paper's order-free | is this two-entry realization), and separable permutations are defined by the separating-tree characterization of Bose, Buss & Lubiw (the paper's (17)) as an inductive predicate: a singleton, or a split into contiguous parts in original (pos) or inverted (neg) order.

Main statements

• derives_of_sepPerm — completeness (the paper's Lemma 1–Lemma 3 / Theorem 2): every separable permutation of a span is derivable, at both slashings of the span category.
• sepPerm_of_derives — soundness (Theorem 1): everything derivable over the NOD grammar is a span category over a separable permutation. Application and second-order composition provably never fire over a first-order chain.
• derives_iff_sepPerm — the universal: derivability at a span category is separability.

Implementation notes

The Schröder-number count (Theorem 3) and the 22-of-24 four-element instance with its typological grounding are not yet formalised; they need a decidability instance for SepPerm.

def StanojevicSteedman2021.tok (i : ℕ) : String

The word token of position i in the dominance chain.

Equations

• StanojevicSteedman2021.tok i = toString i

def StanojevicSteedman2021.fwd (i : ℕ) : CCG.Cat ℕ

The forward realization of chain position i: Xᵢ/Xᵢ₊₁.

Equations

• StanojevicSteedman2021.fwd i = (CCG.Cat.atom i).rslash CCG.Modality.dot (CCG.Cat.atom (i + 1))

def StanojevicSteedman2021.bwd (i : ℕ) : CCG.Cat ℕ

The backward realization of chain position i: Xᵢ\Xᵢ₊₁.

Equations

• StanojevicSteedman2021.bwd i = (CCG.Cat.atom i).lslash CCG.Modality.dot (CCG.Cat.atom (i + 1))

def StanojevicSteedman2021.nodLexicon (n : ℕ) : List (String × CCG.Cat ℕ)

The natural-order-of-dominance lexicon over n words: each position carries both slash realizations of its chain category — the paper's order-free |.

Equations

• One or more equations did not get rendered due to their size.

def StanojevicSteedman2021.nodGrammar (n : ℕ) : CCG.Grammar ℕ

The NOD grammar: the multimodal (universal-rule) grammar over the chain lexicon. The start atom plays no role in the span-level claims.

Equations

• StanojevicSteedman2021.nodGrammar n = CCG.Grammar.multimodal (StanojevicSteedman2021.nodLexicon n) 1

theorem StanojevicSteedman2021.mem_nodLexicon {n m : ℕ} (h1 : 1 ≤ m) (hn : m ≤ n) : (tok m, fwd m) ∈ nodLexicon n ∧ (tok m, bwd m) ∈ nodLexicon n

inductive StanojevicSteedman2021.SepPerm : ℕ → ℕ → List ℕ → Prop

Separable permutations of the span i…j, by the separating-tree characterization ([SS21] (17)): a singleton, or a split of the span into two contiguous parts, concatenated in original (pos) or inverted (neg) order.

• single (i : ℕ) : SepPerm i i [i]

  A single word is a separable permutation of its own span.

• pos {i j k : ℕ} {u v : List ℕ} : SepPerm i j u → SepPerm (j + 1) k v → SepPerm i k (u ++ v)

  Contiguous parts in canonical order.

• neg {i j k : ℕ} {u v : List ℕ} : SepPerm i j u → SepPerm (j + 1) k v → SepPerm i k (v ++ u)

  Contiguous parts in inverted order.

theorem StanojevicSteedman2021.SepPerm.le {i j : ℕ} {l : List ℕ} (h : SepPerm i j l) : i ≤ j

Completeness

Every separable permutation of the span i…j is derivable at both slashings of the span category Xᵢ|Xⱼ₊₁ — the paper's Lemmas 1–3 in one induction: pos splits combine by (possibly crossing) forward composition, neg splits by backward composition, and the strengthened both-slashes hypothesis feeds the harmonic and crossing cases alike.

theorem StanojevicSteedman2021.derives_of_sepPerm {n i j : ℕ} {l : List ℕ} (h1 : 1 ≤ i) (hn : j ≤ n) (h : SepPerm i j l) : (nodGrammar n).Derives ((CCG.Cat.atom i).rslash CCG.Modality.dot (CCG.Cat.atom (j + 1))) (List.map tok l) ∧ (nodGrammar n).Derives ((CCG.Cat.atom i).lslash CCG.Modality.dot (CCG.Cat.atom (j + 1))) (List.map tok l)

Soundness

The rule induction: everything derivable over the NOD grammar is a span category Xᵢ|Xⱼ₊₁ over a separable permutation of i…j. All derivable categories are first-order, so application (which would need an atomic secondary) and second-order composition (which would need a second-order secondary) provably never fire.

theorem StanojevicSteedman2021.sepPerm_of_derives {n : ℕ} {c : CCG.Cat ℕ} {w : List String} (h : (nodGrammar n).Derives c w) : ∃ (i : ℕ) (j : ℕ) (l : List ℕ), 1 ≤ i ∧ j ≤ n ∧ SepPerm i j l ∧ w = List.map tok l ∧ (c = (CCG.Cat.atom i).rslash CCG.Modality.dot (CCG.Cat.atom (j + 1)) ∨ c = (CCG.Cat.atom i).lslash CCG.Modality.dot (CCG.Cat.atom (j + 1)))

The universal

theorem StanojevicSteedman2021.derives_fwd_iff {n i j : ℕ} {w : List String} (h1 : 1 ≤ i) (hn : j ≤ n) : (nodGrammar n).Derives ((CCG.Cat.atom i).rslash CCG.Modality.dot (CCG.Cat.atom (j + 1))) w ↔ ∃ (l : List ℕ), SepPerm i j l ∧ w = List.map tok l

CCG derives exactly the separable permutations ([SS21], Theorems 1 and 2), at the forward slashing of the span category.

theorem StanojevicSteedman2021.derives_bwd_iff {n i j : ℕ} {w : List String} (h1 : 1 ≤ i) (hn : j ≤ n) : (nodGrammar n).Derives ((CCG.Cat.atom i).lslash CCG.Modality.dot (CCG.Cat.atom (j + 1))) w ↔ ∃ (l : List ℕ), SepPerm i j l ∧ w = List.map tok l

The mirror of derives_fwd_iff, at the backward slashing.