Dependency length

This file defines the total dependency length of a graph and its relabeling along a position permutation. Dependency-length minimisation claims natural languages reduce the former beyond what independent constraints predict; relabeling is the formal core of the random-reordering baselines that test the claim.

Main definitions

• Graph.totalLength is the sum of Nat.dist over all arcs.
• OberstesGesetz bounds every arc length by a threshold.
• Graph.relabel transports a graph along a position permutation; Graph.mirror is relabeling along Fin.rev.

Main results

• Graph.totalLength_relabel: relabeling along an isometry of the positions preserves total dependency length.

References

[Beh32] — Deutsche Syntax IV, source of the "Oberstes Gesetz" threshold [FLG20] — Dependency locality as an explanatory principle for word order, source of the minimisation claim and the random-reordering baselines

def DependencyGrammar.Graph.totalLength {n : ℕ} (g : Graph n) : ℕ

Total dependency length: the sum of Nat.dist over all arcs — the quantity dependency-length minimisation is about.

Equations

• g.totalLength = ∑ v : Fin n, ∑ w ∈ g.children v, (↑v).dist ↑w

theorem DependencyGrammar.Graph.totalLength_words {n : ℕ} (g : Graph n) (words' : Fin n → Morphology.Word) : { words := words', label := g.label, root := g.root }.totalLength = g.totalLength

Total dependency length reads only the arc structure, never the tokens.

def DependencyGrammar.OberstesGesetz {n : ℕ} (g : Graph n) (threshold : ℕ) : Prop

[Beh32]'s Oberstes Gesetz: every arc has length at most threshold.

Equations

• DependencyGrammar.OberstesGesetz g threshold = ∀ ⦃v w : Fin n⦄, g.Adj v w → (↑v).dist ↑w ≤ threshold

@[instance_reducible]

instance DependencyGrammar.instDecidableOberstesGesetz {n : ℕ} (g : Graph n) (k : ℕ) : Decidable (OberstesGesetz g k)

Equations

• DependencyGrammar.instDecidableOberstesGesetz g k = DependencyGrammar.instDecidableOberstesGesetz._aux_1 g k

Relabeling: same structure, different linearization

def DependencyGrammar.Graph.relabel {n : ℕ} (g : Graph n) (σ : Equiv.Perm (Fin n)) : Graph n

Transport a graph along a position permutation: arcs, tokens, and root move together, so the labeled structure is unchanged and only the linearization varies.

Equations

• g.relabel σ = { words := g.words ∘ ⇑(Equiv.symm σ), label := fun (v w : Fin n) => g.label ((Equiv.symm σ) v) ((Equiv.symm σ) w), root := σ g.root }

@[simp]

theorem DependencyGrammar.Graph.relabel_adj {n : ℕ} (g : Graph n) (σ : Equiv.Perm (Fin n)) (v w : Fin n) : (g.relabel σ).Adj v w ↔ g.Adj ((Equiv.symm σ) v) ((Equiv.symm σ) w)

def DependencyGrammar.Graph.mirror {n : ℕ} (g : Graph n) : Graph n

The head-final mirror: relabel along position reversal.

Equations

• g.mirror = g.relabel Fin.revPerm

theorem DependencyGrammar.Graph.totalLength_relabel {n : ℕ} (g : Graph n) (σ : Equiv.Perm (Fin n)) (hσ : ∀ (v w : Fin n), (↑(σ v)).dist ↑(σ w) = (↑v).dist ↑w) : (g.relabel σ).totalLength = g.totalLength

Relabeling along an isometry of the positions preserves total dependency length.

theorem Fin.dist_rev_rev {n : ℕ} (v w : Fin n) : (↑v.rev).dist ↑w.rev = (↑v).dist ↑w

Position reversal preserves Nat.dist.

theorem DependencyGrammar.Graph.totalLength_mirror {n : ℕ} (g : Graph n) : g.mirror.totalLength = g.totalLength

The mirror image of a graph has the same total dependency length — the head-final preference is the exact mirror of the head-initial one ([FLG20], examples (7)–(8)).