Islands as Constraints on Rising Catenae

@cite{osborne-2019} @cite{ross-1967}

Formalizes @cite{osborne-2019}'s analysis of islands in dependency grammar. Islands are syntactic configurations that constrain which rising catenae can form — they limit the reach of discontinuities.

Core Insight

In Osborne's framework, discontinuities are analyzed as risen catenae — catenae with non-contiguous yield (see Discontinuity.lean). Islands are constraints on the rising catena (the minimal catena connecting the risen catena to its governor). Different island types constrain rising catenae in different ways:

• Left branch islands (§9.4): The root of a risen catena may not be a determiner, attributive adjective, or degree adverb.
• Subject islands (§9.7): Rising catenae of wh-fronting reluctantly include the subject dependency.
• Adjunct islands (§9.8): Within a rising catena, an adjunct dependency may not dominate a finite verb.
• Wh-islands (§9.9): Wh-expressions are islands to wh-fronting only (not to topicalization or extraposition).
• Specified NP islands (§9.6): Rising catenae cannot easily reach into definite/specific NPs.
• Right roof islands (§9.10): Extraposition is clause-bound; a rising catena of extraposition may not contain more than one finite verb.

Bridges

• → Discontinuity.lean: islands block the formation of risen catenae
• → Catena.lean: island material forms catenae (proven), uses isCatena
• → LongDistance.lean: maps to IslandType (4 shared types + 5 new)

inductive DepGrammar.Islands.OsborneIslandType : Type

Island types (@cite{osborne-2019}, Ch 9). Each type constrains rising catenae in a different way.

• leftBranch : OsborneIslandType
• specifiedNP : OsborneIslandType
• subject : OsborneIslandType
• adjunct : OsborneIslandType
• whIsland : OsborneIslandType
• rightRoof : OsborneIslandType
• pStranding : OsborneIslandType
• piedPiping : OsborneIslandType

instance DepGrammar.Islands.instReprOsborneIslandType : Repr OsborneIslandType

Equations

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

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

Equations

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

instance DepGrammar.Islands.instDecidableEqOsborneIslandType : DecidableEq OsborneIslandType

Equations

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

def DepGrammar.Islands.island_leftBranch : DepTree

Left branch island: *"Whose do you like house?" Words: whose(0) do(1) you(2) like(3) house(4) Deps: do(1) → like(3:ccomp), do(1) → you(2:nsubj), like(3) → house(4:obj), house(4) → whose(0:det)

Risen catena = {whose(0)} — determiner extracted from left branch. Rising catena = {whose(0), do(1),..., house(4)}. The catena {whose(0), house(4)} has non-contiguous yield. Constraint: root of risen catena may NOT be a determiner.

Equations

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

def DepGrammar.Islands.island_subject : DepTree

Subject island: *"Which car did the driver of ignore the traffic light?" (@cite{osborne-2019}, §9.7, example 48) Simplified: "Which car did the driver of ignore the light?" Words: which(0) car(1) did(2) the(3) driver(4) of(5) ignore(6) the_(7) light(8) Deps: did(2) → ignore(6:ccomp), did(2) → driver(4:nsubj), driver(4) → the(3:det), driver(4) → of(5:nmod), of(5) → car(1:nmod), car(1) → which(0:det), ignore(6) → light(8:obj), light(8) → the_(7:det)

Risen catena = {which(0), car(1)} — extracted from inside subject NP. The catena {car(1), of(5)} has non-contiguous yield (did, the, driver intervene). Constraint: rising catena reluctantly includes subject dependency.

Equations

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

def DepGrammar.Islands.island_adjunct : DepTree

Adjunct island: *"What do they always argue before one of them cleans?" (@cite{osborne-2019}, §9.8, example 50b/59) Simplified: "What do they argue before cleaning?" Words: what(0) do(1) they(2) argue(3) before(4) cleaning(5) Deps: do(1) → argue(3:ccomp), do(1) → they(2:nsubj), argue(3) → cleaning(5:advcl), cleaning(5) → before(4:mark), cleaning(5) → what(0:obj)

Risen catena = {what(0)} — extracted from inside adjunct clause. Rising catena contains adjunct dep (argue → cleaning:advcl). The catena {what(0), cleaning(5)} has non-contiguous yield. Constraint: within a rising catena, an adjunct dep may not dominate a finite verb.

Equations

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

def DepGrammar.Islands.island_whIsland : DepTree

Wh-island: *"Which judge might they inquire which performance surprised?" (@cite{osborne-2019}, §9.9, example 61b') Simplified: "Which judge might they inquire surprised?" Words: which(0) judge(1) might(2) they(3) inquire(4) surprised(5) Deps: might(2) → inquire(4:ccomp), might(2) → they(3:nsubj), inquire(4) → surprised(5:ccomp), surprised(5) → judge(1:nsubj), judge(1) → which(0:det)

Risen catena = {which(0), judge(1)} — extracted from embedded wh-clause. The catena {judge(1), surprised(5)} has non-contiguous yield. Constraint: wh-expressions are islands to wh-fronting.

Equations

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

def DepGrammar.Islands.island_specifiedNP : DepTree

Specified NP island: ??"Who did you find those pictures of?" (@cite{osborne-2019}, §9.6, example 36b) Words: who(0) did(1) you(2) find(3) those(4) pictures(5) of(6) Deps: did(1) → find(3:ccomp), did(1) → you(2:nsubj), find(3) → pictures(5:obj), pictures(5) → those(4:det), pictures(5) → of(6:nmod), of(6) → who(0:nmod)

Risen catena = {who(0)} — extracted from inside definite NP. The catena {who(0), of(6)} has non-contiguous yield. Constraint: rising catenae cannot easily reach into specific NPs.

Equations

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

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

The NP containing the left branch {house(4)} is a catena (trivially).

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

The subject NP {the(3), driver(4), of(5)} in the subject island is a catena.

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

The adjunct clause {before(4), cleaning(5)} is a catena.

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

The embedded clause in the wh-island {surprised(5)} is a (trivial) catena.

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

The specified NP {those(4), pictures(5), of(6)} is a catena.

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

Left branch: {whose(0), house(4)} is a risen catena — connected via det but do(1), you(2), like(3) intervene.

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

Subject: {car(1), of(5)} is a risen catena — connected via nmod but did(2), the(3), driver(4) intervene.

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

Adjunct: {what(0), cleaning(5)} is a risen catena — connected via obj but do(1), they(2), argue(3), before(4) intervene.

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

Wh-island: {judge(1), surprised(5)} is a risen catena — connected via nsubj but might(2), they(3), inquire(4) intervene.

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

Specified NP: {who(0), of(6)} is a risen catena — connected via nmod but did(1).pictures(5) intervene.

theorem DepGrammar.Islands.all_island_extractions_risen : Discontinuity.isRisenCatena island_leftBranch [0, 4] = true ∧ Discontinuity.isRisenCatena island_subject [1, 5] = true ∧ Discontinuity.isRisenCatena island_adjunct [0, 5] = true ∧ Discontinuity.isRisenCatena island_whIsland [1, 5] = true ∧ Discontinuity.isRisenCatena island_specifiedNP [0, 6] = true

All island violations produce risen catenae: extraction from an island creates a catena with non-contiguous yield.

def DepGrammar.Islands.toLongDistanceIslandType : OsborneIslandType → Option LongDistance.IslandType

Bridge → LongDistance.lean: Map OsborneIslandType to existing IslandType for the 4 shared types. Osborne's taxonomy is more fine-grained, distinguishing types by their constraints on rising catenae.

Equations

• DepGrammar.Islands.toLongDistanceIslandType DepGrammar.Islands.OsborneIslandType.adjunct = some DepGrammar.LongDistance.IslandType.adjunct
• DepGrammar.Islands.toLongDistanceIslandType DepGrammar.Islands.OsborneIslandType.subject = some DepGrammar.LongDistance.IslandType.subject
• DepGrammar.Islands.toLongDistanceIslandType x✝ = none

theorem DepGrammar.Islands.island_extractions_are_discontinuities : Discontinuity.isRisenCatena island_leftBranch [0, 4] = true ∧ Discontinuity.isRisenCatena island_adjunct [0, 5] = true ∧ Discontinuity.isRisenCatena island_whIsland [1, 5] = true

Bridge → Discontinuity.lean: islands constrain the formation of risen catenae. All island violation examples contain risen catenae (proven above), connecting the island constraint to Osborne's discontinuity theory.

theorem DepGrammar.Islands.all_islands_are_catenae : Catena.isCatena island_leftBranch.deps [4] = true ∧ Catena.isCatena island_subject.deps [3, 4, 5] = true ∧ Catena.isCatena island_adjunct.deps [4, 5] = true ∧ Catena.isCatena island_whIsland.deps [5] = true ∧ Catena.isCatena island_specifiedNP.deps [4, 5, 6] = true

Bridge → Catena.lean: all island material forms catenae. The island is a connected subgraph from which extraction is constrained.