Acceptability Judgment Paradigm

@cite{sprouse-2007} @cite{sprouse-et-al-2012}

Shared vocabulary for the acceptability judgment experimental paradigm — formal-syntax / experimental-syntax studies that elicit sentence acceptability ratings (typically on a Likert or 100-point scale) to test categorical predictions of grammatical theory.

Architectural role

Paradigms/ is the contract layer between Theories/ and Phenomena/Studies/. Theories produce predictions in their native types; bridge theorems in Studies/ translate those predictions into paradigm-typed predictions and prove they satisfy the empirical patterns documented in the study file. The paradigm itself is theory-agnostic: it specifies what kind of input the experiment provides and what shape of output a theory must produce.

What this file provides

1. FactorialCondition: a typed cell in a 2-factor factorial design. Generic over the factor types so that any pair (Bool × WhStrategy, Person × Number, Animacy × Definiteness, …) plugs in.
2. DDResult: a difference-in-differences score (Maxwell & Delaney 2003 method, used by @cite{sprouse-et-al-2012} for island effects and by @cite{chan-shen-2026} for wh-the-hell licensing). Stored as ℚ for exact arithmetic, with a Boolean interactionSignificant flag for the linear-mixed-effects model's interaction p-value.
3. AccountPredictions: an n-cell prediction tuple from a theoretical account, with a matchesPattern comparator. Generic over n so that 2×2 (4 cells), 2×3 (6 cells), etc. all use the same machinery.

Out of scope (per CLAUDE.md Processing 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

The paradigm specifies the empirical contract between an account and the data — what cells are tested and what pattern is observed — not the statistical apparatus that produces the pattern.

structure Paradigms.AcceptabilityJudgment.FactorialCondition (F1 F2 : Type) : Type

A typed cell in a 2-factor factorial design (@cite{sprouse-2007}: §2; @cite{sprouse-et-al-2012}: §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 Paradigms.AcceptabilityJudgment.instReprFactorialCondition {F1✝ F2✝ : Type} [Repr F1✝] [Repr F2✝] : Repr (FactorialCondition F1✝ F2✝)

Equations

• Paradigms.AcceptabilityJudgment.instReprFactorialCondition = { reprPrec := Paradigms.AcceptabilityJudgment.instReprFactorialCondition.repr }

def Paradigms.AcceptabilityJudgment.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.

structure Paradigms.AcceptabilityJudgment.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.

Used by @cite{sprouse-et-al-2012} as the standard test of island effects in experimental syntax, and by @cite{chan-shen-2026} for wh-the-hell licensing.

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 Paradigms.AcceptabilityJudgment.instReprDDResult.repr : DDResult → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Paradigms.AcceptabilityJudgment.instReprDDResult : Repr DDResult

Equations

• Paradigms.AcceptabilityJudgment.instReprDDResult = { reprPrec := Paradigms.AcceptabilityJudgment.instReprDDResult.repr }

def Paradigms.AcceptabilityJudgment.DDResult.Superadditive (r : DDResult) : Prop

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

Equations

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

def Paradigms.AcceptabilityJudgment.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 Paradigms.AcceptabilityJudgment.DDResult.instDecidableSuperadditive (r : DDResult) : Decidable r.Superadditive

Equations

• r.instDecidableSuperadditive = id inferInstance

@[implicit_reducible]

instance Paradigms.AcceptabilityJudgment.DDResult.instDecidableAdditive (r : DDResult) : Decidable r.Additive

Equations

• r.instDecidableAdditive = id inferInstance

structure Paradigms.AcceptabilityJudgment.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 Paradigms.AcceptabilityJudgment.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 Paradigms.AcceptabilityJudgment.AccountPredictions.instDecidableMatches {n : ℕ} (a b : AccountPredictions n) : Decidable (a.Matches b)

Equations

• a.instDecidableMatches b = Fintype.decidableForallFintype

def Paradigms.AcceptabilityJudgment.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 Paradigms.AcceptabilityJudgment.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.

Minimal pairs as introspective grammaticality contrasts — the methodological tradition that Sprouse's factorial-design machinery above was introduced to discipline. A minimal pair records a single (typically the analyst's) judgment per sentence: one is grammatical, one is not, and they differ minimally in the property being tested.

Two parallel families:

* **Word-based** (`MinimalPair`, `PhenomenonData`): sentences are
  `List Word`, requiring feature specifications. Used by analyses
  that operate on parsed/featural representations (HPSG, DG, Minimalism).
* **String-based** (`SentencePair`, `StringPhenomenonData`): sentences
  are raw strings, parseable by any theory. Used by phenomenon data
  files that should remain free of theoretical commitments. 

structure Paradigms.AcceptabilityJudgment.MinimalPair : Type

A minimal pair: grammatical vs ungrammatical, with context.

Conceptually a degenerate FactorialCondition Unit Bool with the Bool factor being grammaticality and a single trivial Unit factor; kept as a distinct shape because the introspective tradition speaks in grammatical / ungrammatical rather than factorial cells.

• grammatical : List Word
• ungrammatical : List Word
• clauseType : Features.ClauseForm
• description : String
• citation : String

def Paradigms.AcceptabilityJudgment.instReprMinimalPair.repr : MinimalPair → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Paradigms.AcceptabilityJudgment.instReprMinimalPair : Repr MinimalPair

Equations

• Paradigms.AcceptabilityJudgment.instReprMinimalPair = { reprPrec := Paradigms.AcceptabilityJudgment.instReprMinimalPair.repr }

structure Paradigms.AcceptabilityJudgment.PhenomenonData : Type

Collection of minimal pairs for a phenomenon.

• name : String
• pairs : List MinimalPair
• generalization : String

@[implicit_reducible]

instance Paradigms.AcceptabilityJudgment.instReprPhenomenonData : Repr PhenomenonData

Equations

• Paradigms.AcceptabilityJudgment.instReprPhenomenonData = { reprPrec := Paradigms.AcceptabilityJudgment.instReprPhenomenonData.repr }

def Paradigms.AcceptabilityJudgment.instReprPhenomenonData.repr : PhenomenonData → ℕ → Std.Format

Equations

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

def Paradigms.AcceptabilityJudgment.capturesMinimalPairBy (pred : List Word → Bool) (pair : MinimalPair) : Bool

Check if a grammaticality predicate captures a minimal pair.

Captures the pair iff the predicate accepts the grammatical sentence and rejects the ungrammatical sentence.

Equations

• Paradigms.AcceptabilityJudgment.capturesMinimalPairBy pred pair = (pred pair.grammatical && !pred pair.ungrammatical)

def Paradigms.AcceptabilityJudgment.capturesPhenomenonData (pred : List Word → Bool) (phenom : PhenomenonData) : Bool

Check if a grammaticality predicate captures all minimal pairs in a phenomenon dataset.

Equations

• Paradigms.AcceptabilityJudgment.capturesPhenomenonData pred phenom = phenom.pairs.all (Paradigms.AcceptabilityJudgment.capturesMinimalPairBy pred)

structure Paradigms.AcceptabilityJudgment.SentencePair : Type

String-based minimal pair for theory-neutral phenomena.

Unlike MinimalPair which uses List Word (requiring feature specifications), this type uses raw strings that can be parsed by any theory. This keeps empirical data in Phenomena/ free from theoretical commitments.

• grammatical : String

  The grammatical sentence

• ungrammatical : String

  The ungrammatical sentence

• clauseType : Features.ClauseForm

  Clause form (declarative, question, etc.)

• description : String

  Description of what the pair tests

• citation : String

  Citation for the data; empty string for uncited examples.

@[implicit_reducible]

instance Paradigms.AcceptabilityJudgment.instReprSentencePair : Repr SentencePair

Equations

• Paradigms.AcceptabilityJudgment.instReprSentencePair = { reprPrec := Paradigms.AcceptabilityJudgment.instReprSentencePair.repr }

def Paradigms.AcceptabilityJudgment.instReprSentencePair.repr : SentencePair → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Paradigms.AcceptabilityJudgment.instBEqSentencePair : BEq SentencePair

Equations

• Paradigms.AcceptabilityJudgment.instBEqSentencePair = { beq := Paradigms.AcceptabilityJudgment.instBEqSentencePair.beq }

def Paradigms.AcceptabilityJudgment.instBEqSentencePair.beq : SentencePair → SentencePair → Bool

Equations

• One or more equations did not get rendered due to their size.
• Paradigms.AcceptabilityJudgment.instBEqSentencePair.beq x✝¹ x✝ = false

structure Paradigms.AcceptabilityJudgment.StringPhenomenonData : Type

String-based phenomenon data for theory-neutral representation.

This is the string-based analogue of PhenomenonData. Phenomena files should use this type so that empirical data is decoupled from any particular grammatical theory's representation.

• name : String

  Name of the phenomenon

• pairs : List SentencePair

  List of minimal pairs

• generalization : String

  Generalization captured by this data

@[implicit_reducible]

instance Paradigms.AcceptabilityJudgment.instReprStringPhenomenonData : Repr StringPhenomenonData

Equations

• Paradigms.AcceptabilityJudgment.instReprStringPhenomenonData = { reprPrec := Paradigms.AcceptabilityJudgment.instReprStringPhenomenonData.repr }

def Paradigms.AcceptabilityJudgment.instReprStringPhenomenonData.repr : StringPhenomenonData → ℕ → Std.Format

Equations

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

def Paradigms.AcceptabilityJudgment.SentencePair.toFactorial (sp : 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 to §1's 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.