Gibson 2025: DLM and the head-direction generalization

[Gib25] [Dry92] [Gre63] [DH13a]

[Gib25] argues that dependency length minimization explains the head-direction generalization of [Gre63] and [Dry92]: languages overwhelmingly prefer consistent (harmonic) head direction because disharmonic order stretches spine dependencies on recursive structures, while single-word dependents (his Table 4: adjective-noun, demonstrative-noun, intensifier-adjective, negator-verb) escape the pressure because direction does not affect the length of a one-word attachment. Both halves are worked examples below (harmonic_always_shorter, single_word_direction_irrelevant); the typological half is the harmonic-dominance of his WALS cross-tabulations (Tables 1–3) and of their substrate-derived counterparts (CrossTab.fromWALSCh95, CrossTab.fromWALSCh96).

The AlignmentCell/CrossTab apparatus is paper-anchored here; its other consumer is the gradient extension in Studies/LevshinaEtAl2023.lean. Gibson's hand-coded counts differ from the raw WALS chapters by a handful of languages (his reporting excludes "Other" rows); cell pairings match exactly, and the dominance conclusion is the same on both.

Cross-tabulation apparatus

structure Gibson2025.AlignmentCell : Type

A single cell in a 2×2 head-direction cross-tabulation: the head directions of the two construction types being correlated, and the language count.

• dir1 : HeadDirection
• dir2 : HeadDirection
• count : ℕ

def Gibson2025.instReprAlignmentCell.repr : AlignmentCell → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Gibson2025.instReprAlignmentCell : Repr AlignmentCell

Equations

• Gibson2025.instReprAlignmentCell = { reprPrec := Gibson2025.instReprAlignmentCell.repr }

def Gibson2025.instDecidableEqAlignmentCell.decEq (x✝ x✝¹ : AlignmentCell) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Gibson2025.instDecidableEqAlignmentCell : DecidableEq AlignmentCell

Equations

• Gibson2025.instDecidableEqAlignmentCell = Gibson2025.instDecidableEqAlignmentCell.decEq

def Gibson2025.AlignmentCell.IsHarmonic (c : AlignmentCell) : Prop

A cell is harmonic when both constructions take the same head direction.

Equations

• c.IsHarmonic = (c.dir1 = c.dir2)

@[instance_reducible]

instance Gibson2025.instDecidablePredAlignmentCellIsHarmonic : DecidablePred AlignmentCell.IsHarmonic

Equations

• Gibson2025.instDecidablePredAlignmentCellIsHarmonic c = decEq c.dir1 c.dir2

structure Gibson2025.CrossTab : Type

A 2×2 cross-tabulation of two head-direction-bearing construction types (e.g., verb-object × adposition).

• name : String
• construction1 : String
• construction2 : String
• hihi : AlignmentCell
• hihf : AlignmentCell
• hfhi : AlignmentCell
• hfhf : AlignmentCell

def Gibson2025.instReprCrossTab.repr : CrossTab → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Gibson2025.instReprCrossTab : Repr CrossTab

Equations

• Gibson2025.instReprCrossTab = { reprPrec := Gibson2025.instReprCrossTab.repr }

def Gibson2025.CrossTab.harmonicCount (t : CrossTab) : ℕ

Total count of harmonic (diagonal) cells.

Equations

• t.harmonicCount = t.hihi.count + t.hfhf.count

def Gibson2025.CrossTab.disharmonicCount (t : CrossTab) : ℕ

Total count of disharmonic (off-diagonal) cells.

Equations

• t.disharmonicCount = t.hihf.count + t.hfhi.count

def Gibson2025.CrossTab.totalCount (t : CrossTab) : ℕ

Total number of languages in the table.

Equations

• t.totalCount = t.harmonicCount + t.disharmonicCount

def Gibson2025.CrossTab.IsHarmonicDominant (t : CrossTab) : Prop

Harmonic pairings strictly outnumber disharmonic. A raw-count primitive; serious typological generalisations require sample-bias correction (cf. [Dry92]'s genus method).

Equations

• t.IsHarmonicDominant = (t.harmonicCount > t.disharmonicCount)

@[instance_reducible]

instance Gibson2025.instDecidablePredCrossTabIsHarmonicDominant : DecidablePred CrossTab.IsHarmonicDominant

Equations

• Gibson2025.instDecidablePredCrossTabIsHarmonicDominant x✝ = x✝.disharmonicCount.decLt x✝.harmonicCount

Gibson's tables

def Gibson2025.voAdposition : CrossTab

Gibson Table 1: verb-object order × adposition order (981 languages).

Equations

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

def Gibson2025.voSubordinator : CrossTab

Gibson Table 2: verb-object order × subordinator order (456 languages).

Equations

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

def Gibson2025.voRelativeClause : CrossTab

Gibson Table 3: verb-object order × relative clause order (665 languages).

Equations

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

def Gibson2025.allTables : List CrossTab

Gibson's three cross-tabulations.

Equations

• Gibson2025.allTables = [Gibson2025.voAdposition, Gibson2025.voSubordinator, Gibson2025.voRelativeClause]

theorem Gibson2025.head_direction_generalization (t : CrossTab) : t ∈ allTables → t.IsHarmonicDominant

The head-direction generalization ([Gre63], [Dry92]): harmonic pairings dominate in every one of Gibson's construction-pair tables.

The recursive-embedding worked examples

Gibson's mechanism: "thinks John knows Mary likes cats" in the four head-direction regimes. Consistent direction keeps every arc short; mixed direction stretches the spine arcs.

def Gibson2025.harmonicHI : DependencyGrammar.Graph 6

Harmonic head-initial.

Equations

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

def Gibson2025.harmonicHF : DependencyGrammar.Graph 6

Harmonic head-final (the mirror).

Equations

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

def Gibson2025.disharmonicHF : DependencyGrammar.Graph 6

Disharmonic: head-initial spine, head-final complements.

Equations

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

def Gibson2025.disharmonicFH : DependencyGrammar.Graph 6

Disharmonic: head-final spine, head-initial complements.

Equations

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

theorem Gibson2025.harmonic_always_shorter : harmonicHI.totalLength < disharmonicHF.totalLength ∧ harmonicHI.totalLength < disharmonicFH.totalLength ∧ harmonicHF.totalLength = harmonicHI.totalLength

Harmonic order is strictly cheaper in both directions, and the mirror pair costs exactly the same.

Single-word dependents escape the pressure (Gibson Table 4)

Adjective-noun, demonstrative-noun, intensifier-adjective, and negator-verb orders are frequently disharmonic; all four involve dependents that are typically single words, and a one-word attachment has the same dependency length in either direction.

def Gibson2025.intensifierFinal : DependencyGrammar.Graph 2

"very tall": single-word intensifier before its head.

Equations

• Gibson2025.intensifierFinal = DependencyGrammar.Graph.ofArcs [Morphology.Word.mk' "very" UD.UPOS.ADV, Morphology.Word.mk' "tall" UD.UPOS.ADJ] 1 [(1, 0, UD.DepRel.advmod)]

def Gibson2025.intensifierInitial : DependencyGrammar.Graph 2

"tall very": the same attachment, head-initial.

Equations

• Gibson2025.intensifierInitial = DependencyGrammar.Graph.ofArcs [Morphology.Word.mk' "tall" UD.UPOS.ADJ, Morphology.Word.mk' "very" UD.UPOS.ADV] 0 [(0, 1, UD.DepRel.advmod)]

theorem Gibson2025.single_word_direction_irrelevant : intensifierFinal.totalLength = intensifierInitial.totalLength

A single-word dependent costs the same in either direction — DLM is silent exactly where the typology tolerates disharmony.

Substrate-derived counterparts (WALS Ch 95, Ch 96)

def Gibson2025.CrossTab.fromWALSCh95 : CrossTab

Gibson's Table 1 rebuilt from Data.WALS.F95A.allData ([DH13a] Ch 95): the verb-object × adposition correlation from raw WALS counts.

Equations

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

def Gibson2025.CrossTab.fromWALSCh96 : CrossTab

Gibson's Table 3 rebuilt from Data.WALS.F96A.allData ([DH13a] Ch 96): the verb-object × relative-clause correlation from raw WALS counts. NRel is head-initial for the noun-relative construction, RelN head-final.

Equations

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

theorem Gibson2025.fromWALSCh95_harmonic_dominant : CrossTab.fromWALSCh95.IsHarmonicDominant

The substrate-derived Ch 95 table is harmonic-dominant — the same conclusion as Gibson's hand-coded Table 1.

theorem Gibson2025.fromWALSCh96_harmonic_dominant : CrossTab.fromWALSCh96.IsHarmonicDominant

The substrate-derived Ch 96 table is harmonic-dominant — the same conclusion as Gibson's hand-coded Table 3.