Gibson (2025): Syntax: A Cognitive Approach #
This file formalizes chapter 5 of [Gib25], where dependency length minimization is a
constraint on grammars: the head-direction generalization of [Gre63] and [Dry92],
that a language's head-argument orders share one direction, follows because a disharmonic order
stretches the dependencies along a recursive spine. The measure is the total dependency length
of [FMG15], illustrated on the book's (99a) (totalLength_99a), and a
head-final language reads the same structure in the mirrored order of its head-argument rules
with subjects kept before their verbs (sov_harmonic). The argument is worked through the
book's (122) and (123): every regime is one dependency structure read in a different order
(Graph.linearize), the harmonic orders are the shortest, and each mismatch of verb-complement
direction with the direction of infinitival, subordinator, adposition, or relative-clause
dependencies costs the lengths the book computes (totalLength_122, totalLength_123). The
mechanism is an arc to the far end of its own phrase (Graph.ncard_yield_le_dist), which
is why the one-word dependents of Table 5.4 need not align (single_word_free).
Implementation notes #
Arcs follow the book's chapter 3: a subordinator or infinitival marker heads its clause, an
adposition its noun phrase, and a relative clause's verb the clause, with the nearest UD label
on each arc. The book's Tables 5.1 to 5.3, WALS cross-tabulations of verb-object order with
adposition, subordinator, and relative-clause order ([DH13a]), are prose here:
raw-count dominance over atlas rows is not a theorem of the theory. The full mirror of (123)
costs the same as the English order (Graph.totalLength_mirror); the book's head-final orders
cost more only because they keep subjects before their verbs.
References #
An order is head-first or head-final, section 5.2, when every head-argument arc, that is every arc but a subject's, takes that direction.
Equations
- Gibson2025.Harmonic g d = ∀ (v w : Fin n), g.Adj v w → g.label v w ≠ some UD.DepRel.nsubj → HeadDirection.ofLT v w = d
Instances For
Equations
- One or more equations did not get rendered due to their size.
An order that is neither head-first nor head-final.
Equations
- Gibson2025.Disharmonic g = ∀ (d : HeadDirection), ¬Gibson2025.Harmonic g d
Instances For
Equations
- Gibson2025.instDecidableDisharmonic g = { decide := decide (∀ a ∈ Finset.univ, (fun (x : HeadDirection) => ¬Gibson2025.Harmonic g x) a), reflects_decide := ⋯ }
Section 5.1: the measure, on (99a) #
(99a) Mary threw away the important documents that she brought home yesterday, whose total dependency length the book computes as eighteen.
Equations
- One or more equations did not get rendered due to their size.
Instances For
(99b), the particle after the long object, where the arc to away crosses the eight words of the object.
Equations
- Gibson2025.ex99b = Gibson2025.ex99a.linearize [0, 1, 3, 4, 5, 6, 7, 8, 9, 10, 2] Gibson2025.ex99b._proof_1
Instances For
Section 5.2: the mirror rules of a verb-final language, (119) to (121) #
(119a) Lana ate pizza.
Equations
- One or more equations did not get rendered due to their size.
Instances For
(119b) Lana pizza ate.
Equations
Instances For
(120a) Lana gave pizza to Francine.
Equations
- One or more equations did not get rendered due to their size.
Instances For
(120b) Lana Francine to pizza gave.
Equations
- Gibson2025.sov120 = Gibson2025.svo120.linearize [0, 4, 3, 2, 1] Gibson2025.sov120._proof_1
Instances For
(121a) Alfred said that Lana gave pizza to Francine.
Equations
- One or more equations did not get rendered due to their size.
Instances For
(121b) Alfred Lana Francine to pizza gave that said, where each clause keeps its subject first and mirrors the rest.
Equations
- Gibson2025.sov121 = Gibson2025.svo121.linearize [0, 3, 7, 6, 5, 4, 2, 1] Gibson2025.sov121._proof_1
Instances For
The English orders are head-first and their verb-final counterparts head-final in every head-argument rule.
Section 5.3.1: verb-object and verb-complement direction, (122) #
(122) Alfred wanted to eat bananas from Hawaii, head-first: every arc is adjacent.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The head-final order with the subject next to its verb: Hawaii from bananas eat to Alfred wanted.
Equations
- Gibson2025.hf122 = Gibson2025.hi122.linearize [6, 5, 4, 3, 2, 0, 1] Gibson2025.hf122._proof_1
Instances For
Verb-object order for eat but complement-verb order for wanted: Alfred to eat bananas from Hawaii wanted.
Equations
- Gibson2025.voCompV122 = Gibson2025.hi122.linearize [0, 2, 3, 4, 5, 6, 1] Gibson2025.voCompV122._proof_1
Instances For
Object-verb order for eat but verb-complement order for wanted: Alfred wanted to bananas from Hawaii eat.
Equations
- Gibson2025.ovVComp122 = Gibson2025.hi122.linearize [0, 1, 2, 4, 5, 6, 3] Gibson2025.ovVComp122._proof_1
Instances For
The harmonic orders cost six and seven, the mismatches fifteen and eleven.
Sections 5.3.2 to 5.3.4: subordinators, adpositions, and relative clauses, (123) #
(123) Alfred said that Lana gave pizza to monkeys who wanted bananas in English order.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The head-final order with subjects first: Alfred Lana who bananas wanted monkeys to pizza gave that said.
Equations
- Gibson2025.hfSubjFirst123 = Gibson2025.en123.linearize [0, 3, 8, 10, 9, 7, 6, 5, 4, 2, 1] Gibson2025.hfSubjFirst123._proof_1
Instances For
The head-final order with subjects next to their verbs: who bananas wanted monkeys to pizza Lana gave that Alfred said.
Equations
- Gibson2025.hf123 = Gibson2025.en123.linearize [8, 10, 9, 7, 6, 5, 3, 4, 2, 0, 1] Gibson2025.hf123._proof_1
Instances For
Verb-initial but subordinator-final: that follows the clause it heads.
Equations
- Gibson2025.voSubFinal123 = Gibson2025.en123.linearize [0, 1, 3, 4, 5, 6, 7, 8, 9, 10, 2] Gibson2025.ex99b._proof_1
Instances For
Verb-final but subordinator-initial: that precedes the clause it heads.
Equations
- Gibson2025.ovSubInitial123 = Gibson2025.en123.linearize [2, 8, 10, 9, 7, 6, 5, 3, 4, 0, 1] Gibson2025.ovSubInitial123._proof_1
Instances For
Verb-initial but postpositional: to follows its noun phrase.
Equations
- Gibson2025.voPost123 = Gibson2025.en123.linearize [0, 1, 2, 3, 4, 5, 7, 8, 9, 10, 6] Gibson2025.voPost123._proof_1
Instances For
Verb-final but prepositional: to precedes its noun phrase.
Equations
- Gibson2025.ovPre123 = Gibson2025.en123.linearize [6, 8, 10, 9, 7, 5, 3, 4, 2, 0, 1] Gibson2025.ovPre123._proof_1
Instances For
Verb-initial but with the relative clause before its noun.
Equations
- Gibson2025.voRelN123 = Gibson2025.en123.linearize [0, 1, 2, 3, 4, 5, 6, 8, 9, 10, 7] Gibson2025.voRelN123._proof_1
Instances For
Verb-final but with the relative clause after its noun.
Equations
- Gibson2025.ovNRel123 = Gibson2025.en123.linearize [7, 8, 10, 9, 6, 5, 3, 4, 2, 0, 1] Gibson2025.ovNRel123._proof_1
Instances For
The English order costs thirteen and the head-final orders twenty-seven and fifteen; each mismatch costs more than its harmonic baseline.
Reversing every arc, subjects included, costs nothing, so the book's head-final orders are dearer than English only because their subjects stay before their verbs.
A subordinator at the far end of its clause, where the arc from said to that is at least as long as the nine-word clause that heads.
Section 5.3.5: one-word dependents, Table 5.4 #
very tall, an intensifier before its adjective.
Equations
- Gibson2025.intensifierFirst = DependencyGrammar.Graph.ofArcs [Morphology.Word.mk' "very" UD.UPOS.ADV, Morphology.Word.mk' "tall" UD.UPOS.ADJ] 1 [(1, 0, UD.DepRel.advmod)]
Instances For
A one-word dependent costs the same on either side of its head, since the two orders are mirror images: Table 5.4's adjective, demonstrative, intensifier, and negator orders need not align with the verb-object order.