Islands: Descriptive Vocabulary

Cross-paper substrate types for classifying island constraints. Each island study (Studies/AuthorYear.lean) populates these classifications from its own theoretical commitments; the types themselves are theory-neutral descriptive labels.

Types

• ConstraintType — Ross 1967's foundational island-constraint inventory (CNPC, adjunct, coordinate, subject, sentential subject) plus later extensions (manner-of-speaking, definite nominal).
• ConstraintStrength — strong (categorical) vs weak (ameliorated by D-linking, processing, or other factors).
• IslandSource — the mechanism a study attributes the island to: syntactic (PIC, subjacency, AL), semantic (binding, Specificity Condition), processing (memory/retrieval), discourse (information-structural backgroundedness).

Why this file exists

These enums were originally hosted in Studies/Ross1967.lean, which forced every consumer (across Islands/, Questions/, FillerGap/, ArgumentStructure/) to transitively import Ross's empirical apparatus just to obtain the classification types. Promoting them to a phenomenon-level data file matches the CLAUDE.md "Data files (top level)" pattern: no imports from Theories/, shared facts any theory must account for.

Consumers

Files that classify islands using these types include:

• Studies/Adger2025.lean — Angular Locality (graph-theoretic)
• Studies/ShenHuang2026.lean — PIC + Specificity composite
• Studies/CartnerEtAl2026.lean — cross-constructional invariance
• Studies/HofmeisterSag2010.lean — processing/gradient
• Phenomena/Islands/MannerOfSpeaking.lean — discourse backgroundedness
• Phenomena/Questions/Studies/ChanShen2026.lean — semantic
• Phenomena/FillerGap/Studies/LuPanDegen2025.lean — backgroundedness

inductive Phenomena.Islands.ConstraintType : Type

Types of island constraints (descriptive labels). Ross's foundational five plus later additions (MoS verbs, definite nominals).

• embeddedQuestion : ConstraintType

  Wh-word blocks further wh-dependency.

• complexNP : ConstraintType

  Complex NP blocks dependency (Ross 1967).

• adjunct : ConstraintType

  Adjunct clause blocks dependency.

• coordinate : ConstraintType

  Coordination blocks asymmetric dependency (CSC).

• subject : ConstraintType

  Subject position blocks dependency.

• sententialSubject : ConstraintType

  Sentential subject blocks dependency.

• mannerOfSpeaking : ConstraintType

  MoS verb complement backgrounds content (@cite{lu-pan-degen-2025}).

• definiteNominal : ConstraintType

  Definite/specific DP blocks dependency (@cite{chomsky-1973}, @cite{shen-huang-2026}).

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

Equations

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

@[implicit_reducible]

instance Phenomena.Islands.instReprConstraintType : Repr ConstraintType

Equations

• Phenomena.Islands.instReprConstraintType = { reprPrec := Phenomena.Islands.instReprConstraintType.repr }

@[implicit_reducible]

instance Phenomena.Islands.instDecidableEqConstraintType : DecidableEq ConstraintType

Equations

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

inductive Phenomena.Islands.ConstraintStrength : Type

Constraint strength classification.

• strong : ConstraintStrength

  Consistently blocks the dependency.

• weak : ConstraintStrength

  Ameliorated in some contexts (D-linking, processing facilitation, stage-level subjects, etc.).

@[implicit_reducible]

instance Phenomena.Islands.instReprConstraintStrength : Repr ConstraintStrength

Equations

• Phenomena.Islands.instReprConstraintStrength = { reprPrec := Phenomena.Islands.instReprConstraintStrength.repr }

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

Equations

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

@[implicit_reducible]

instance Phenomena.Islands.instDecidableEqConstraintStrength : DecidableEq ConstraintStrength

Equations

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

inductive Phenomena.Islands.IslandSource : Type

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

These are descriptive labels for the mechanism — the classification of which source applies to which island type is a theoretical claim, derived in individual study files from their theoretical commitments.

• syntactic : IslandSource

  Syntactic: island follows from structural configuration (PIC, subjacency, Angular Locality).

• semantic : IslandSource

  Semantic: island follows from a binding restriction (Specificity Condition).

• processing : IslandSource

  Processing: island is an artifact of memory/retrieval difficulty.

• discourse : IslandSource

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

@[implicit_reducible]

instance Phenomena.Islands.instReprIslandSource : Repr IslandSource

Equations

• Phenomena.Islands.instReprIslandSource = { reprPrec := Phenomena.Islands.instReprIslandSource.repr }

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

Equations

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

@[implicit_reducible]

instance Phenomena.Islands.instDecidableEqIslandSource : DecidableEq IslandSource

Equations

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