Harmonic Word Order via Dependency Length Minimization

[Dry92] [FLG20] [Gib25] [Gre63]

[Gib25] argues that dependency length minimization (DLM) explains the head-direction generalization: consistent head direction (HH or FF) keeps spine dependencies local, while mixed direction (HF or FH) forces intervening subtree material between a head and its spine dependent. For single-word (leaf) dependents the direction is irrelevant because there is no subtree to intervene.

Main declarations

• chainTDL, listSpan — abstract chain total dependency length on List Nat position sequences, with chain_tdl_ge_span (triangle inequality) and monotone_ascending_achieves_span (monotone chains hit the lower bound).
• interveningSubtreeNodes, dep_length_ge_one_plus_intervening — the structural bridge from chain TDL to projective tree topology.
• isLeaf, leaf_no_intervening — the leaf exception that licenses free direction for single-word dependents.
• harmonicHI, harmonicHF, disharmonicHF, disharmonicFH — concrete trees instantiating [Gib25]'s recursive-embedding pattern.
• harmonic_always_shorter, dlmPredictsHarmonicCheaper — the DLM prediction in the worked-example set.

Implementation notes

• Predicate-shape definitions inherit the substrate-wide Bool convention from DependencyGrammar.Basic (isLeaf, dlmPredictsHarmonicCheaper); migrating these to Prop is a directory-wide refactor.
• The foldl_* helpers in ### Chain TDL substrate are private bookkeeping for the two main chain theorems; they exist because listSpan is defined via foldl max/foldl min rather than mathlib's List.maximum?.

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]|. Monotone sequences achieve the lower bound span = max - min; non-monotone sequences strictly exceed it.

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 ℕ → Prop

A list is monotone ascending.

Equations

• DepGrammar.HarmonicOrder.isAscending [] = True
• DepGrammar.HarmonicOrder.isAscending [head] = True
• DepGrammar.HarmonicOrder.isAscending (a :: b :: rest) = (a ≤ b ∧ DepGrammar.HarmonicOrder.isAscending (b :: rest))

@[implicit_reducible]

instance DepGrammar.HarmonicOrder.instDecidablePredListNatIsAscending : DecidablePred isAscending

Equations

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

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

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

Equations

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

Chain TDL substrate (foldl helpers)

Core chain TDL theorems

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

Triangle inequality for chains: chainTDL l ≥ listSpan l.

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

A monotone-ascending chain achieves chainTDL = listSpan.

Intervening material in projective trees

The structural heart of [Gib25]'s argument: dependency length between head h and dependent d is bounded below by 1 plus the number of d's subtree members that fall between h and d in linear order.

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

All transitive descendants of idx, excluding idx itself.

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 : ℕ) : ℕ

Number of nodes from subtreeMembers t depPos that fall strictly between headPos and depPos in linear order.

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 is at least 1 plus the number of intervening subtree nodes of the dependent. Strict equality holds when d's subtree is the sole occupant of (h, d) — the harmonic-order scenario in ### Harmonic vs disharmonic trees.

Leaf (single-word) exception

A leaf dependent has no subtree, so no nodes can intervene regardless of direction. This is the formal basis for [Gib25]'s exception for single-word adjectives, demonstratives, intensifiers, and negation markers.

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 contributes zero intervening nodes for any head position.

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: a single leaf dependency has the same length regardless of direction.

Harmonic vs disharmonic trees

[Gib25]'s recursive-embedding pattern: a verb takes a clausal complement, embedded three levels deep. Head-initial (HI) and head-final (HF) consistent orders share the same TDL; mixed orders inflate it.

def DepGrammar.HarmonicOrder.harmonicHI : DepTree

Consistent head-initial (HI) tree: V₁ S₁ V₂ S₂ V₃ O₃.

Equations

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

def DepGrammar.HarmonicOrder.harmonicHF : DepTree

Consistent head-final (HF) tree: O₃ V₃ S₂ V₂ S₁ V₁ — mirror of harmonicHI.

Equations

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

def DepGrammar.HarmonicOrder.disharmonicHF : DepTree

Disharmonic HF tree: head-initial main clause, head-final embedding.

Equations

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

def DepGrammar.HarmonicOrder.disharmonicFH : DepTree

Disharmonic FH tree: head-final main clause, head-initial embedding.

Equations

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

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. Consumed by Studies/Gibson2025 and Studies/HahnDegenFutrell2021.

Equations

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