Dependency length

The length of a dependency is the distance in words between head and dependent. This file defines the total dependency length of a graph, transports a graph along a permutation of its positions, and defines the distance from a head to the nearest word of a dependent's yield, dependency length measured to the boundary of the dependent's phrase. On a projective tree that distance is one more than the sizes of the yields of the sibling dependents between head and dependent: it is the block measure WordOrder.Arrangement.boundaryDist with yields as blocks. Summed over the elements after a head, the block measure weighs each element's length by the number of elements farther out, so by the rearrangement inequality an order whose lengths grow outward is shortest: this is Behaghel's law of growing constituents, and its mirror image orders long before short before a final head.

Main definitions

• Graph.totalLength: the sum of Nat.dist over the arcs.
• Graph.map: a graph transported along a permutation of its positions; Graph.mirror and Graph.linearize read it in reverse and in a given order.
• Graph.yieldDist: the distance from a position to the nearest word of a yield.
• WordOrder.Arrangement.boundaryDist: the distance in words between two constituents of given lengths in an arrangement.
• Graph.siblingArrangement: a head and its dependents in the order of their positions.

Main results

• Graph.totalLength_map: transport along an isometry preserves total dependency length.
• Graph.yieldDist_eq_one_add_sum: on a projective tree, the yield distance from a head to a dependent is one more than the yield sizes of the dependents between them.
• WordOrder.Arrangement.sum_boundaryDist_after_le: Behaghel's law, no rearrangement of the elements after a head is shorter than the order whose lengths grow outward.
• Graph.sum_yieldDist_eq_sum_boundaryDist: on a projective tree a head's yield distances are the boundary distances of its sibling arrangement with phrase lengths.

References

• [Beh09]
• [FLG20]
• [FCJ18]

theorem WordOrder.Arrangement.monovaryOn_mirror_iff {α : Type u_1} {n : ℕ} {a : Arrangement α n} (ℓ : α → ℕ) {s : Set α} : MonovaryOn ℓ (⇑a.mirror) s ↔ AntivaryOn ℓ (⇑a) s

Mirroring an arrangement swaps monovariation and antivariation of a weight with rank.

theorem WordOrder.Arrangement.card_after {α : Type u_1} {n : ℕ} [Fintype α] {a : Arrangement α n} (d : α) : (a.after d).card = n - 1 - ↑(a d)

The number of elements after d is its rank from the end.

theorem WordOrder.Arrangement.apply_eq_self_of_notMem_after {α : Type u_1} {n : ℕ} [Fintype α] {a : Arrangement α n} {x : α} {σ : Equiv.Perm α} (hσ : {c : α | σ c ≠ c} ⊆ ↑(a.after x)) {c : α} (hc : c ∉ a.after x) : σ c = c

theorem WordOrder.Arrangement.mem_after_apply_of_mem {α : Type u_1} {n : ℕ} [Fintype α] {a : Arrangement α n} {x : α} {σ : Equiv.Perm α} (hσ : {c : α | σ c ≠ c} ⊆ ↑(a.after x)) {c : α} (hc : c ∈ a.after x) : σ c ∈ a.after x

theorem WordOrder.Arrangement.precedes_trans_iff_of_notMem_after {α : Type u_1} {n : ℕ} [Fintype α] {a : Arrangement α n} {x : α} {σ : Equiv.Perm α} (hσ : {c : α | σ c ≠ c} ⊆ ↑(a.after x)) {c d : α} (hc : c ∉ a.after x) : (Precedes (Equiv.trans σ a) c d ↔ a.Precedes c d) ∧ (Precedes (Equiv.trans σ a) d c ↔ a.Precedes d c)

Rearranging the elements after x keeps precedence relative to anything not after x.

theorem WordOrder.Arrangement.after_trans {α : Type u_1} {n : ℕ} [Fintype α] {a : Arrangement α n} {x : α} {σ : Equiv.Perm α} (hσ : {c : α | σ c ≠ c} ⊆ ↑(a.after x)) : after (Equiv.trans σ a) x = a.after x

Rearranging the elements after x leaves the set of them unchanged.

def WordOrder.Arrangement.boundaryDist {α : Type u_1} {n : ℕ} [Fintype α] [DecidableEq α] (a : Arrangement α n) (ℓ : α → ℕ) (x y : α) : ℕ

The distance in words between the closest boundaries of x and y when each element c is ℓ c words long, which is one more than the words of the elements between them and zero from an element to itself.

Equations

• a.boundaryDist ℓ x y = if x = y then 0 else 1 + ∑ c : α with a.Precedes x c ∧ a.Precedes c y ∨ a.Precedes y c ∧ a.Precedes c x, ℓ c

@[simp]

theorem WordOrder.Arrangement.boundaryDist_self {α : Type u_1} {n : ℕ} [Fintype α] [DecidableEq α] (a : Arrangement α n) (ℓ : α → ℕ) (x : α) : a.boundaryDist ℓ x x = 0

theorem WordOrder.Arrangement.boundaryDist_comm {α : Type u_1} {n : ℕ} [Fintype α] [DecidableEq α] (a : Arrangement α n) (ℓ : α → ℕ) (x y : α) : a.boundaryDist ℓ x y = a.boundaryDist ℓ y x

@[simp]

theorem WordOrder.Arrangement.boundaryDist_mirror {α : Type u_1} {n : ℕ} [Fintype α] [DecidableEq α] (a : Arrangement α n) (ℓ : α → ℕ) (x y : α) : a.mirror.boundaryDist ℓ x y = a.boundaryDist ℓ x y

Mirroring preserves every distance.

theorem WordOrder.Arrangement.sum_boundaryDist_after {α : Type u_1} {n : ℕ} [Fintype α] [DecidableEq α] {a : Arrangement α n} (ℓ : α → ℕ) {x : α} : ∑ c ∈ a.after x, a.boundaryDist ℓ x c = (a.after x).card + ∑ d ∈ a.after x, ℓ d * (n - 1 - ↑(a d))

Summed over the elements after x, the distances from x weigh each element's length by the number of elements farther out, which cross its words.

theorem WordOrder.Arrangement.boundaryDist_trans_of_notMem_after {α : Type u_1} {n : ℕ} [Fintype α] [DecidableEq α] {a : Arrangement α n} (ℓ : α → ℕ) {x : α} {σ : Equiv.Perm α} (hσ : {c : α | σ c ≠ c} ⊆ ↑(a.after x)) {c : α} (hc : c ∉ a.after x) : boundaryDist (Equiv.trans σ a) ℓ x c = a.boundaryDist ℓ x c

Rearranging the elements after x leaves the distance from x to anything not after it.

theorem WordOrder.Arrangement.sum_boundaryDist_after_le {α : Type u_1} {n : ℕ} [Fintype α] [DecidableEq α] {a : Arrangement α n} (ℓ : α → ℕ) {x : α} {σ : Equiv.Perm α} (hσ : {c : α | σ c ≠ c} ⊆ ↑(a.after x)) (h : MonovaryOn ℓ ⇑a ↑(a.after x)) : ∑ c ∈ a.after x, a.boundaryDist ℓ x c ≤ ∑ c ∈ after (Equiv.trans σ a) x, boundaryDist (Equiv.trans σ a) ℓ x c

Behaghel's law of growing constituents ([Beh09]). When the lengths of the elements after x grow outward (ℓ monovaries with rank, short before long), no rearrangement of them shortens the distance from x to them.

theorem WordOrder.Arrangement.sum_boundaryDist_after_lt_iff {α : Type u_1} {n : ℕ} [Fintype α] [DecidableEq α] {a : Arrangement α n} (ℓ : α → ℕ) {x : α} {σ : Equiv.Perm α} (hσ : {c : α | σ c ≠ c} ⊆ ↑(a.after x)) (h : MonovaryOn ℓ ⇑a ↑(a.after x)) : ∑ c ∈ a.after x, a.boundaryDist ℓ x c < ∑ c ∈ after (Equiv.trans σ a) x, boundaryDist (Equiv.trans σ a) ℓ x c ↔ ¬MonovaryOn ℓ ⇑(Equiv.trans σ a) ↑(after (Equiv.trans σ a) x)

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

theorem WordOrder.Arrangement.sum_boundaryDist_le {α : Type u_1} {n : ℕ} [Fintype α] [DecidableEq α] {a : Arrangement α n} (ℓ : α → ℕ) {x : α} {σ : Equiv.Perm α} (hσ : {c : α | σ c ≠ c} ⊆ ↑(a.after x)) (h : MonovaryOn ℓ ⇑a ↑(a.after x)) : ∑ c : α, a.boundaryDist ℓ x c ≤ ∑ c : α, boundaryDist (Equiv.trans σ a) ℓ x c

Over the whole head, rearranging the elements after x cannot shorten the head's measure when their lengths grow outward.

theorem WordOrder.Arrangement.sum_boundaryDist_lt_iff {α : Type u_1} {n : ℕ} [Fintype α] [DecidableEq α] {a : Arrangement α n} (ℓ : α → ℕ) {x : α} {σ : Equiv.Perm α} (hσ : {c : α | σ c ≠ c} ⊆ ↑(a.after x)) (h : MonovaryOn ℓ ⇑a ↑(a.after x)) : ∑ c : α, a.boundaryDist ℓ x c < ∑ c : α, boundaryDist (Equiv.trans σ a) ℓ x c ↔ ¬MonovaryOn ℓ ⇑(Equiv.trans σ a) ↑(after (Equiv.trans σ a) x)

Over the whole head, the rearrangement is strictly longer exactly when it is not itself short before long.

theorem WordOrder.Arrangement.sum_boundaryDist_before_le {α : Type u_1} {n : ℕ} [Fintype α] [DecidableEq α] {a : Arrangement α n} (ℓ : α → ℕ) {x : α} {σ : Equiv.Perm α} (hσ : {c : α | σ c ≠ c} ⊆ ↑(a.before x)) (h : AntivaryOn ℓ ⇑a ↑(a.before x)) : ∑ c ∈ a.before x, a.boundaryDist ℓ x c ≤ ∑ c ∈ before (Equiv.trans σ a) x, boundaryDist (Equiv.trans σ a) ℓ x c

In the mirror image, when the lengths of the elements before x grow outward (long before short), no rearrangement of them shortens the distance from x to them.

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

Total dependency length sums 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.

Transport: same structure, different linearization

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

g.map σ transports g along the position permutation σ. Arcs, tokens and root move together, so the labeled structure is unchanged and only the linearization varies.

Equations

• g.map σ = { 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.map_adj {n : ℕ} (g : Graph n) (σ : Equiv.Perm (Fin n)) (v w : Fin n) : (g.map σ).Adj v w ↔ g.Adj ((Equiv.symm σ) v) ((Equiv.symm σ) w)

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

The mirror image, transported along position reversal.

Equations

• g.mirror = g.map Fin.revPerm

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

Transport 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)).

def DependencyGrammar.Graph.linearize {n : ℕ} (g : Graph n) (order : List (Fin n)) (h : order.Perm (List.finRange n)) : Graph n

The graph read in the order order, which lists every position once. The token at position p is the token of g at order[p], arcs and root following.

Equations

• g.linearize order h = g.map ((finCongr ⋯).trans (List.Nodup.getEquivOfForallMemList order ⋯ ⋯)).symm

theorem DependencyGrammar.Graph.linearize_words {n : ℕ} (g : Graph n) (order : List (Fin n)) (h : order.Perm (List.finRange n)) (p : Fin n) : (g.linearize order h).words p = g.words (order.get (Fin.cast ⋯ p))

Arc length and the dependent's phrase

theorem DependencyGrammar.Graph.ncard_yield_le_dist {n : ℕ} (g : Graph n) {v w : Fin n} (hv : v ∉ g.yield w) (h : ∀ x ∈ g.yield w, x ∈ Set.uIcc v w) : (g.yield w).ncard ≤ (↑v).dist ↑w

An arc to the far end of the dependent's own phrase is at least as long as the phrase: when every position the dependent dominates lies between the head and the dependent, the arc's length bounds their number. Direction is free for a one-word phrase and costly for a long one.

Distance to a phrase

theorem DependencyGrammar.Graph.toFinset_yield_nonempty {n : ℕ} (g : Graph n) (w : Fin n) : (g.yield w).toFinset.Nonempty

def DependencyGrammar.Graph.yieldDist {n : ℕ} (g : Graph n) (v w : Fin n) : ℕ

The distance from v to the nearest word of the yield of w, dependency length measured to the closest boundary of the dependent's phrase.

Equations

• g.yieldDist v w = (g.yield w).toFinset.inf' ⋯ fun (x : Fin n) => (↑v).dist ↑x

theorem DependencyGrammar.Graph.yieldDist_le_dist {n : ℕ} (g : Graph n) (v w : Fin n) : g.yieldDist v w ≤ (↑v).dist ↑w

The distance to a phrase is at most the distance to its head.

theorem DependencyGrammar.Graph.yieldDist_eq_one_add_sum {n : ℕ} {g : Graph n} {v w : Fin n} (hT : g.IsTree) (hP : g.IsProjective) (h : g.Adj v w) : g.yieldDist v w = 1 + ∑ u ∈ g.children v with v < u ∧ u < w ∨ w < u ∧ u < v, (g.yield u).ncard

On a projective tree the distance from a head to the nearest word of a dependent's phrase is one more than the phrase sizes of the dependents between them.

A head's dependents as an arrangement

def DependencyGrammar.Graph.siblings {n : ℕ} (g : Graph n) (v : Fin n) : Finset (Fin n)

A head together with its dependents.

Equations

• g.siblings v = insert v (g.children v)

def DependencyGrammar.Graph.siblingRank {n : ℕ} (g : Graph n) (v : Fin n) (c : ↥(g.siblings v)) : Fin (g.siblings v).card

The rank of a sibling counts the siblings before it.

Equations

• g.siblingRank v c = ⟨{d ∈ g.siblings v | d < ↑c}.card, ⋯⟩

theorem DependencyGrammar.Graph.siblingRank_strictMono {n : ℕ} (g : Graph n) (v : Fin n) : StrictMono (g.siblingRank v)

noncomputable def DependencyGrammar.Graph.siblingArrangement {n : ℕ} (g : Graph n) (v : Fin n) : WordOrder.Arrangement (↥(g.siblings v)) (g.siblings v).card

A head and its dependents arranged by position. The inverse is classical, but Precedes reads only the rank, which the kernel reduces.

Equations

• g.siblingArrangement v = Equiv.ofBijective (g.siblingRank v) ⋯

def DependencyGrammar.Graph.phraseLength {n : ℕ} (g : Graph n) (c : Fin n) : ℕ

The phrase length of a position is the number of words of its yield.

Equations

• g.phraseLength c = (g.yield c).toFinset.card

theorem DependencyGrammar.Graph.phraseLength_eq_ncard {n : ℕ} (g : Graph n) (c : Fin n) : g.phraseLength c = (g.yield c).ncard

@[simp]

theorem DependencyGrammar.Graph.self_mem_siblings {n : ℕ} (g : Graph n) (v : Fin n) : v ∈ g.siblings v

theorem DependencyGrammar.Graph.mem_siblings_of_adj {n : ℕ} {g : Graph n} {v w : Fin n} (h : g.Adj v w) : w ∈ g.siblings v

@[simp]

theorem DependencyGrammar.Graph.siblingArrangement_precedes {n : ℕ} {g : Graph n} {v : Fin n} {c d : ↥(g.siblings v)} : (g.siblingArrangement v).Precedes c d ↔ ↑c < ↑d

theorem DependencyGrammar.Graph.yieldDist_eq_boundaryDist {n : ℕ} {g : Graph n} {v : Fin n} (hT : g.IsTree) (hP : g.IsProjective) {w : Fin n} (h : g.Adj v w) : g.yieldDist v w = (g.siblingArrangement v).boundaryDist (fun (c : ↥(g.siblings v)) => g.phraseLength ↑c) ⟨v, ⋯⟩ ⟨w, ⋯⟩

On a projective tree the yield distance from a head to a dependent is the boundary distance of the sibling arrangement with phrase lengths.

theorem DependencyGrammar.Graph.sum_yieldDist_eq_sum_boundaryDist {n : ℕ} {g : Graph n} {v : Fin n} (hT : g.IsTree) (hP : g.IsProjective) : ∑ w ∈ g.children v, g.yieldDist v w = ∑ c : ↥(g.siblings v), (g.siblingArrangement v).boundaryDist (fun (c : ↥(g.siblings v)) => g.phraseLength ↑c) ⟨v, ⋯⟩ c

The sum of a head's yield distances is the head's measure in the sibling arrangement.