Harmonic Word Order via Dependency Length Minimization

@cite{dryer-1992} @cite{futrell-gibson-2020} @cite{gibson-2025} @cite{greenberg-1963}

@cite{gibson-2025} argues that dependency length minimization (DLM) explains the head-direction generalization: languages overwhelmingly prefer consistent head direction across construction types. The argument:

1. In recursive structures, consistent direction (HH or FF) keeps spine dependencies local — each dependent is adjacent to its head.
2. Mixed direction (HF or FH) forces intervening subtree material between a head and its spine dependent, inflating dependency lengths.
3. For single-word dependents (leaves), direction is irrelevant to DLM because there is no subtree to intervene.

Structure

• §1: Chain TDL — abstract theory over List Nat position sequences
• §2: Intervening material — connecting DLM to tree topology
• §3: Single-word exception — leaf dependents have no intervening material
• §4: Direction change cost — concrete DepTree examples (Gibson's pattern)
• §5: DLM prediction — harmonic order is cheaper

Chain Total Dependency Length

For a sequence of positions p[0], p[1],..., p[k] representing a chain of dependencies (head → dep₁ → dep₂ →...), the total dependency length is the sum of |p[i+1] - p[i]| for all consecutive pairs.

Key insight: monotone sequences (all ascending or all descending) achieve the minimum TDL = span = max - min. Non-monotone sequences must exceed the span because each direction reversal adds distance.

def DepGrammar.HarmonicOrder.chainTDL : List ℕ → ℕ

Total dependency length of a chain of positions: sum of consecutive absolute differences |p[i+1] - p[i]|.

Equations

• DepGrammar.HarmonicOrder.chainTDL [] = 0
• DepGrammar.HarmonicOrder.chainTDL [head] = 0
• DepGrammar.HarmonicOrder.chainTDL (a :: b :: rest) = max a b - min a b + DepGrammar.HarmonicOrder.chainTDL (b :: rest)

def DepGrammar.HarmonicOrder.isAscending : List ℕ → Bool

A list is monotone ascending.

Equations

• DepGrammar.HarmonicOrder.isAscending [] = true
• DepGrammar.HarmonicOrder.isAscending [head] = true
• DepGrammar.HarmonicOrder.isAscending (a :: b :: rest) = (decide (a ≤ b) && DepGrammar.HarmonicOrder.isAscending (b :: rest))

def DepGrammar.HarmonicOrder.isDescending : List ℕ → Bool

A list is monotone descending.

Equations

• DepGrammar.HarmonicOrder.isDescending [] = true
• DepGrammar.HarmonicOrder.isDescending [head] = true
• DepGrammar.HarmonicOrder.isDescending (a :: b :: rest) = (decide (a ≥ b) && DepGrammar.HarmonicOrder.isDescending (b :: rest))

def DepGrammar.HarmonicOrder.isMonotone (l : List ℕ) : Bool

A list is monotone if it is all ascending or all descending.

Equations

• DepGrammar.HarmonicOrder.isMonotone l = (DepGrammar.HarmonicOrder.isAscending l || DepGrammar.HarmonicOrder.isDescending l)

def DepGrammar.HarmonicOrder.listSpan (l : List ℕ) : ℕ

The span of a list: max - min. For a chain of k+1 positions spanning k dependencies, this is the minimum possible TDL.

Equations

• DepGrammar.HarmonicOrder.listSpan [] = 0
• DepGrammar.HarmonicOrder.listSpan l = List.foldl max 0 l - List.foldl min (List.foldl max 0 l) l

theorem DepGrammar.HarmonicOrder.chain_tdl_ge_span (l : List ℕ) : chainTDL l ≥ listSpan l

Triangle inequality for chains: total dep length ≥ span. By induction: |a-b| + span(b::rest) ≥ span(a::b::rest) reduces to arithmetic on max/min given m ≤ b ≤ M (head is between min and max of the tail).

theorem DepGrammar.HarmonicOrder.monotone_ascending_achieves_span (l : List ℕ) (h : isAscending l = true) : chainTDL l = listSpan l

Monotone (ascending) chain achieves TDL = span. For ascending lists, each step contributes exactly b - a and the span decomposes as (b - a) + span(tail).

theorem DepGrammar.HarmonicOrder.consecutive_tdl (k : ℕ) : chainTDL (List.range (k + 1)) = k

The consecutive sequence [0, 1,..., k] has chainTDL = k.

Intervening Material

The structural heart of Gibson's argument: dependency length between a head h and dependent d equals 1 + the number of subtree members of d that fall between h and d in linear order. In a projective tree, all subtree members of d are on the same side of h as d, so they may intervene.

When direction is consistent (harmonic), recursive spine dependents are adjacent to their heads. When direction is mixed (disharmonic), subtree material from one dependent intervenes between the next spine dependent and its head.

def DepGrammar.HarmonicOrder.subtreeMembers (t : DepTree) (idx : ℕ) : List ℕ

Collect all transitive descendants of a node (excluding the node itself). Uses projection from Core/Basic.lean.

Equations

• DepGrammar.HarmonicOrder.subtreeMembers t idx = List.filter (fun (x : ℕ) => x != idx) (DepGrammar.projection t.deps idx)

def DepGrammar.HarmonicOrder.interveningSubtreeNodes (t : DepTree) (headPos depPos : ℕ) : ℕ

Count nodes from subtree(d) that fall between positions h and d in linear order. These are the "intervening" nodes that inflate dependency length beyond 1.

Equations

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

theorem DepGrammar.HarmonicOrder.dep_length_ge_one_plus_intervening (t : DepTree) (d : Dependency) (hd : d ∈ t.deps) (hne : d.headIdx ≠ d.depIdx) : DependencyLength.depLength d ≥ 1 + interveningSubtreeNodes t d.headIdx d.depIdx

Dependency length ≥ 1 + intervening subtree nodes.

depLength counts ALL positions between head and dependent (= |h − d|). interveningSubtreeNodes counts only dep's subtree members in that interval. The gap is filled by siblings' subtrees placed between h and d.

The original equality depLength = 1 + interveningSubtreeNodes (@cite{gibson-2025}, Ch. 5.3) holds only when d's subtree is the SOLE occupant of the interval (h, d) — i.e., no sibling subtrees intervene. That special case is exactly the harmonic-order scenario demonstrated concretely in §4 below.

Single-Word (Leaf) Exception

When a dependent is a leaf (no children), its subtree is empty, so there are no intervening nodes regardless of direction. This is why single-word dependents (adjectives, demonstratives, intensifiers, negation markers) can freely violate the head-direction generalization without DLM cost.

def DepGrammar.HarmonicOrder.isLeaf (t : DepTree) (idx : ℕ) : Bool

A node is a leaf if it has no dependents.

Equations

• DepGrammar.HarmonicOrder.isLeaf t idx = t.deps.all fun (x : DepGrammar.Dependency) => x.headIdx != idx

theorem DepGrammar.HarmonicOrder.leaf_no_subtree_members (t : DepTree) (idx : ℕ) (h : isLeaf t idx = true) : subtreeMembers t idx = []

A leaf has no subtree members.

theorem DepGrammar.HarmonicOrder.leaf_no_intervening (t : DepTree) (headPos depPos : ℕ) (h : isLeaf t depPos = true) : interveningSubtreeNodes t headPos depPos = 0

A leaf has 0 intervening nodes for any head position.

Since leaves have no subtree, no subtree members can intervene. Direction of a leaf dependent is irrelevant to DLM.

theorem DepGrammar.HarmonicOrder.leaf_direction_irrelevant_bridge (h d : ℕ) : DependencyLength.depLength { headIdx := h, depIdx := d, depType := UD.DepRel.amod } = DependencyLength.depLength { headIdx := d, depIdx := h, depType := UD.DepRel.amod }

Bridge to single_dep_direction_irrelevant from DependencyLength.lean: a single (leaf) dependency has the same length regardless of direction. This is the formal basis for Gibson's Table 4 exceptions.

Harmonic vs Disharmonic Trees

@cite{gibson-2025} pattern: a recursive embedding where the verb takes a clausal complement. With 3 levels of embedding:

V₁ — S₁ — V₂ — S₂ — V₃ — O₃

In head-initial (HH): V₁ S₁ V₂ S₂ V₃ O₃ — each V is adjacent to its S In head-final (FF): O₃ V₃ S₂ V₂ S₁ V₁ — same TDL, mirror image In mixed (HF): V₁ S₁ S₂ V₃ O₃ V₂ — V₂ separated from V₁ by intervening material In mixed (FH): S₁ V₁ V₂ O₃ V₃ S₂ — similar inflation

We build concrete DepTrees for each and verify TDL.

def DepGrammar.HarmonicOrder.harmonicHI : DepTree

Consistent head-initial (HH) tree: V₁(0) S₁(1) V₂(2) S₂(3) V₃(4) O₃(5) Dependencies: V₁→S₁ (nsubj, 1), V₁→V₂ (ccomp, 2), V₂→S₂ (nsubj, 1), V₂→V₃ (ccomp, 2), V₃→O₃ (obj, 1)

Equations

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

def DepGrammar.HarmonicOrder.harmonicHF : DepTree

Consistent head-final (FF) tree: O₃(0) V₃(1) S₂(2) V₂(3) S₁(4) V₁(5) Mirror image of HH. Same TDL.

Equations

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

def DepGrammar.HarmonicOrder.disharmonicHF : DepTree

Disharmonic HF tree: verb-initial main clause but verb-final embedding. V₁(0) S₁(1) S₂(2) O₃(3) V₃(4) V₂(5) The ccomp V₁→V₂ now spans the entire sentence (length 5).

Equations

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

def DepGrammar.HarmonicOrder.disharmonicFH : DepTree

Disharmonic FH tree: verb-final main clause but verb-initial embedding. S₁(0) V₂(1) S₂(2) V₃(3) O₃(4) V₁(5) The ccomp V₁→V₂ again spans far.

Equations

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

theorem DepGrammar.HarmonicOrder.harmonic_hi_beats_disharmonic_hf : DependencyLength.totalDepLength harmonicHI < DependencyLength.totalDepLength disharmonicHF

Core DLM prediction: HH < HF (harmonic beats disharmonic).

theorem DepGrammar.HarmonicOrder.harmonic_hf_beats_disharmonic_fh : DependencyLength.totalDepLength harmonicHF < DependencyLength.totalDepLength disharmonicFH

Core DLM prediction: FF < FH (harmonic beats disharmonic).

theorem DepGrammar.HarmonicOrder.direction_irrelevant_consistency_matters : DependencyLength.totalDepLength harmonicHI = DependencyLength.totalDepLength harmonicHF

Direction itself doesn't matter, only consistency: HH = FF.

theorem DepGrammar.HarmonicOrder.harmonic_always_shorter : DependencyLength.totalDepLength harmonicHI < DependencyLength.totalDepLength disharmonicHF ∧ DependencyLength.totalDepLength harmonicHI < DependencyLength.totalDepLength disharmonicFH ∧ DependencyLength.totalDepLength harmonicHF < DependencyLength.totalDepLength disharmonicHF ∧ DependencyLength.totalDepLength harmonicHF < DependencyLength.totalDepLength disharmonicFH

Both harmonic orders beat both disharmonic orders.

def DepGrammar.HarmonicOrder.dlmPredictsHarmonicCheaper : Bool

DLM predicts harmonic order is cheaper.

Equations

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