Constraints on Variables in Syntax

[Ros67]

[Ros67] identified the foundational island constraints that block long-distance wh-dependencies: embedded question constraint, Complex NP Constraint, adjunct clause constraint, Coordinate Structure Constraint, and subject constraint.

Vocabulary types

ConstraintType / ConstraintStrength / IslandSource are the descriptive labels island studies classify with. The constraint inventory is Ross's five plus the later extensions the enum must carry because consumers share one type (manner-of-speaking, definite nominal). Source and strength classifications are NOT stipulated globally — each study derives its own from its theoretical commitments. See:

• LuPanDegen2025.lean: mosIslandSources, mosIslandStrength
• ShenHuang2026.lean: definiteNominalSources, definiteNominalStrength
• Adger2025.lean: adgerSubjectIslandSource, adgerDefiniteNominalSources
• CartnerEtAl2026.lean: subjectIslandSource

inductive 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 ([LPD25]).

• definiteNominal : ConstraintType

  Definite/specific DP blocks dependency ([Cho73], [SH26]).

def instReprConstraintType.repr : ConstraintType → ℕ → 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✝

@[implicit_reducible]

instance instReprConstraintType : Repr ConstraintType

Equations

• instReprConstraintType = { reprPrec := instReprConstraintType.repr }

@[implicit_reducible]

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

  Consistently blocks the dependency.

• weak : ConstraintStrength

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

def instReprConstraintStrength.repr : ConstraintStrength → ℕ → 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✝

@[implicit_reducible]

instance instReprConstraintStrength : Repr ConstraintStrength

Equations

• instReprConstraintStrength = { reprPrec := instReprConstraintStrength.repr }

@[implicit_reducible]

instance instDecidableEqConstraintStrength : DecidableEq ConstraintStrength

Equations

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

inductive 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 ([Gol06], [LPD25]).

@[implicit_reducible]

instance instReprIslandSource : Repr IslandSource

Equations

• instReprIslandSource = { reprPrec := instReprIslandSource.repr }

def instReprIslandSource.repr : IslandSource → ℕ → 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.semantic prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "IslandSource.semantic")).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✝

@[implicit_reducible]

instance instDecidableEqIslandSource : DecidableEq IslandSource

Equations

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

def Ross1967.embeddedQuestionConstraint : Features.MinimalPairs.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 Ross1967.complexNPConstraint : Features.MinimalPairs.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 Ross1967.adjunctClauseConstraint : Features.MinimalPairs.PhenomenonData

Adjunct constraint: wh-dependencies blocked into adjunct clauses

Equations

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

def Ross1967.coordinateStructureConstraint : Features.MinimalPairs.PhenomenonData

CSC: asymmetric wh-dependencies blocked in coordination

Equations

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

def Ross1967.subjectConstraint : Features.MinimalPairs.PhenomenonData

Subject constraint: wh-dependencies into subjects degraded

Equations

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

def Ross1967.islandData : List Features.MinimalPairs.PhenomenonData

All island constraint data

Equations

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