Heaviness vs. newness in constituent ordering

[AWLG00] use a corpus analysis (the Aligned-Hansard corpus: bring … to and take … into account for heavy NP shift, give for the dative alternation) and an elicitation experiment (directors instructing actors to give objects to toy animals) to disentangle two confounded predictors of English postverbal ordering: heaviness (relative word count; [Beh09]'s law of growing constituents, "end weight") and newness (given-before-new, coded with [Pri92]'s discourse-given/new distinction, the corpus's few inferables collapsed into given). Both factors independently predict ordering in both constructions (§2 corpus, §3 experiment), and §5 reads the interaction pattern as "a constraint-based system, where the strength of a constraint is greater when competing constraints are weak".

The two factors are weighted markedness constraints *HEAVY-FIRST and *NEW-FIRST over the binary ordering candidates ([GJ03]'s MaxEnt encoding of the paper's soft-constraint architecture). The harmony difference between the two orders decomposes additively into signed per-constraint preferences (score_diff_eq_components), so independence, composition, and the constraint-strength interaction are one-step consequences; a pure-heaviness and a pure-newness contrast pair witness that neither factor reduces to the other.

Phrases, orderings, and candidates

structure ArnoldEtAl2000.Phrase : Type

A constituent characterized by the two dimensions [AWLG00] measure: word count (heaviness) and discourse status (newness). Concrete syntactic structure is abstracted away — these two scalars exhaust what the paper's regressions condition on.

• wordCount : ℕ
• discourse : Features.BinaryGivenness

@[instance_reducible]

instance ArnoldEtAl2000.instDecidableEqPhrase : DecidableEq Phrase

Equations

• ArnoldEtAl2000.instDecidableEqPhrase = ArnoldEtAl2000.instDecidableEqPhrase.decEq

def ArnoldEtAl2000.instDecidableEqPhrase.decEq (x✝ x✝¹ : Phrase) : Decidable (x✝ = x✝¹)

Equations

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

@[reducible, inline]

abbrev ArnoldEtAl2000.Pair : Type

The two constituents of a binary postverbal alternation. For the dative alternation, (theme, goal); for heavy NP shift, (direct object, prepositional phrase). The constraints below are construction-neutral.

Equations

• ArnoldEtAl2000.Pair = (ArnoldEtAl2000.Phrase × ArnoldEtAl2000.Phrase)

inductive ArnoldEtAl2000.Order : Type

Which of the two constituents occupies the second (sentence-final) slot. For DA (pair = theme, goal): themeLast is the double object (give the white rabbit the carrot), goalLast the prepositional dative (give the carrot to the white rabbit). For HNPS (pair = direct object, PP): themeLast is the shifted V PP DO, goalLast the canonical V DO PP.

• themeLast : Order
• goalLast : Order

@[instance_reducible]

instance ArnoldEtAl2000.instDecidableEqOrder : DecidableEq Order

Equations

• ArnoldEtAl2000.instDecidableEqOrder x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[reducible, inline]

abbrev ArnoldEtAl2000.Candidate : Type

Equations

• ArnoldEtAl2000.Candidate = (ArnoldEtAl2000.Pair × ArnoldEtAl2000.Order)

The two constraints

def ArnoldEtAl2000.heavyFirst : Constraints.Constraint Candidate

*HEAVY-FIRST: violated when the first (verb-adjacent) constituent is strictly heavier than the second — the markedness encoding of [Beh09]'s law of growing constituents.

Equations

• ArnoldEtAl2000.heavyFirst ((th, gl), ArnoldEtAl2000.Order.themeLast) = if gl.wordCount > th.wordCount then 1 else 0
• ArnoldEtAl2000.heavyFirst ((th, gl), ArnoldEtAl2000.Order.goalLast) = if th.wordCount > gl.wordCount then 1 else 0

def ArnoldEtAl2000.newFirst : Constraints.Constraint Candidate

*NEW-FIRST: violated when the first constituent is discourse-new while the second is discourse-given — the markedness encoding of the given-before-new principle ([Pri81], [GHZ93]).

Equations

• ArnoldEtAl2000.newFirst ((th, gl), ArnoldEtAl2000.Order.themeLast) = if gl.discourse = Features.BinaryGivenness.new ∧ th.discourse = Features.BinaryGivenness.given then 1 else 0
• ArnoldEtAl2000.newFirst ((th, gl), ArnoldEtAl2000.Order.goalLast) = if th.discourse = Features.BinaryGivenness.new ∧ gl.discourse = Features.BinaryGivenness.given then 1 else 0

def ArnoldEtAl2000.con : Constraints.CON Candidate 2

The two-constraint set as a CON over the ordering candidates.

Equations

• ArnoldEtAl2000.con = ![ArnoldEtAl2000.heavyFirst, ArnoldEtAl2000.newFirst]

def ArnoldEtAl2000.gW (wH wN : ℝ) : Fin 2 → ℝ

The weight vector pairing with con: wH weights *HEAVY-FIRST, wN weights *NEW-FIRST.

Equations

• ArnoldEtAl2000.gW wH wN = ![wH, wN]

Per-constraint signed preferences

def ArnoldEtAl2000.heavyDiff (p : Pair) : ℝ

The heaviness constraint's signed preference for themeLast over goalLast on a pair: +1 when the theme (p.1) is heavier (so placing it last avoids violation), -1 when the goal (p.2) is heavier, 0 when they are equal.

Equations

• ArnoldEtAl2000.heavyDiff p = (if p.1.wordCount > p.2.wordCount then 1 else 0) - if p.2.wordCount > p.1.wordCount then 1 else 0

def ArnoldEtAl2000.newDiff (p : Pair) : ℝ

The newness constraint's signed preference for themeLast over goalLast on a pair: +1 when the theme is new and the goal given (so placing the theme last respects given-before-new), -1 in the mirror case, 0 otherwise.

Equations

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

theorem ArnoldEtAl2000.score_diff_eq_components (wH wN : ℝ) (p : Pair) : Constraints.harmonyScore con (gW wH wN) (p, Order.themeLast) - Constraints.harmonyScore con (gW wH wN) (p, Order.goalLast) = wH * heavyDiff p + wN * newDiff p

The harmony-score difference decomposes additively into per-constraint signed preferences scaled by their weights. Every prediction theorem below is a one-step consequence.

theorem ArnoldEtAl2000.heavyDiff_pos_iff {p : Pair} : 0 < heavyDiff p ↔ p.1.wordCount > p.2.wordCount

heavyDiff is positive iff the theme (p.1) is strictly heavier than the goal — i.e., *HEAVY-FIRST prefers themeLast.

theorem ArnoldEtAl2000.newDiff_pos_iff {p : Pair} : 0 < newDiff p ↔ p.1.discourse = Features.BinaryGivenness.new ∧ p.2.discourse = Features.BinaryGivenness.given

newDiff is positive iff the theme is new while the goal is given — i.e., *NEW-FIRST prefers themeLast.

Independence — the central paper claim, derived

theorem ArnoldEtAl2000.heaviness_independently_predicts {p : Pair} {wH : ℝ} (hH : 0 < wH) (h : 0 < heavyDiff p) : Constraints.harmonyDominates con (gW wH 0) (p, Order.themeLast) (p, Order.goalLast)

Heaviness independently predicts ordering. With the newness weight zeroed out, a positive heaviness weight makes the order placing the heavier constituent last strictly preferred.

theorem ArnoldEtAl2000.newness_independently_predicts {p : Pair} {wN : ℝ} (hN : 0 < wN) (h : 0 < newDiff p) : Constraints.harmonyDominates con (gW 0 wN) (p, Order.themeLast) (p, Order.goalLast)

Newness independently predicts ordering. With the heaviness weight zeroed out, a positive newness weight makes the order placing the new constituent last strictly preferred.

theorem ArnoldEtAl2000.both_factors_compose {p : Pair} {wH wN : ℝ} (hH : 0 ≤ wH) (hN : 0 ≤ wN) (hHeavy : 0 ≤ heavyDiff p) (hNew : 0 ≤ newDiff p) (hStrict : 0 < wH * heavyDiff p ∨ 0 < wN * newDiff p) : Constraints.harmonyDominates con (gW wH wN) (p, Order.themeLast) (p, Order.goalLast)

Both factors compose additively. When neither factor opposes themeLast and at least one strictly favors it, themeLast wins; no separate interaction term is stipulated.

theorem ArnoldEtAl2000.tradeoff_resolved_by_weights {p : Pair} {wH wN : ℝ} (h : 0 < wH * heavyDiff p + wN * newDiff p) : Constraints.harmonyDominates con (gW wH wN) (p, Order.themeLast) (p, Order.goalLast)

Tradeoff. When heaviness and newness conflict, the prediction depends on which side has the larger weighted contribution — the constraint-based architecture the paper argues for.

Constraint-strength interaction

In the corpus study the dative regressions had both main effects and no newness × heaviness interaction; the experiment showed one — "heaviness had the largest effect on utterances where both constituents were given" (§5). In additive harmony the pattern is immediate: when one constraint's differential is zero, the entire harmony difference is borne by the other constraint, undiluted.

theorem ArnoldEtAl2000.heaviness_dominates_when_newness_neutral (wH wN : ℝ) {p : Pair} (hN : newDiff p = 0) : Constraints.harmonyScore con (gW wH wN) (p, Order.themeLast) - Constraints.harmonyScore con (gW wH wN) (p, Order.goalLast) = wH * heavyDiff p

When the newness constraint is neutral on a pair (both constituents share givenness status), the harmony difference is exactly the weighted heaviness term.

theorem ArnoldEtAl2000.newness_dominates_when_heaviness_neutral (wH wN : ℝ) {p : Pair} (hH : heavyDiff p = 0) : Constraints.harmonyScore con (gW wH wN) (p, Order.themeLast) - Constraints.harmonyScore con (gW wH wN) (p, Order.goalLast) = wN * newDiff p

When the heaviness constraint is neutral on a pair (equal lengths), the harmony difference is exactly the weighted newness term.

Contrast pairs and non-reducibility

def ArnoldEtAl2000.heavyGoalContrast : Pair

A heavy-goal contrast: light theme, heavy goal, both new — only heaviness discriminates.

Equations

• ArnoldEtAl2000.heavyGoalContrast = ({ wordCount := 1, discourse := Features.BinaryGivenness.new }, { wordCount := 8, discourse := Features.BinaryGivenness.new })

def ArnoldEtAl2000.newThemeContrast : Pair

A pure-newness contrast in the experiment's give-frame (give the carrot to the white rabbit): lengths matched, theme new, goal given — only newness discriminates.

Equations

• ArnoldEtAl2000.newThemeContrast = ({ wordCount := 1, discourse := Features.BinaryGivenness.new }, { wordCount := 1, discourse := Features.BinaryGivenness.given })

@[simp]

theorem ArnoldEtAl2000.heavyDiff_heavyGoalContrast : heavyDiff heavyGoalContrast = -1

@[simp]

theorem ArnoldEtAl2000.newDiff_heavyGoalContrast : newDiff heavyGoalContrast = 0

@[simp]

theorem ArnoldEtAl2000.heavyDiff_newThemeContrast : heavyDiff newThemeContrast = 0

@[simp]

theorem ArnoldEtAl2000.newDiff_newThemeContrast : newDiff newThemeContrast = 1

theorem ArnoldEtAl2000.heaviness_and_newness_genuinely_independent : newDiff heavyGoalContrast = 0 ∧ heavyDiff heavyGoalContrast ≠ 0 ∧ heavyDiff newThemeContrast = 0 ∧ newDiff newThemeContrast ≠ 0

Non-reducibility witness. heavyGoalContrast activates only heaviness, newThemeContrast only newness: a theory operationalizing one factor collapses one contrast to the trivial baseline, contradicting the paper's findings.

theorem ArnoldEtAl2000.heavy_goal_predicts_goalLast : Constraints.harmonyDominates con (gW 1 0) (heavyGoalContrast, Order.goalLast) (heavyGoalContrast, Order.themeLast)

Pure-heaviness grammar predicts goal-last (heavier-last) on the heavy-goal contrast.

theorem ArnoldEtAl2000.new_theme_predicts_themeLast : Constraints.harmonyDominates con (gW 0 1) (newThemeContrast, Order.themeLast) (newThemeContrast, Order.goalLast)

Pure-newness grammar predicts theme-last (given-first) on the pure-newness contrast.