Discontinuities as risen catenae

[Osb19] [OG12]

A risen catena ([Osb19], Ch 7 §7.10) is a catena whose string yield is not contiguous: the catena is connected in the dependency graph but intervening words separate it in linear order. Osborne treats every discontinuity (wh-fronting, topicalization, scrambling, extraposition, right dislocation) as a risen catena, replacing the movement transformations of phrase-structure grammar with a single tree-level predicate.

Main definitions

• DiscontinuityType — Osborne's Ch 8 taxonomy (five constructions).
• DisplacementDir — rising vs. lowering displacement.
• isContiguous, isRisenCatena — predicates over node lists.
• classifyDisplacement, displacementDir — direction lookups.
• Example trees whFrontingTree, topicalizationTree, scramblingTree, extrapositionTree, rightDislocationTree.

Main theorems

• whFronting_risen_catena, topicalization_risen_catena, scrambling_risen_catena, extraposition_risen_catena, rightDislocation_risen_catena — each example tree carries a risen catena over the indicated node pair.

Implementation notes

• isContiguous and isRisenCatena return Bool to match the substrate-wide Catena.isCatena convention; a project-level Bool → Prop migration would refactor Catena.lean first.
• isContiguous delegates to isInterval after insertionSort so kernel decide proofs reduce; see Syntax/DependencyGrammar/Projection.lean.

Discontinuity classification

inductive DepGrammar.Discontinuity.DiscontinuityType : Type

Discontinuity types ([Osb19], 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.

@[implicit_reducible]

instance DepGrammar.Discontinuity.instReprDiscontinuityType : Repr DiscontinuityType

Equations

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

@[implicit_reducible]

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

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

Equations

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

@[implicit_reducible]

instance DepGrammar.Discontinuity.instReprDisplacementDir : Repr DisplacementDir

Equations

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

@[implicit_reducible]

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; 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

Risen catenae

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

A list of node indices is contiguous iff its sorted form is an interval. Uses insertionSort (not mergeSort) so downstream decide proofs reduce in the kernel.

Equations

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

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

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

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 by 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

Example trees from [Osb19] Ch 8

def DepGrammar.Discontinuity.whFrontingTree : DepTree

Wh-fronting: "What did you eat?". The catena {what(0), eat(3)} is risen — connected via obj but did(1), you(2) intervene.

Equations

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

def DepGrammar.Discontinuity.whFrontingArc : Dependency

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

Equations

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

def DepGrammar.Discontinuity.topicalizationTree : DepTree

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

Equations

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

def DepGrammar.Discontinuity.topicalizationArc : Dependency

The displaced dependency in topicalizationTree: 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". The catena {uns(1), gebacken(4)} is risen — uns is scrambled past the subject.

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". The catena {idea(1), try(4)} is risen — arose(2), to(3) intervene. Lowering.

Equations

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

def DepGrammar.Discontinuity.extrapositionArc : Dependency

The displaced dependency in extrapositionTree: 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". The catena {nice(2), boy(4)} is risen — that(3) intervenes.

Equations

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

Risen-catena theorems

Each example tree carries a risen catena over the displaced-element / governor pair: connected via the dependency edge but yielding non-contiguously.

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

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

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

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

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

Displacement direction

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

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

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