Discontinuities as Risen Catenae

@cite{osborne-2019} @cite{osborne-gross-2012}

Formalizes @cite{osborne-2019}'s analysis of discontinuities in dependency grammar. The central concept is the risen catena: a catena that takes on a word as its head that is not its governor, producing a non-contiguous yield.

Core Concepts

A catena is a connected subgraph of a dependency tree. When a dependent is displaced from its canonical position (e.g., by topicalization, wh-fronting, or extraposition), the displaced element and its governor still form a catena — they are connected in the tree — but their string yield is no longer contiguous: other words intervene. This catena is a risen catena.

The rising catena (@cite{osborne-2019}, Ch 9 §9.2) is the minimal catena that includes the root of the risen catena and the governor of the risen catena. Every discontinuity has a rising catena.

The Rising Principle (@cite{osborne-2019}, Ch 7 §7.12): The head of the risen catena must dominate the governor of the risen catena. This constrains which discontinuities are possible.

Discontinuity Types (Ch 8)

Osborne identifies five types:

• Wh-fronting: "Which song do you like?" — constituent rising
• Topicalization: "That song, you don't like" — constituent rising
• NP-internal fronting: "too difficult (of) a problem" — non-constituent rising
• Scrambling: German "dass uns Maria etwas gebacken hat" — constituent rising
• Extraposition: "The idea arose to try again" — constituent rising

Rising vs. lowering: wh-fronting, topicalization, and scrambling displace leftward (rising); extraposition displaces rightward (lowering).

Bridges

• → Catena.lean: risen catenae are catenae with non-contiguous yield
• → NonProjective.lean: arc-crossing non-projectivity is a stricter notion; risen catenae generalize it
• → LongDistance.lean: topicalization and wh-fronting map to GapType.objGap

inductive DepGrammar.Discontinuity.DiscontinuityType : Type

Discontinuity types (Ch 8, Table 19).

• whFronting : DiscontinuityType
• topicalization : DiscontinuityType
• npInternalFront : DiscontinuityType
• scrambling : DiscontinuityType
• extraposition : DiscontinuityType

def DepGrammar.Discontinuity.instReprDiscontinuityType.repr : DiscontinuityType → ℕ → Std.Format

Equations

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

instance DepGrammar.Discontinuity.instReprDiscontinuityType : Repr DiscontinuityType

Equations

• DepGrammar.Discontinuity.instReprDiscontinuityType = { reprPrec := DepGrammar.Discontinuity.instReprDiscontinuityType.repr }

instance DepGrammar.Discontinuity.instDecidableEqDiscontinuityType : DecidableEq DiscontinuityType

Equations

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

inductive DepGrammar.Discontinuity.DisplacementDir : Type

Direction of displacement relative to canonical position. : wh-fronting, topicalization, NP-internal fronting, and scrambling displace leftward; extraposition displaces rightward.

• rising : DisplacementDir
• lowering : DisplacementDir

instance DepGrammar.Discontinuity.instReprDisplacementDir : Repr DisplacementDir

Equations

• DepGrammar.Discontinuity.instReprDisplacementDir = { reprPrec := DepGrammar.Discontinuity.instReprDisplacementDir.repr }

def DepGrammar.Discontinuity.instReprDisplacementDir.repr : DisplacementDir → ℕ → Std.Format

Equations

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

instance DepGrammar.Discontinuity.instDecidableEqDisplacementDir : DecidableEq DisplacementDir

Equations

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

def DepGrammar.Discontinuity.displacementDir : DiscontinuityType → DisplacementDir

Classify a discontinuity type by its displacement direction. Scrambling can go either direction, but the canonical case is leftward.

Equations

• DepGrammar.Discontinuity.displacementDir DepGrammar.Discontinuity.DiscontinuityType.whFronting = DepGrammar.Discontinuity.DisplacementDir.rising
• DepGrammar.Discontinuity.displacementDir DepGrammar.Discontinuity.DiscontinuityType.topicalization = DepGrammar.Discontinuity.DisplacementDir.rising
• DepGrammar.Discontinuity.displacementDir DepGrammar.Discontinuity.DiscontinuityType.npInternalFront = DepGrammar.Discontinuity.DisplacementDir.rising
• DepGrammar.Discontinuity.displacementDir DepGrammar.Discontinuity.DiscontinuityType.scrambling = DepGrammar.Discontinuity.DisplacementDir.rising
• DepGrammar.Discontinuity.displacementDir DepGrammar.Discontinuity.DiscontinuityType.extraposition = DepGrammar.Discontinuity.DisplacementDir.lowering

inductive DepGrammar.Discontinuity.RisingType : Type

Whether a discontinuity type involves constituent or non-constituent rising. : constituent rising = risen catena is a constituent; non-constituent rising = risen catena is not a constituent.

• constituent : RisingType
• nonConstituent : RisingType

instance DepGrammar.Discontinuity.instReprRisingType : Repr RisingType

Equations

• DepGrammar.Discontinuity.instReprRisingType = { reprPrec := DepGrammar.Discontinuity.instReprRisingType.repr }

def DepGrammar.Discontinuity.instReprRisingType.repr : RisingType → ℕ → Std.Format

Equations

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

instance DepGrammar.Discontinuity.instDecidableEqRisingType : DecidableEq RisingType

Equations

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

def DepGrammar.Discontinuity.isContiguous (nodes : List ℕ) : Bool

Check if a list of node indices is contiguous (no gaps in the sequence). Delegates to isInterval from Core/Basic.lean after sorting.

Equations

• DepGrammar.Discontinuity.isContiguous nodes = DepGrammar.isInterval (nodes.mergeSort fun (x1 x2 : ℕ) => decide (x1 ≤ x2))

def DepGrammar.Discontinuity.isRisenCatena (t : DepTree) (nodes : List ℕ) : Bool

A risen catena (Ch 7 §7.10) is a catena whose string yield is not contiguous — the catena is connected in the dependency tree but its words are separated by intervening material in linear order.

This is the core formalization of Osborne's "discontinuity": when a dependent is displaced, it and its governor remain a catena, but the catena's yield is no longer contiguous.

Equations

• DepGrammar.Discontinuity.isRisenCatena t nodes = (DepGrammar.Catena.isCatena t.deps nodes && !DepGrammar.Discontinuity.isContiguous nodes)

def DepGrammar.Discontinuity.classifyDisplacement (d : Dependency) : DisplacementDir

Classify a dependency as rising or lowering based on whether the dependent precedes or follows its head in linear order. .

Equations

• DepGrammar.Discontinuity.classifyDisplacement d = if d.depIdx < d.headIdx then DepGrammar.Discontinuity.DisplacementDir.rising else DepGrammar.Discontinuity.DisplacementDir.lowering

def DepGrammar.Discontinuity.whFrontingTree : DepTree

Wh-fronting: "What did you eat?" (Ch 8 §8.2) Words: what(0) did(1) you(2) eat(3) Deps: eat(3) → you(2:nsubj), eat(3) → what(0:obj), eat(3) → did(1:aux)

Risen catena = {what(0)} — displaced to sentence-initial position. Rising catena = {what(0), did(1), you(2), eat(3)} — minimal catena from risen catena root to governor eat(3). The catena {what(0), eat(3)} has non-contiguous yield.

Equations

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

def DepGrammar.Discontinuity.whFrontingArc : Dependency

The displaced dependency: eat(3) → what(0).

Equations

• DepGrammar.Discontinuity.whFrontingArc = { headIdx := 3, depIdx := 0, depType := UD.DepRel.obj }

def DepGrammar.Discontinuity.topicalizationTree : DepTree

Topicalization: "...but those ideas I do accept" (Ch 8 §8.3) Simplified to core: "Those ideas I do accept" Words: those(0) ideas(1) I(2) do(3) accept(4) Deps: accept(4) → I(2:nsubj), accept(4) → do(3:aux), accept(4) → ideas(1:obj), ideas(1) → those(0:det)

Risen catena = {those(0), ideas(1)} — topicalized NP. Rising catena connects risen catena to governor accept(4). The catena {ideas(1), accept(4)} has non-contiguous yield.

Equations

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

def DepGrammar.Discontinuity.topicalizationArc : Dependency

The displaced dependency: accept(4) → ideas(1).

Equations

• DepGrammar.Discontinuity.topicalizationArc = { headIdx := 4, depIdx := 1, depType := UD.DepRel.obj }

def DepGrammar.Discontinuity.scramblingTree : DepTree

Scrambling (German): "dass uns Maria etwas gebacken hat" (that us Maria something baked has) Words: dass(0) uns(1) Maria(2) etwas(3) gebacken(4) hat(5) Deps: dass(0) → hat(5:...), hat(5) → gebacken(4:xcomp), gebacken(4) → Maria(2:nsubj), gebacken(4) → etwas(3:obj), gebacken(4) → uns(1:iobj)

Risen catena = {uns(1)} — scrambled to pre-subject position. The catena {uns(1), gebacken(4)} has non-contiguous yield. .

Equations

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

def DepGrammar.Discontinuity.extrapositionTree : DepTree

Extraposition: "The idea arose to try again" (Ch 8 §8.6) Words: the(0) idea(1) arose(2) to(3) try(4) again(5) Deps: arose(2) → idea(1:nsubj), idea(1) → the(0:det), idea(1) → try(4:acl), try(4) → to(3:mark), try(4) → again(5:advmod)

Risen catena = {to(3), try(4), again(5)} — extraposed infinitival. The catena {idea(1), try(4)} has non-contiguous yield: arose(2), to(3) intervene. Lowering displacement.

Equations

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

def DepGrammar.Discontinuity.extrapositionArc : Dependency

The displaced dependency: idea(1) → try(4).

Equations

• DepGrammar.Discontinuity.extrapositionArc = { headIdx := 1, depIdx := 4, depType := UD.DepRel.acl }

def DepGrammar.Discontinuity.rightDislocationTree : DepTree

Right dislocation: "He's nice, that boy" Words: he(0) is(1) nice(2) that(3) boy(4) Deps: nice(2) → he(0:nsubj), nice(2) → is(1:cop), nice(2) → boy(4:dislocated), boy(4) → that(3:det)

The catena {nice(2), boy(4)} — the predicate and its dislocated dependent — has non-contiguous yield (that(3) intervenes).

Equations

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

theorem DepGrammar.Discontinuity.whFronting_risen_catena : isRisenCatena whFrontingTree [0, 3] = true

Wh-fronting: {what(0), eat(3)} is a risen catena — connected via obj but did(1), you(2) intervene in the yield.

theorem DepGrammar.Discontinuity.topicalization_risen_catena : isRisenCatena topicalizationTree [1, 4] = true

Topicalization: {ideas(1), accept(4)} is a risen catena — connected via obj but I(2), do(3) intervene.

theorem DepGrammar.Discontinuity.scrambling_risen_catena : isRisenCatena scramblingTree [1, 4] = true

Scrambling: {uns(1), gebacken(4)} is a risen catena — connected via iobj but Maria(2), etwas(3) intervene.

theorem DepGrammar.Discontinuity.extraposition_risen_catena : isRisenCatena extrapositionTree [1, 4] = true

Extraposition: {idea(1), try(4)} is a risen catena — connected via acl but arose(2), to(3) intervene.

theorem DepGrammar.Discontinuity.rightDislocation_risen_catena : isRisenCatena rightDislocationTree [2, 4] = true

Right dislocation: {nice(2), boy(4)} is a risen catena — connected via dislocated dep but that(3) intervenes in the yield.

theorem DepGrammar.Discontinuity.all_discontinuities_are_risen_catenae : isRisenCatena whFrontingTree [0, 3] = true ∧ isRisenCatena topicalizationTree [1, 4] = true ∧ isRisenCatena scramblingTree [1, 4] = true ∧ isRisenCatena extrapositionTree [1, 4] = true ∧ isRisenCatena rightDislocationTree [2, 4] = true

: all discontinuity types produce risen catenae.

theorem DepGrammar.Discontinuity.whFronting_is_rising : classifyDisplacement whFrontingArc = DisplacementDir.rising

Wh-fronting is rising: what(0) precedes eat(3).

theorem DepGrammar.Discontinuity.topicalization_is_rising : classifyDisplacement topicalizationArc = DisplacementDir.rising

Topicalization is rising: ideas(1) precedes accept(4).

theorem DepGrammar.Discontinuity.extraposition_is_lowering : classifyDisplacement extrapositionArc = DisplacementDir.lowering

Extraposition is lowering: try(4) follows idea(1).

theorem DepGrammar.Discontinuity.rising_types : displacementDir DiscontinuityType.whFronting = DisplacementDir.rising ∧ displacementDir DiscontinuityType.topicalization = DisplacementDir.rising ∧ displacementDir DiscontinuityType.npInternalFront = DisplacementDir.rising ∧ displacementDir DiscontinuityType.scrambling = DisplacementDir.rising

Rising discontinuities: wh-fronting, topicalization, NP-internal fronting, scrambling. (Ch 8 Table 19).

theorem DepGrammar.Discontinuity.lowering_types : displacementDir DiscontinuityType.extraposition = DisplacementDir.lowering

Lowering discontinuity: extraposition. (Ch 8 Table 19).

theorem DepGrammar.Discontinuity.displaced_pairs_are_catenae : Catena.isCatena whFrontingTree.deps [0, 3] = true ∧ Catena.isCatena topicalizationTree.deps [1, 4] = true ∧ Catena.isCatena scramblingTree.deps [1, 4] = true ∧ Catena.isCatena extrapositionTree.deps [1, 4] = true

Bridge → Catena.lean: all displaced element + governor pairs form catenae. The catena structure is what allows Osborne's analysis — even though the yield is non-contiguous, the syntactic connection remains.

theorem DepGrammar.Discontinuity.wh_fronting_is_obj_gap : LongDistance.gapToDepRel LongDistance.GapType.objGap = UD.DepRel.obj

Bridge → LongDistance.lean: wh-fronting and topicalization involve object extraction, mapping to GapType.objGap.

theorem DepGrammar.Discontinuity.nonProjective_tree_also_risen : isRisenCatena nonProjectiveTree [0, 2] = true

Bridge → NonProjective.lean: risen catenae generalize arc-crossing non-projectivity. The nonProjectiveTree from NonProjective.lean has arcs 0→2 and 1→3 — these genuinely cross AND produce risen catenae. Osborne's single-clause examples produce risen catenae without crossing arcs.