Islands as Constraints on Rising Catenae

Formalizes [Osb19]'s analysis of islands in dependency grammar: islands are syntactic configurations that constrain which rising catenae can form, limiting the reach of discontinuities. Each island example below exhibits both (i) island material that is itself a catena and (ii) an extraction that produces a risen catena with non-contiguous yield.

Main declarations

• OsborneIslandType — eight island categories from [Osb19] Ch 9.
• islandLeftBranch, islandSubject, islandAdjunct, islandWhIsland, islandSpecifiedNP — minimal DG example trees, one per island type with a worked extraction.
• *_NP_is_catena / *_clause_is_catena — the island material is catena-shaped.
• *_extraction_risen — the extracted-plus-governor pair is a risen catena.

Implementation notes

• Predicates inherit the substrate-wide Bool convention from Catena.lean / Discontinuity.lean; statements are ... = true.
• The OsborneIslandType enum's three cases (adjunct, subject, whIsland) line up with the Ross-1967 inventory in ConstraintType (Studies/Ross1967.lean).

Todo

• Consume the canonical Ross-1967 ConstraintType enum directly so OsborneIslandType becomes a refinement mapping onto it.

Extended island taxonomy

inductive DepGrammar.Islands.OsborneIslandType : Type

Island types from [Osb19], Ch 9. Each variant names the construction whose extraction Osborne's rising-catena constraints rule out.

• leftBranch : OsborneIslandType

  §9.4: *"Whose do you like house?"

• specifiedNP : OsborneIslandType

  §9.6: ??"Who did you find those pictures of?"

• subject : OsborneIslandType

  §9.7: *"Which car did the driver of ignore the light?"

• adjunct : OsborneIslandType

  §9.8: *"What do they always argue before one of them cleans?"

• whIsland : OsborneIslandType

  §9.9: *"Which judge might they inquire which performance surprised?"

• rightRoof : OsborneIslandType

  §9.10: *"That someone was there was a relief who I knew"

• pStranding : OsborneIslandType

  §9.3: *"Wem hast du mit gesprochen?" (German P-stranding)

• piedPiping : OsborneIslandType

  §9.5: pied-piping overcomes left branch islands

def DepGrammar.Islands.instReprOsborneIslandType.repr : OsborneIslandType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance DepGrammar.Islands.instReprOsborneIslandType : Repr OsborneIslandType

Equations

• DepGrammar.Islands.instReprOsborneIslandType = { reprPrec := DepGrammar.Islands.instReprOsborneIslandType.repr }

@[implicit_reducible]

instance DepGrammar.Islands.instDecidableEqOsborneIslandType : DecidableEq OsborneIslandType

Equations

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

Island example trees

Each tree models a sentence where extraction from an island creates a risen catena whose rising catena violates the corresponding island constraint.

def DepGrammar.Islands.islandLeftBranch : DepTree

DG tree for the left-branch island *"Whose do you like house?".

Equations

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

def DepGrammar.Islands.islandSubject : DepTree

DG tree for the subject island *"Which car did the driver of ignore the light?" ([Osb19], §9.7, ex. 48).

Equations

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

def DepGrammar.Islands.islandAdjunct : DepTree

DG tree for the adjunct island *"What do they argue before cleaning?" ([Osb19], §9.8, ex. 50b/59, simplified).

Equations

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

def DepGrammar.Islands.islandWhIsland : DepTree

DG tree for the wh-island *"Which judge might they inquire surprised?" ([Osb19], §9.9, ex. 61b', simplified).

Equations

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

def DepGrammar.Islands.islandSpecifiedNP : DepTree

DG tree for the specified-NP island ??"Who did you find those pictures of?" ([Osb19], §9.6, ex. 36b).

Equations

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

Island material is catena-shaped

Osborne's key insight: islands are syntactic contexts (catenae) that constrain which rising catenae can form. The island material itself is connected.

theorem DepGrammar.Islands.leftBranch_NP_is_catena : Catena.isCatena islandLeftBranch.deps [4] = true

theorem DepGrammar.Islands.subject_NP_is_catena : Catena.isCatena islandSubject.deps [3, 4, 5] = true

theorem DepGrammar.Islands.adjunct_clause_is_catena : Catena.isCatena islandAdjunct.deps [4, 5] = true

theorem DepGrammar.Islands.whIsland_clause_is_catena : Catena.isCatena islandWhIsland.deps [5] = true

theorem DepGrammar.Islands.specifiedNP_is_catena : Catena.isCatena islandSpecifiedNP.deps [4, 5, 6] = true

Extraction creates risen catenae

When extraction reaches into an island, the extracted element and its governor form a risen catena: connected in the tree but with non-contiguous yield. The island constraint blocks the risen catena from being well-formed.

theorem DepGrammar.Islands.leftBranch_extraction_risen : Discontinuity.isRisenCatena islandLeftBranch [0, 4] = true

theorem DepGrammar.Islands.subject_extraction_risen : Discontinuity.isRisenCatena islandSubject [1, 5] = true

theorem DepGrammar.Islands.adjunct_extraction_risen : Discontinuity.isRisenCatena islandAdjunct [0, 5] = true

theorem DepGrammar.Islands.whIsland_extraction_risen : Discontinuity.isRisenCatena islandWhIsland [1, 5] = true

theorem DepGrammar.Islands.specifiedNP_extraction_risen : Discontinuity.isRisenCatena islandSpecifiedNP [0, 6] = true