Sprouse, Wagers and Phillips (2012): A Test of the Relation Between Working-Memory Capacity and Syntactic Island Effects

This file formalizes the logic of [SWP12]'s test of the resource-limitation theory of island effects. An island effect is defined factorially, over the four sentences that cross the presence of an island structure with the position of the gap: it is the superadditive interaction, the drop in acceptability from combining a long-distance dependency with an island structure exceeding the sum of the drops for each alone, and it is measured by the differences-in-differences score (dd, superadditive_iff_dd_pos). The simplest reductionist theory, on which a dependency cost and a structure cost add, predicts additivity and so no island effect (dd_linear). The resource-limitation theory of [KK93] adds an overload penalty when the two processes, deployed simultaneously, exceed a limited capacity, so its interaction is the penalty (dd_resourceLimitation), decreasing in capacity and vanishing once capacity suffices (dd_resourceLimitation_antitone, dd_resourceLimitation_eq_zero); a grammatical theory penalizes the island-violating sentence alone, so its interaction is the constraint's penalty whatever the capacity (dd_grammatical). The two theories part on whether the interaction covaries with working-memory capacity across speakers, the prediction the paper tests.

Implementation notes

Ratings are values in an ordered field, one per cell of the design, as for a speaker's mean ratings; the score of the paper's (8) is the interaction contrast, and the linking hypothesis that costs lower acceptability is the sign convention of the models. The overload penalty is any function of capacity, with the theory's assumptions, that it is nonnegative, decreasing in capacity, and zero when capacity covers both costs, as hypotheses. The two experiments, over three hundred speakers on four island types, with seven-point and magnitude-estimation ratings and serial-recall and n-back measures of capacity, found no relation between capacity and the interaction and no structure cost for complex NP and subject islands; the results and their resampling analyses are not formalized.

References

• [SWP12]
• [KK93]
• [HS10]
• [Spr07]

inductive SprouseEtAl2012.Structure : Type

The structure factor: whether the sentence contains an island structure.

• nonisland : Structure
• island : Structure

@[instance_reducible]

instance SprouseEtAl2012.instDecidableEqStructure : DecidableEq Structure

Equations

• SprouseEtAl2012.instDecidableEqStructure x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def SprouseEtAl2012.instReprStructure.repr : Structure → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance SprouseEtAl2012.instReprStructure : Repr Structure

Equations

• SprouseEtAl2012.instReprStructure = { reprPrec := SprouseEtAl2012.instReprStructure.repr }

inductive SprouseEtAl2012.GapPosition : Type

The gap-position factor: whether the dependency ends in the matrix clause or in the embedded clause.

• matrix : GapPosition
• embedded : GapPosition

@[instance_reducible]

instance SprouseEtAl2012.instDecidableEqGapPosition : DecidableEq GapPosition

Equations

• SprouseEtAl2012.instDecidableEqGapPosition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def SprouseEtAl2012.instReprGapPosition.repr : GapPosition → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance SprouseEtAl2012.instReprGapPosition : Repr GapPosition

Equations

• SprouseEtAl2012.instReprGapPosition = { reprPrec := SprouseEtAl2012.instReprGapPosition.repr }

@[reducible, inline]

abbrev SprouseEtAl2012.Ratings (α : Type u_1) : Type u_1

The ratings of a 2 × 2 factorial design (the paper's (5)): one rating per structure and gap position.

Equations

• SprouseEtAl2012.Ratings α = (SprouseEtAl2012.Structure → SprouseEtAl2012.GapPosition → α)

def SprouseEtAl2012.lengthEffect {α : Type u_1} [Field α] (r : Ratings α) : α

The dependency-length effect: the drop from a matrix to an embedded gap in nonisland structures.

Equations

• SprouseEtAl2012.lengthEffect r = r SprouseEtAl2012.Structure.nonisland SprouseEtAl2012.GapPosition.matrix - r SprouseEtAl2012.Structure.nonisland SprouseEtAl2012.GapPosition.embedded

def SprouseEtAl2012.structureEffect {α : Type u_1} [Field α] (r : Ratings α) : α

The island-structure effect: the drop from a nonisland to an island structure with a matrix gap.

Equations

• SprouseEtAl2012.structureEffect r = r SprouseEtAl2012.Structure.nonisland SprouseEtAl2012.GapPosition.matrix - r SprouseEtAl2012.Structure.island SprouseEtAl2012.GapPosition.matrix

def SprouseEtAl2012.dd {α : Type u_1} [Field α] (r : Ratings α) : α

The differences-in-differences score (the paper's (8)): the island-structure drop with an embedded gap less the island-structure drop with a matrix gap.

Equations

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

def SprouseEtAl2012.Additive {α : Type u_1} [Field α] (r : Ratings α) : Prop

Additivity: the drop for the island-violating sentence is the sum of the two effects.

Equations

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

def SprouseEtAl2012.Superadditive {α : Type u_1} [Field α] [LinearOrder α] (r : Ratings α) : Prop

Superadditivity, the island effect: the drop for the island-violating sentence exceeds the sum of the two effects.

Equations

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

theorem SprouseEtAl2012.additive_iff_dd_eq_zero {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] (r : Ratings α) : Additive r ↔ dd r = 0

theorem SprouseEtAl2012.superadditive_iff_dd_pos {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] (r : Ratings α) : Superadditive r ↔ 0 < dd r

The score is positive exactly on a superadditive interaction.

The theories

def SprouseEtAl2012.linear {α : Type u_1} [Field α] (base c₁ c₂ : α) : Ratings α

The simplest reductionist theory (the paper's (4)): a baseline lowered by the cost of a long-distance dependency and the cost of an island structure, each charged wherever present.

Equations

• SprouseEtAl2012.linear base c₁ c₂ s g = (base - if g = SprouseEtAl2012.GapPosition.embedded then c₁ else 0) - if s = SprouseEtAl2012.Structure.island then c₂ else 0

def SprouseEtAl2012.resourceLimitation {α : Type u_1} [Field α] (base c₁ c₂ : α) (overload : α → α) (capacity : α) : Ratings α

The resource-limitation theory (the paper's (6)): the linear costs, and an overload penalty depending on capacity in the sentence deploying both processes at once.

Equations

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

def SprouseEtAl2012.grammatical {α : Type u_1} [Field α] (base c₁ c₂ penalty : α) : Ratings α

A grammatical theory: the linear costs, and a constraint penalty on the island-violating sentence alone.

Equations

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

theorem SprouseEtAl2012.lengthEffect_linear {α : Type u_1} [Field α] (base c₁ c₂ : α) : lengthEffect (linear base c₁ c₂) = c₁

theorem SprouseEtAl2012.structureEffect_linear {α : Type u_1} [Field α] (base c₁ c₂ : α) : structureEffect (linear base c₁ c₂) = c₂

theorem SprouseEtAl2012.dd_linear {α : Type u_1} [Field α] (base c₁ c₂ : α) : dd (linear base c₁ c₂) = 0

The simplest reductionist theory predicts additivity: no island effect.

theorem SprouseEtAl2012.additive_linear {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] (base c₁ c₂ : α) : Additive (linear base c₁ c₂)

theorem SprouseEtAl2012.dd_resourceLimitation {α : Type u_1} [Field α] (base c₁ c₂ : α) (overload : α → α) (capacity : α) : dd (resourceLimitation base c₁ c₂ overload capacity) = overload capacity

The interaction under the resource-limitation theory is the overload penalty at the speaker's capacity.

theorem SprouseEtAl2012.superadditive_resourceLimitation_iff {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] (base c₁ c₂ : α) (overload : α → α) (capacity : α) : Superadditive (resourceLimitation base c₁ c₂ overload capacity) ↔ 0 < overload capacity

The resource-limitation theory predicts the observed superadditivity exactly where the penalty is positive.

theorem SprouseEtAl2012.dd_resourceLimitation_antitone {α : Type u_1} [Field α] [LinearOrder α] (base c₁ c₂ : α) {overload : α → α} (h : Antitone overload) : Antitone fun (capacity : α) => dd (resourceLimitation base c₁ c₂ overload capacity)

Limited capacity: with a penalty decreasing in capacity, the island effect decreases as capacity grows, the prediction of the paper's Figure 2a.

theorem SprouseEtAl2012.dd_resourceLimitation_eq_zero {α : Type u_1} [Field α] [LinearOrder α] (base c₁ c₂ : α) {overload : α → α} (h : ∀ (capacity : α), c₁ + c₂ ≤ capacity → overload capacity = 0) {capacity : α} (hc : c₁ + c₂ ≤ capacity) : dd (resourceLimitation base c₁ c₂ overload capacity) = 0

Overload: a speaker whose capacity covers both costs shows no island effect.

theorem SprouseEtAl2012.dd_grammatical {α : Type u_1} [Field α] (base c₁ c₂ penalty : α) : dd (grammatical base c₁ c₂ penalty) = penalty

The interaction under a grammatical theory is the constraint's penalty, the same at every capacity, the prediction of the paper's Figure 2b.

theorem SprouseEtAl2012.resourceLimitation_eq_grammatical {α : Type u_1} [Field α] (base c₁ c₂ : α) (overload : α → α) (capacity : α) : resourceLimitation base c₁ c₂ overload capacity = grammatical base c₁ c₂ (overload capacity)

Both theories reproduce the observed pattern: the resource-limitation theory at a capacity the two costs exceed matches a grammatical theory whose penalty is the overload.