Gibson 2025: DLM and the Head-Direction Generalization

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

[Gib25] argues that Dependency Length Minimization (DLM) explains the head-direction generalization originally documented by [Gre63] and systematized by [Dry92]: languages overwhelmingly prefer consistent (harmonic) head direction across construction types, because disharmonic order incurs higher total dependency length on recursive structures.

This file owns Gibson's quantitative argument: the WALS-derived count tables he uses (Tables 1–3, plus the Single-Word-Exceptions discussion at Table 4), the per-table harmonic-dominance theorems, the head-direction-generalization statement over those tables, and the DLM-vs-WALS consistency theorems that package the central claim. The DLM apparatus itself lives in Syntax/DependencyGrammar/Formal/HarmonicOrder.lean.

Cross-tabulation apparatus

The AlignmentCell / CrossTab 2×2 head-direction tabulation types are defined here as paper-anchored apparatus rather than substrate, since the only consumers are this paper plus the Levshina-style gradient extension (Studies/LevshinaEtAl2023.lean). They will be promoted to Features/WordOrder.lean substrate when a second paper-independent consumer materialises (e.g., a FOFC.lean, a Hawkins1983.lean, or a systematic WALS Ch 95/96/97 ingestion that needs the type at substrate level).

Substrate-derivation evidence: WALS Ch 95

fromWALSCh95 constructs a CrossTab directly from Data.WALS.F95A.allData (verb-object × adposition correlation; [DH13a] Ch 95). This is internal evidence that Gibson's hand-coded Table 1 corresponds to the substrate-derivable form: same correlation, same harmonic-dominance conclusion. Counts differ in magnitude (Gibson 981 = 454+41+14+472; WALS Ch 95 raw = 984 = 456+42+14+472, the residual ~3 absorbed in Gibson's reporting and ~158 "Other" languages excluded by Gibson). Cell pairings match exactly: hihf = HI×HF = (VO, postpositions); hfhi = HF×HI = (OV, prepositions). Studies/DryerHaspelmath2013.lean has its own aggregate-count ch95_harmonic_dominant theorem at higher stringency (>16×); chronological dependency rules prohibit DH2013 importing this file, so it is not currently wired through.

structure Gibson2025.AlignmentCell : Type

A single cell in a 2×2 head-direction cross-tabulation. dir1 and dir2 are the head directions of two construction types being correlated. The struct does not enforce that dir1 / dir2 originate from genuinely head-direction-bearing constructions; consumers carry that contract.

• 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.

@[implicit_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.

@[implicit_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)

@[implicit_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). The four cells enumerate the head-initial / head-final combinations.

• 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.

@[implicit_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)

@[implicit_reducible]

instance Gibson2025.instDecidablePredCrossTabIsHarmonicDominant : DecidablePred CrossTab.IsHarmonicDominant

Equations

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

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

All three Gibson cross-tabulations.

Equations

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

theorem Gibson2025.voAdposition_harmonic_dominant : voAdposition.IsHarmonicDominant

Table 1: harmonic (926) > disharmonic (55).

theorem Gibson2025.voSubordinator_harmonic_dominant : voSubordinator.IsHarmonicDominant

Table 2: harmonic (393) > disharmonic (63).

theorem Gibson2025.voRelativeClause_harmonic_dominant : voRelativeClause.IsHarmonicDominant

Table 3: harmonic (547) > disharmonic (118).

theorem Gibson2025.hihi_is_harmonic : voAdposition.hihi.IsHarmonic

Harmonic cells have matching directions.

theorem Gibson2025.hfhf_is_harmonic : voAdposition.hfhf.IsHarmonic

theorem Gibson2025.hihf_is_disharmonic : ¬voAdposition.hihf.IsHarmonic

Disharmonic cells have mismatched directions.

theorem Gibson2025.hfhi_is_disharmonic : ¬voAdposition.hfhi.IsHarmonic

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

The head-direction generalization: across all three of Gibson's construction-pair tables, harmonic word-order pairings dominate. The underlying observation goes back to [Gre63] and was systematized by [Dry92]; [Gib25] argues DLM explains it (consistent head direction keeps recursive spine dependencies local).

inductive Gibson2025.SingleWordException : Type

Construction types where disharmonic order is common (Gibson's Table 4).

These are cases where the dependent is typically a single word (no recursive subtree), so head direction doesn't affect DLM. Gibson's argument: DLM only cares about direction when subtrees intervene between head and dependent.

• adjN : SingleWordException

  adjective-noun: many VO languages have Adj-N (head-final order).

• demN : SingleWordException

  demonstrative-noun: many OV languages have Dem-N (head-initial order).

• intensAdj : SingleWordException

  intensifier-adjective: "very tall" is head-initial in many OV languages.

• negVerb : SingleWordException

  negator-verb: "not run" is head-initial in many OV languages.

@[implicit_reducible]

instance Gibson2025.instReprSingleWordException : Repr SingleWordException

Equations

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

def Gibson2025.instReprSingleWordException.repr : SingleWordException → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Gibson2025.instDecidableEqSingleWordException : DecidableEq SingleWordException

Equations

• Gibson2025.instDecidableEqSingleWordException x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Gibson2025.singleWordExceptions : List SingleWordException

All single-word exceptions from Gibson Table 4.

Equations

• Gibson2025.singleWordExceptions = [Gibson2025.SingleWordException.adjN, Gibson2025.SingleWordException.demN, Gibson2025.SingleWordException.intensAdj, Gibson2025.SingleWordException.negVerb]

def Gibson2025.isSingleWordDependent : SingleWordException → Prop

These exceptions all involve dependents that are typically single words (leaves in the dependency tree), not recursive phrases.

Equations

• Gibson2025.isSingleWordDependent Gibson2025.SingleWordException.adjN = True
• Gibson2025.isSingleWordDependent Gibson2025.SingleWordException.demN = True
• Gibson2025.isSingleWordDependent Gibson2025.SingleWordException.intensAdj = True
• Gibson2025.isSingleWordDependent Gibson2025.SingleWordException.negVerb = True

@[implicit_reducible]

instance Gibson2025.instDecidablePredSingleWordExceptionIsSingleWordDependent : DecidablePred isSingleWordDependent

Equations

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

theorem Gibson2025.all_exceptions_single_word (e : SingleWordException) : e ∈ singleWordExceptions → isSingleWordDependent e

def Gibson2025.walsConfirmsHarmonic (t : CrossTab) : Bool

WALS confirms harmonic order is more common, for a given table.

Equations

• Gibson2025.walsConfirmsHarmonic t = decide t.IsHarmonicDominant

def Gibson2025.dlmWalsConsistent (t : CrossTab) : Bool

Combined consistency check: DLM prediction and WALS observation agree.

Equations

• Gibson2025.dlmWalsConsistent t = (DepGrammar.HarmonicOrder.dlmPredictsHarmonicCheaper && Gibson2025.walsConfirmsHarmonic t)

theorem Gibson2025.dlm_explains_head_direction_generalization : allTables.all dlmWalsConsistent = true

For all three of Gibson's construction pairs, DLM predicts harmonic is cheaper AND WALS confirms harmonic is more common. This is [Gib25]'s central claim: DLM explains the head-direction generalization.

theorem Gibson2025.vo_adposition_consistent : dlmWalsConsistent voAdposition = true

Per-table DLM-WALS consistency theorems.

theorem Gibson2025.vo_subordinator_consistent : dlmWalsConsistent voSubordinator = true

theorem Gibson2025.vo_relative_clause_consistent : dlmWalsConsistent voRelativeClause = true

def Gibson2025.CrossTab.fromWALSCh95 : CrossTab

Build a CrossTab for WALS Ch 95 (verb-object × adposition) by counting datapoints in each of the four cells of [DH13a]'s WALS Ch 95. The same underlying correlation viewed via raw WALS counts rather than Gibson's hand-coded snapshot.

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 CrossTab is harmonic-dominant — the same fact voAdposition_harmonic_dominant proves over Gibson's hand-coded counts, restated over the WALS-derived form. The substrate-side claim is harmonicCount > disharmonicCount; the aggregate-count form in DryerHaspelmath2013.ch95_harmonic_dominant proves the stronger 16-to-1 dominance.