Reordering a head's dependents

Graph.reorderDependents g v σ moves the phrases of the dependents of v as whole blocks into the order a permutation σ of v and its dependents gives them; every other position keeps its place. The position permutation ranks positions by a key (the block's new rank, then the old position inside the yield of v), so it is defined on every graph and computable. On a projective tree only the head's own dependencies change length under the move, by the change in their boundary distances, so Behaghel's law of growing constituents (WordOrder.Arrangement.sum_boundaryDist_lt_iff) becomes a statement about total dependency length: when the phrases after a head grow outward, every reordering that does not is strictly longer.

Main definitions

• Graph.reorderDependents: the graph with a head's dependent phrases reordered as blocks.

Main results

• Graph.totalLength_reorderDependents_add: on a projective tree, reordering changes total dependency length exactly as it changes the head's boundary distances.
• Graph.totalLength_lt_reorderDependents_iff: Behaghel's law for graphs.

References

• [Beh09]
• [FLG20]

Blocks

def DependencyGrammar.Graph.blockHead {n : ℕ} (g : Graph n) (v x : Fin n) : ↥(g.siblings v)

g.blockHead v x is the sibling of v whose block holds x, the dependent of v whose phrase contains x, and v itself for v and for positions outside its yield.

Equations

• g.blockHead v x = match h : List.find? (fun (c : Fin n) => decide (g.Adj v c ∧ x ∈ g.yield c)) (List.finRange n) with | some c => ⟨c, ⋯⟩ | none => ⟨v, ⋯⟩

def DependencyGrammar.Graph.reorderKey {n : ℕ} (g : Graph n) (v : Fin n) (σ : Equiv.Perm ↥(g.siblings v)) (x : Fin n) : Lex (Fin n × Lex (ℕ × Fin n))

The reordered positions are ranked by this key. A position outside the yield of v keeps its place, and a position inside sorts by the new rank of its block, then by its old position.

Equations

• g.reorderKey v σ x = toLex (if x ∈ g.yield v then v else x, toLex (↑(g.siblingRank v (σ (g.blockHead v x))), x))

def DependencyGrammar.Graph.reorderRank {n : ℕ} (g : Graph n) (v : Fin n) (σ : Equiv.Perm ↥(g.siblings v)) (x : Fin n) : Fin n

The new position of x counts the positions whose key is smaller.

Equations

• g.reorderRank v σ x = ⟨{y : Fin n | g.reorderKey v σ y < g.reorderKey v σ x}.card, ⋯⟩

theorem DependencyGrammar.Graph.reorderKey_injective {n : ℕ} {g : Graph n} {v : Fin n} {σ : Equiv.Perm ↥(g.siblings v)} : Function.Injective (g.reorderKey v σ)

theorem DependencyGrammar.Graph.reorderRank_lt_of_lt {n : ℕ} {g : Graph n} {v : Fin n} {σ : Equiv.Perm ↥(g.siblings v)} {x y : Fin n} (h : g.reorderKey v σ x < g.reorderKey v σ y) : g.reorderRank v σ x < g.reorderRank v σ y

theorem DependencyGrammar.Graph.reorderRank_injective {n : ℕ} {g : Graph n} {v : Fin n} {σ : Equiv.Perm ↥(g.siblings v)} : Function.Injective (g.reorderRank v σ)

theorem DependencyGrammar.Graph.reorderRank_bijective {n : ℕ} {g : Graph n} {v : Fin n} {σ : Equiv.Perm ↥(g.siblings v)} : Function.Bijective (g.reorderRank v σ)

def DependencyGrammar.Graph.reorderPerm {n : ℕ} (g : Graph n) (v : Fin n) (σ : Equiv.Perm ↥(g.siblings v)) : Equiv.Perm (Fin n)

The position permutation that moves the blocks of v's dependents into the order σ gives them; its inverse is computable.

Equations

• g.reorderPerm v σ = { toFun := g.reorderRank v σ, invFun := Fintype.bijInv ⋯, left_inv := ⋯, right_inv := ⋯ }

def DependencyGrammar.Graph.reorderDependents {n : ℕ} (g : Graph n) (v : Fin n) (σ : Equiv.Perm ↥(g.siblings v)) : Graph n

The graph with the dependents of v reordered by σ, each phrase moving as a block.

Equations

• g.reorderDependents v σ = g.map (g.reorderPerm v σ)

@[simp]

theorem DependencyGrammar.Graph.reorderPerm_apply {n : ℕ} (g : Graph n) (v : Fin n) (σ : Equiv.Perm ↥(g.siblings v)) (x : Fin n) : (g.reorderPerm v σ) x = g.reorderRank v σ x

Total length under transport

theorem DependencyGrammar.Graph.totalLength_map_eq {n : ℕ} (g : Graph n) (π : Equiv.Perm (Fin n)) : (g.map π).totalLength = ∑ u : Fin n, ∑ w ∈ g.children u, (↑(π u)).dist ↑(π w)

Block lemmas (trees)

theorem DependencyGrammar.Graph.blockHead_spec {n : ℕ} {g : Graph n} {v : Fin n} (x : Fin n) : ↑(g.blockHead v x) = v ∨ g.Adj v ↑(g.blockHead v x) ∧ x ∈ g.yield ↑(g.blockHead v x)

theorem DependencyGrammar.Graph.blockHead_of_notMem_yield {n : ℕ} {g : Graph n} {v x : Fin n} (hx : x ∉ g.yield v) : ↑(g.blockHead v x) = v

theorem DependencyGrammar.Graph.blockHead_self {n : ℕ} {g : Graph n} {v : Fin n} (hT : g.IsTree) : ↑(g.blockHead v v) = v

theorem DependencyGrammar.Graph.blockHead_eq_of_mem_yield {n : ℕ} {g : Graph n} {v : Fin n} (hT : g.IsTree) {x c : Fin n} (hc : g.Adj v c) (hx : x ∈ g.yield c) : ↑(g.blockHead v x) = c

theorem DependencyGrammar.Graph.adj_blockHead_of_ne {n : ℕ} {g : Graph n} {v : Fin n} (hT : g.IsTree) {x : Fin n} (hx : x ∈ g.yield v) (hne : x ≠ v) : g.Adj v ↑(g.blockHead v x) ∧ x ∈ g.yield ↑(g.blockHead v x)

theorem DependencyGrammar.Graph.blockHead_eq_self_iff {n : ℕ} {g : Graph n} {v : Fin n} (hT : g.IsTree) {x : Fin n} (hx : x ∈ g.yield v) : ↑(g.blockHead v x) = v ↔ x = v

theorem DependencyGrammar.Graph.mem_yield_blockHead {n : ℕ} {g : Graph n} {v x : Fin n} (hx : x ∈ g.yield v) : x ∈ g.yield ↑(g.blockHead v x)

Projectivity: blocks are intervals in the order of their heads

theorem DependencyGrammar.Graph.lt_of_adj_of_mem_yield {n : ℕ} {g : Graph n} {v : Fin n} (hT : g.IsTree) (hP : g.IsProjective) {d x : Fin n} (hd : g.Adj v d) (hvd : v < d) (hx : x ∈ g.yield d) : v < x

A dependent after the head has its whole phrase after the head.

theorem DependencyGrammar.Graph.lt_of_adj_of_mem_yield' {n : ℕ} {g : Graph n} {v : Fin n} (hT : g.IsTree) (hP : g.IsProjective) {d x : Fin n} (hd : g.Adj v d) (hdv : d < v) (hx : x ∈ g.yield d) : x < v

theorem DependencyGrammar.Graph.lt_of_mem_yield_of_mem_yield {n : ℕ} {g : Graph n} {v : Fin n} (hT : g.IsTree) (hP : g.IsProjective) {c d y x : Fin n} (hc : g.Adj v c) (hd : g.Adj v d) (hcd : c < d) (hy : y ∈ g.yield c) (hx : x ∈ g.yield d) : y < x

The phrases of two dependents lie in the order of their heads.

theorem DependencyGrammar.Graph.lt_iff_blockHead_lt {n : ℕ} {g : Graph n} {v : Fin n} (hT : g.IsTree) (hP : g.IsProjective) {x y : Fin n} (hx : x ∈ g.yield v) (hy : y ∈ g.yield v) (hne : g.blockHead v y ≠ g.blockHead v x) : y < x ↔ ↑(g.blockHead v y) < ↑(g.blockHead v x)

Two positions of the yield of v in distinct blocks are ordered as their blocks.

The rank, decomposed

theorem DependencyGrammar.Graph.reorderKey_lt_iff_of_mem {n : ℕ} {g : Graph n} {v : Fin n} (σ : Equiv.Perm ↥(g.siblings v)) {x y : Fin n} (hx : x ∈ g.yield v) : g.reorderKey v σ y < g.reorderKey v σ x ↔ y ∉ g.yield v ∧ y < v ∨ y ∈ g.yield v ∧ g.siblingRank v (σ (g.blockHead v y)) < g.siblingRank v (σ (g.blockHead v x)) ∨ y ∈ g.yield v ∧ g.blockHead v y = g.blockHead v x ∧ y < x

theorem DependencyGrammar.Graph.reorderKey_lt_iff_of_notMem {n : ℕ} {g : Graph n} {v : Fin n} (σ : Equiv.Perm ↥(g.siblings v)) {x y : Fin n} (hx : x ∉ g.yield v) : g.reorderKey v σ y < g.reorderKey v σ x ↔ y ∉ g.yield v ∧ y < x ∨ y ∈ g.yield v ∧ v < x

The rank of a position in the yield, decomposed

theorem DependencyGrammar.Graph.reorderRank_of_notMem {n : ℕ} {g : Graph n} {v : Fin n} (σ : Equiv.Perm ↥(g.siblings v)) {x : Fin n} (hx : x ∉ g.yield v) : ↑(g.reorderRank v σ x) = {y : Fin n | y ∉ g.yield v ∧ y < x}.card + {y : Fin n | y ∈ g.yield v ∧ v < x}.card

theorem DependencyGrammar.Graph.reorderRank_of_notMem_eq {n : ℕ} {g : Graph n} {v : Fin n} (σ : Equiv.Perm ↥(g.siblings v)) {x : Fin n} (hx : x ∉ g.yield v) (τ : Equiv.Perm ↥(g.siblings v)) : g.reorderRank v σ x = g.reorderRank v τ x

Outside the yield, the rank does not depend on σ.

The identity permutation keeps every position

theorem DependencyGrammar.Graph.lt_iff_lt_of_notMem_yield {n : ℕ} {g : Graph n} {v : Fin n} (hP : g.IsProjective) {x y : Fin n} (hx : x ∈ g.yield v) (hy : y ∉ g.yield v) : y < x ↔ y < v

A position outside the yield of v is before v exactly when it is before any position of the yield.

theorem DependencyGrammar.Graph.reorderRank_one {n : ℕ} {g : Graph n} {v : Fin n} (hT : g.IsTree) (hP : g.IsProjective) (x : Fin n) : g.reorderRank v 1 x = x

theorem DependencyGrammar.Graph.reorderRank_of_notMem_yield {n : ℕ} {g : Graph n} {v : Fin n} (σ : Equiv.Perm ↥(g.siblings v)) (hT : g.IsTree) (hP : g.IsProjective) {x : Fin n} (hx : x ∉ g.yield v) : g.reorderRank v σ x = x

Transport of total dependency length

Per-arc identities

The transport theorem

Behaghel's law for graphs

theorem DependencyGrammar.Graph.totalLength_reorderDependents_add {n : ℕ} {g : Graph n} {v : Fin n} {σ : Equiv.Perm ↥(g.siblings v)} (hT : g.IsTree) (hP : g.IsProjective) (hσ : σ.support ⊆ (g.siblingArrangement v).after ⟨v, ⋯⟩) : (g.reorderDependents v σ).totalLength + ∑ c : ↥(g.siblings v), (g.siblingArrangement v).boundaryDist (fun (c : ↥(g.siblings v)) => g.phraseLength ↑c) ⟨v, ⋯⟩ c = g.totalLength + ∑ c : ↥(g.siblings v), WordOrder.Arrangement.boundaryDist (Equiv.trans σ (g.siblingArrangement v)) (fun (c : ↥(g.siblings v)) => g.phraseLength ↑c) ⟨v, ⋯⟩ c

Reordering the dependents after v changes total dependency length exactly as it changes the head's boundary distances in the sibling arrangement.

theorem DependencyGrammar.Graph.totalLength_le_reorderDependents {n : ℕ} {g : Graph n} {v : Fin n} {σ : Equiv.Perm ↥(g.siblings v)} (hT : g.IsTree) (hP : g.IsProjective) (hσ : σ.support ⊆ (g.siblingArrangement v).after ⟨v, ⋯⟩) (h : MonovaryOn (fun (c : ↥(g.siblings v)) => g.phraseLength ↑c) ⇑(g.siblingArrangement v) ↑((g.siblingArrangement v).after ⟨v, ⋯⟩)) : g.totalLength ≤ (g.reorderDependents v σ).totalLength

Behaghel's law for a projective tree. When the phrases after a head grow outward, moving them about (each as a block) cannot shorten total dependency length.

theorem DependencyGrammar.Graph.totalLength_lt_reorderDependents_iff {n : ℕ} {g : Graph n} {v : Fin n} {σ : Equiv.Perm ↥(g.siblings v)} (hT : g.IsTree) (hP : g.IsProjective) (hσ : σ.support ⊆ (g.siblingArrangement v).after ⟨v, ⋯⟩) (h : MonovaryOn (fun (c : ↥(g.siblings v)) => g.phraseLength ↑c) ⇑(g.siblingArrangement v) ↑((g.siblingArrangement v).after ⟨v, ⋯⟩)) : g.totalLength < (g.reorderDependents v σ).totalLength ↔ ¬MonovaryOn (fun (c : ↥(g.siblings v)) => g.phraseLength ↑c) ⇑(Equiv.trans σ (g.siblingArrangement v)) ↑(WordOrder.Arrangement.after (Equiv.trans σ (g.siblingArrangement v)) ⟨v, ⋯⟩)

The reordering is strictly longer exactly when it is not itself short before long.