Discourse Segments — DSP Stack

@cite{grosz-sidner-1986} @cite{grosz-joshi-weinstein-1995}

A theory-neutral type for the discourse segment purpose (DSP) stack of @cite{grosz-sidner-1986}. Segments organize a discourse into a tree of purposes; the DSP stack tracks which segment is currently active during processing.

Centering theory @cite{grosz-joshi-weinstein-1995} is explicitly local to a single segment: Cf, Cb, and the transition typology only apply to adjacent utterances within the same segment. Cross-segment transitions are governed by the segment-structure level instead. This module provides the minimal scaffolding (the stack and basic push/pop operations) that downstream Centering and SDRT files can hook into without committing to a specific account of segment boundaries.

Segment-purpose semantics — what makes a sequence of utterances a single purpose, how purposes are introduced and terminated — is not fixed here; this module provides the bookkeeping layer.

structure Core.Discourse.Segment.Segment (P : Type) : Type

A discourse segment, parameterized by the purpose-content type P. The id distinguishes co-purposed segments (two distinct segments can share a purpose-description but be different segments).

• id : Nat
• purpose : P

@[implicit_reducible]

instance Core.Discourse.Segment.instReprSegment {P✝ : Type} [Repr P✝] : Repr (Segment P✝)

Equations

• Core.Discourse.Segment.instReprSegment = { reprPrec := Core.Discourse.Segment.instReprSegment.repr }

def Core.Discourse.Segment.instReprSegment.repr {P✝ : Type} [Repr P✝] : Segment P✝ → Nat → Std.Format

Equations

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

@[reducible, inline]

abbrev Core.Discourse.Segment.DSPStack (P : Type) : Type

The discourse-segment-purpose stack: most recently pushed segment is at the head. The empty stack represents the discourse-initial state (before any purpose has been opened).

Equations

• Core.Discourse.Segment.DSPStack P = List (Core.Discourse.Segment.Segment P)

def Core.Discourse.Segment.DSPStack.current {P : Type} (s : DSPStack P) : Option (Segment P)

The currently active segment (top of the stack), or none if the stack is empty.

Equations

• s.current = List.head? s

def Core.Discourse.Segment.DSPStack.push {P : Type} (s : DSPStack P) (seg : Segment P) : DSPStack P

Push a new segment onto the stack — beginning a new sub-purpose.

Equations

• s.push seg = seg :: s

def Core.Discourse.Segment.DSPStack.pop {P : Type} : DSPStack P → DSPStack P

Pop the topmost segment — terminating the current purpose and returning to the dominating one. Returns the original stack unchanged if it was already empty.

Equations

• Core.Discourse.Segment.DSPStack.pop [] = []
• Core.Discourse.Segment.DSPStack.pop (head :: xs) = xs

def Core.Discourse.Segment.DSPStack.coSegmental {P : Type} [DecidableEq P] (s₁ s₂ : DSPStack P) : Bool

Two utterances are co-segmental when they are processed under the same active segment. Centering operations are restricted to co-segmental utterance pairs.

Equations

• s₁.coSegmental s₂ = match List.head? s₁, List.head? s₂ with | some a, some b => a.id == b.id | none, none => true | x, x_1 => false