Sprouse, Wagers & Phillips (2012) — Factorial Acceptability Designs

[SWP12], with the magnitude-estimation groundwork of [Spr07].

Contract types for the factorial acceptability-judgment experimental paradigm: formal/experimental-syntax studies that elicit sentence acceptability ratings across a factorial design to test categorical predictions of grammatical theory. The paradigm is theory-agnostic: it specifies what kind of input the experiment provides and what shape of output a theory must produce; bridge theorems in downstream Studies/ files translate theory-native predictions into these types.

Main declarations

• FactorialCondition: a typed cell in a 2-factor factorial design, generic over the factor types.
• DDResult: a difference-in-differences score (the Maxwell & Delaney 2003 computation [SWP12] use as the standard test of island effects), stored as ℚ for exact arithmetic.
• AccountPredictions: an n-cell prediction tuple from a theoretical account, with a decidable Matches comparator.
• SentencePair.toFactorial: the pre-experimental minimal-pair datum (Linglib/Features/MinimalPairs.lean) as the degenerate 1×2 case of a factorial design.

Out of scope

• Statistical-model specifications (LME formulae, contrast coding, random-effect structures) — analysis-pipeline detail
• Stimulus norming details (filler ratings, balancing constraints) — study-internal methodology
• Participant-population metadata (L1, age, dialect) — study metadata
• Raw rating scales / z-score transformations — measurement detail

Factorial conditions

structure SprouseEtAl2012.FactorialCondition (F1 F2 : Type) : Type

A typed cell in a 2-factor factorial design ([Spr07]: §2; [SWP12]: §2.1).

Generic over the two factor types so that the same machinery accepts any 2×2/2×3/3×3 design. The sentence field carries the actual stimulus (verbatim from the paper); label is the experiment's printed condition name.

• label : String

  Condition label as printed in the paper (e.g. "WhHell-Situ").

• level1 : F1

  Level of the first factor.

• level2 : F2

  Level of the second factor.

• sentence : String

  Verbatim stimulus sentence.

@[implicit_reducible]

instance SprouseEtAl2012.instReprFactorialCondition {F1✝ F2✝ : Type} [Repr F1✝] [Repr F2✝] : Repr (FactorialCondition F1✝ F2✝)

Equations

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

def SprouseEtAl2012.instReprFactorialCondition.repr {F1✝ F2✝ : Type} [Repr F1✝] [Repr F2✝] : FactorialCondition F1✝ F2✝ → ℕ → Std.Format

Equations

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

Difference-in-differences scores

structure SprouseEtAl2012.DDResult : Type

A difference-in-differences (DD) score from a 2×2 factorial design, using the Maxwell & Delaney (2003) computation: DD = D2 − D1, where D1 and D2 are the two main-factor differences. A positive DD reflects a superadditive interaction — a penalty above and beyond the sum of the two main effects. [SWP12]'s standard test of island effects in experimental syntax.

Stored as ℚ rather than Float to respect linglib's exact-arithmetic discipline. The interactionSignificant flag records the linear mixed-effects model's interaction-term p-value (typically p < 0.05).

• comparison : String

  Description of the two-factor contrast (e.g. "in-situ vs full movement").

• dd : ℚ

  DD score. Positive → superadditive interaction; ≈ 0 → additive.

• interactionSignificant : Bool

  Did the LME model's interaction term reach significance?

def SprouseEtAl2012.instReprDDResult.repr : DDResult → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance SprouseEtAl2012.instReprDDResult : Repr DDResult

Equations

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

def SprouseEtAl2012.DDResult.Superadditive (r : DDResult) : Prop

A DD score is superadditive if positive — extra penalty beyond main effects.

Equations

• r.Superadditive = (r.dd > 0)

def SprouseEtAl2012.DDResult.Additive (r : DDResult) : Prop

A DD score is additive if ≈ 0 — no interaction beyond main effects.

Equations

• r.Additive = (r.dd = 0)

@[implicit_reducible]

instance SprouseEtAl2012.DDResult.instDecidableSuperadditive (r : DDResult) : Decidable r.Superadditive

Equations

• r.instDecidableSuperadditive = id inferInstance

@[implicit_reducible]

instance SprouseEtAl2012.DDResult.instDecidableAdditive (r : DDResult) : Decidable r.Additive

Equations

• r.instDecidableAdditive = id inferInstance

Account predictions

structure SprouseEtAl2012.AccountPredictions (n : ℕ) : Type

A theoretical account's predicted acceptability pattern across n cells of a factorial design. Each cell is True (predicted acceptable) or False (predicted unacceptable).

Used to compare a theory's predictions against the empirical pattern via Matches.

• cell : Fin n → Prop

  Per-cell predicted acceptability.

• decCell (i : Fin n) : Decidable (self.cell i)

  Each cell is decidable (so pattern comparison is decidable).

def SprouseEtAl2012.AccountPredictions.Matches {n : ℕ} (a b : AccountPredictions n) : Prop

Two prediction tuples match iff they predict the same pattern in every cell.

Equations

• a.Matches b = ∀ (i : Fin n), a.cell i ↔ b.cell i

@[implicit_reducible]

instance SprouseEtAl2012.AccountPredictions.instDecidableMatches {n : ℕ} (a b : AccountPredictions n) : Decidable (a.Matches b)

Equations

• a.instDecidableMatches b = Fintype.decidableForallFintype

def SprouseEtAl2012.AccountPredictions.of2x2 (p₀₀ p₀₁ p₁₀ p₁₁ : Prop) [Decidable p₀₀] [Decidable p₀₁] [Decidable p₁₀] [Decidable p₁₁] : AccountPredictions 4

Build a 4-cell AccountPredictions from four explicit Props (the standard 2×2 case). Convenience for the most common factorial.

Equations

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

def SprouseEtAl2012.AccountPredictions.of3 (p₀ p₁ p₂ : Prop) [Decidable p₀] [Decidable p₁] [Decidable p₂] : AccountPredictions 3

Build a 3-cell AccountPredictions (e.g., a 1×3 strategy contrast).

Equations

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

Relation to introspective minimal pairs

def SprouseEtAl2012.SentencePair.toFactorial (sp : Features.MinimalPairs.SentencePair) : FactorialCondition Unit Bool × FactorialCondition Unit Bool

A SentencePair is structurally a 1×2 factorial design: one Unit-valued first factor, a Bool-valued grammaticality factor, one cell per Bool value. This makes the relationship between the minimal-pair tradition and the factorial discipline explicit: SentencePair is the degenerate case of FactorialCondition Unit Bool lifted to a pair of cells.

Equations

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