def embeddedQuestionConstraint : PhenomenonData

Embedded question constraint: wh-dependencies blocked across intervening wh-phrase

Equations

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

def complexNPConstraint : PhenomenonData

CNPC: wh-dependencies blocked into relative clauses and noun complements

Equations

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

def adjunctClauseConstraint : PhenomenonData

Adjunct constraint: wh-dependencies blocked into adjunct clauses

Equations

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

def coordinateStructureConstraint : PhenomenonData

CSC: asymmetric wh-dependencies blocked in coordination

Equations

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

def subjectConstraint : PhenomenonData

Subject constraint: wh-dependencies into subjects degraded

Equations

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

def islandData : List PhenomenonData

All island constraint data

Equations

• islandData = [embeddedQuestionConstraint, complexNPConstraint, adjunctClauseConstraint, coordinateStructureConstraint, subjectConstraint]

inductive ConstraintType : Type

Types of island constraints (descriptive labels)

• embeddedQuestion : ConstraintType
• complexNP : ConstraintType
• adjunct : ConstraintType
• coordinate : ConstraintType
• subject : ConstraintType
• sententialSubject : ConstraintType
• mannerOfSpeaking : ConstraintType

instance instReprConstraintType : Repr ConstraintType

Equations

• instReprConstraintType = { reprPrec := instReprConstraintType.repr }

def instReprConstraintType.repr : ConstraintType → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• instReprConstraintType.repr ConstraintType.complexNP prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ConstraintType.complexNP")).group prec✝
• instReprConstraintType.repr ConstraintType.adjunct prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ConstraintType.adjunct")).group prec✝
• instReprConstraintType.repr ConstraintType.coordinate prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ConstraintType.coordinate")).group prec✝
• instReprConstraintType.repr ConstraintType.subject prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ConstraintType.subject")).group prec✝

instance instDecidableEqConstraintType : DecidableEq ConstraintType

Equations

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

inductive ConstraintStrength : Type

Constraint strength classification

• strong : ConstraintStrength
• weak : ConstraintStrength

instance instReprConstraintStrength : Repr ConstraintStrength

Equations

• instReprConstraintStrength = { reprPrec := instReprConstraintStrength.repr }

def instReprConstraintStrength.repr : ConstraintStrength → Nat → Std.Format

Equations

• instReprConstraintStrength.repr ConstraintStrength.strong prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ConstraintStrength.strong")).group prec✝
• instReprConstraintStrength.repr ConstraintStrength.weak prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ConstraintStrength.weak")).group prec✝

instance instDecidableEqConstraintStrength : DecidableEq ConstraintStrength

Equations

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

def constraintStrength : ConstraintType → ConstraintStrength

Classification of constraint types by strength

Equations

• constraintStrength ConstraintType.embeddedQuestion = ConstraintStrength.weak
• constraintStrength ConstraintType.complexNP = ConstraintStrength.strong
• constraintStrength ConstraintType.adjunct = ConstraintStrength.strong
• constraintStrength ConstraintType.coordinate = ConstraintStrength.strong
• constraintStrength ConstraintType.subject = ConstraintStrength.weak
• constraintStrength ConstraintType.sententialSubject = ConstraintStrength.strong
• constraintStrength ConstraintType.mannerOfSpeaking = ConstraintStrength.weak

inductive FGDConstruction : Type

The three canonical filler-gap dependency constructions in English. Each shares the abstract mechanism of movement (a filler displaced from a gap) but differs in information-structural profile (@cite{abeille-et-al-2020}).

The distinction matters for testing whether island effects are construction-specific (as @cite{abeille-et-al-2020} claim) or construction-general (as @cite{cartner-et-al-2026} argue).

• whQuestion : FGDConstruction

  Wh-questions: "Which driver did Stephanie explain _ had already questioned the driver?"

• relativeClause : FGDConstruction

  Relative clauses: "I noticed [the investigator that Stephanie explained _ had already questioned the driver]."

• topicalization : FGDConstruction

  Topicalization: "That investigator, Stephanie explained _ had already questioned the driver."

instance instDecidableEqFGDConstruction : DecidableEq FGDConstruction

Equations

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

def instReprFGDConstruction.repr : FGDConstruction → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• instReprFGDConstruction.repr FGDConstruction.whQuestion prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "FGDConstruction.whQuestion")).group prec✝

instance instReprFGDConstruction : Repr FGDConstruction

Equations

• instReprFGDConstruction = { reprPrec := instReprFGDConstruction.repr }

def instBEqFGDConstruction.beq : FGDConstruction → FGDConstruction → Bool

Equations

• instBEqFGDConstruction.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance instBEqFGDConstruction : BEq FGDConstruction

Equations

• instBEqFGDConstruction = { beq := instBEqFGDConstruction.beq }

inductive ExtractionPosition : Type

Extraction position within the embedded clause. The subject/object asymmetry is the core empirical target of subject island research (@cite{ross-1967}, @cite{chomsky-1973}).

• subject : ExtractionPosition
• object : ExtractionPosition

instance instDecidableEqExtractionPosition : DecidableEq ExtractionPosition

Equations

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

def instReprExtractionPosition.repr : ExtractionPosition → Nat → Std.Format

Equations

• instReprExtractionPosition.repr ExtractionPosition.subject prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ExtractionPosition.subject")).group prec✝
• instReprExtractionPosition.repr ExtractionPosition.object prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ExtractionPosition.object")).group prec✝

instance instReprExtractionPosition : Repr ExtractionPosition

Equations

• instReprExtractionPosition = { reprPrec := instReprExtractionPosition.repr }

instance instBEqExtractionPosition : BEq ExtractionPosition

Equations

• instBEqExtractionPosition = { beq := instBEqExtractionPosition.beq }

def instBEqExtractionPosition.beq : ExtractionPosition → ExtractionPosition → Bool

Equations

• instBEqExtractionPosition.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

inductive IslandSource : Type

Source of an island constraint: what mechanism produces it. Distinguishes structural accounts (subjacency), processing accounts (memory load), and discourse accounts (information structure).

• syntactic : IslandSource

  Syntactic: island follows from structural configuration

• processing : IslandSource

  Processing: island is an artifact of memory/retrieval difficulty

• discourse : IslandSource

  Discourse: island arises from information-structural backgroundedness (@cite{goldberg-2006}, 2013; Lu, @cite{lu-degen-2025})

instance instReprIslandSource : Repr IslandSource

Equations

• instReprIslandSource = { reprPrec := instReprIslandSource.repr }

def instReprIslandSource.repr : IslandSource → Nat → Std.Format

Equations

• instReprIslandSource.repr IslandSource.syntactic prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "IslandSource.syntactic")).group prec✝
• instReprIslandSource.repr IslandSource.processing prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "IslandSource.processing")).group prec✝
• instReprIslandSource.repr IslandSource.discourse prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "IslandSource.discourse")).group prec✝

instance instDecidableEqIslandSource : DecidableEq IslandSource

Equations

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

instance instBEqIslandSource : BEq IslandSource

Equations

• instBEqIslandSource = { beq := instBEqIslandSource.beq }

def instBEqIslandSource.beq : IslandSource → IslandSource → Bool

Equations

• instBEqIslandSource.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def constraintSource : ConstraintType → IslandSource

Classification of island constraints by source. Traditional islands are syntactic; MoS islands are discourse-based. Note: this classification is itself debated — @cite{hofmeister-sag-2010} argue that many "syntactic" islands are actually processing-based. See Comparisons/Islands.lean.

Equations

• constraintSource ConstraintType.embeddedQuestion = IslandSource.syntactic
• constraintSource ConstraintType.complexNP = IslandSource.syntactic
• constraintSource ConstraintType.adjunct = IslandSource.syntactic
• constraintSource ConstraintType.coordinate = IslandSource.syntactic
• constraintSource ConstraintType.subject = IslandSource.syntactic
• constraintSource ConstraintType.sententialSubject = IslandSource.syntactic
• constraintSource ConstraintType.mannerOfSpeaking = IslandSource.discourse

theorem mos_is_discourse_island : constraintSource ConstraintType.mannerOfSpeaking = IslandSource.discourse

MoS islands are the only discourse-sourced island type currently formalized.

theorem mos_is_weak : constraintStrength ConstraintType.mannerOfSpeaking = ConstraintStrength.weak

MoS islands are weak (ameliorable).

Gradience in Island Effects

@cite{hofmeister-sag-2010} @cite{chomsky-1973} @cite{chomsky-1982} @cite{chomsky-1995} @cite{ross-1967} @cite{goldberg-2006} @cite{lu-degen-2025}

@cite{hofmeister-sag-2010} argue that the binary strong/weak classification is insufficient. Island effects are gradient along multiple dimensions, and acceptability varies systematically with nonstructural manipulations that leave island configurations intact.

This challenges every categorical island constraint proposed:

• Subjacency
• Complex NP Constraint
• Barriers
• Minimal Link Condition

See Phenomena.FillerGap.Compare for the competence vs. performance comparison.

inductive ProcessingFactor : Type

Processing factors that independently contribute to the difficulty of filler-gap dependencies inside islands.

• locality : ProcessingFactor

  Distance between filler and gap increases memory load (§3.1). Confirmed by processing studies.

• referentialLoad : ProcessingFactor

  Referential processing of intervening constituents depletes resources (§3.2). Definites trigger referent search; proper names > definites > indefinites > pronouns in processing cost.

• clauseBoundary : ProcessingFactor

  Clause boundaries impose processing cost independent of extraction (§3.3). Even in yes-no questions, different complementizers elicit different neurological responses and acceptability.

• fillerComplexity : ProcessingFactor

  Syntactic/semantic complexity of the filler phrase affects retrieval (§3.4). Counterintuitively, MORE complex fillers REDUCE processing difficulty because richer representations resist interference and aid retrieval.

def instReprProcessingFactor.repr : ProcessingFactor → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• instReprProcessingFactor.repr ProcessingFactor.locality prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ProcessingFactor.locality")).group prec✝

instance instReprProcessingFactor : Repr ProcessingFactor

Equations

• instReprProcessingFactor = { reprPrec := instReprProcessingFactor.repr }

instance instDecidableEqProcessingFactor : DecidableEq ProcessingFactor

Equations

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

instance instBEqProcessingFactor : BEq ProcessingFactor

Equations

• instBEqProcessingFactor = { beq := instBEqProcessingFactor.beq }

def instBEqProcessingFactor.beq : ProcessingFactor → ProcessingFactor → Bool

Equations

• instBEqProcessingFactor.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

inductive FillerType : Type

Complexity of the displaced wh-phrase.

Hofmeister & Sag's central manipulation across all three experiments. More complex fillers (which-N phrases) facilitate processing inside islands, because richer representations aid memory retrieval (§3.4).

• bare : FillerType

  Bare wh-word: who, what

• whichN : FillerType

  Complex wh-phrase: which convict, which employee

def instReprFillerType.repr : FillerType → Nat → Std.Format

Equations

• instReprFillerType.repr FillerType.bare prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "FillerType.bare")).group prec✝
• instReprFillerType.repr FillerType.whichN prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "FillerType.whichN")).group prec✝

instance instReprFillerType : Repr FillerType

Equations

• instReprFillerType = { reprPrec := instReprFillerType.repr }

instance instDecidableEqFillerType : DecidableEq FillerType

Equations

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

instance instBEqFillerType : BEq FillerType

Equations

• instBEqFillerType = { beq := instBEqFillerType.beq }

def instBEqFillerType.beq : FillerType → FillerType → Bool

Equations

• instBEqFillerType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

inductive IslandNPType : Type

Type of the island-forming NP (Experiment 1 only).

Definite NPs trigger referent search and presupposition accommodation, consuming resources needed for dependency resolution (§3.2).

• definite : IslandNPType

  Definite singular: the report

• plural : IslandNPType

  Indefinite plural: reports

• indefinite : IslandNPType

  Indefinite singular: a report

instance instReprIslandNPType : Repr IslandNPType

Equations

• instReprIslandNPType = { reprPrec := instReprIslandNPType.repr }

def instReprIslandNPType.repr : IslandNPType → Nat → Std.Format

Equations

• instReprIslandNPType.repr IslandNPType.definite prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "IslandNPType.definite")).group prec✝
• instReprIslandNPType.repr IslandNPType.plural prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "IslandNPType.plural")).group prec✝
• instReprIslandNPType.repr IslandNPType.indefinite prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "IslandNPType.indefinite")).group prec✝

instance instDecidableEqIslandNPType : DecidableEq IslandNPType

Equations

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

instance instBEqIslandNPType : BEq IslandNPType

Equations

• instBEqIslandNPType = { beq := instBEqIslandNPType.beq }

def instBEqIslandNPType.beq : IslandNPType → IslandNPType → Bool

Equations

• instBEqIslandNPType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

structure IslandCondition : Type

An experimental condition from @cite{hofmeister-sag-2010}. Acceptability stored as Nat (judgment ratio × 100, so 78 means 0.78).

• island : ConstraintType
• filler : FillerType
• npType : Option IslandNPType
• acceptability : Nat

  Mean judgment ratio × 100

• citation : String

instance instReprIslandCondition : Repr IslandCondition

Equations

• instReprIslandCondition = { reprPrec := instReprIslandCondition.repr }

def instReprIslandCondition.repr : IslandCondition → Nat → Std.Format

Equations

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

def cnpcAcceptability : List IslandCondition

Experiment 1: CNPC violations (§5). 36 items, (2 × 3) + 1 design. Acceptability ratings on 1–8 scale, normalized as ratio of subject mean. Data from Figure 3 (p. 393).

Equations

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

def whIslandAcceptability : List IslandCondition

Experiment 2: Wh-island violations (§6). 24 items, 2 + 1 design. Acceptability on 1–7 scale, normalized. Data from Figure 5 (p. 397). Key finding: F1(1,15)=15.964, p=0.001; F2(1,19)=14.428, p=0.001.

Equations

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

def cnpcBaseline : Nat

Non-island baseline acceptability (CNPC experiment, Figure 3).

Equations

• cnpcBaseline = 108

def avgAcceptability (conditions : List IslandCondition) (f : FillerType) : Nat

Average acceptability for a filler type across a set of conditions.

Equations

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

theorem cnpc_whichN_gt_bare : avgAcceptability cnpcAcceptability FillerType.whichN > avgAcceptability cnpcAcceptability FillerType.bare

Filler complexity effect in CNPC: which-N > bare wh (§5.2). F1(1,20)=48.741, p<0.0001; F2(1,35)=39.494, p<0.0001. The structure is identical — only the filler changes.

theorem whIsland_whichN_gt_bare : avgAcceptability whIslandAcceptability FillerType.whichN > avgAcceptability whIslandAcceptability FillerType.bare

Filler complexity effect in wh-islands: which-N > bare wh (§6.2). F1(1,15)=15.964, p=0.001.

theorem cnpc_indefinite_gt_definite : have indef := List.filter (fun (x : IslandCondition) => x.npType == some IslandNPType.indefinite) cnpcAcceptability; have def_ := List.filter (fun (x : IslandCondition) => x.npType == some IslandNPType.definite) cnpcAcceptability; List.foldl (fun (x1 : Nat) (x2 : IslandCondition) => x1 + x2.acceptability) 0 indef > List.foldl (fun (x1 : Nat) (x2 : IslandCondition) => x1 + x2.acceptability) 0 def_

NP type effect: indefinite > definite across both filler types (§5.2). Consistent with lower referential processing cost for indefinites.

theorem best_island_lt_baseline : 85 < cnpcBaseline

Even the best island condition (which-PL, 85) remains below the non-island baseline (108). Islands are ameliorated, not eliminated.