Documentation

Linglib.Theories.Discourse.Centering.Transition

Centering Theory — Transitions #

@cite{grosz-joshi-weinstein-1995} §3, §4

The three transition types and their classification, split into a strict version (paper Definition 4) and an extended version (paper convention for the segment-initial case).

Why a split? #

@cite{grosz-joshi-weinstein-1995} Definition 4 only classifies transitions where both Cb(U_n) and Cb(U_{n+1}) exist. The paper also discusses segment-initial transitions where the prior Cb is undefined; for these, the worked examples (e.g., Discourses 1 and 20) implicitly use a "treat-as-continuation when Cb=Cp" convention. We make this distinction explicit:

The earlier monolithic classifyTransition (in the study file) was the extended version; downstream code that needs the strict reading should use the strict variant.

Rule 2 (transition preference: continuation > retaining > shifting) lives in Rules.lean.

source
inductive Discourse.Centering.Transition :
Type

Three transition types between U_n and U_{n+1} (@cite{grosz-joshi-weinstein-1995} §3, Def 4):

  • continuation: Cb(U_{n+1}) = Cb(U_n) AND Cb(U_{n+1}) is the most-highly-ranked element of Cf(U_{n+1}).
  • retaining: Cb(U_{n+1}) = Cb(U_n), but is not the most-highly-ranked element of Cf(U_{n+1}).
  • shifting: Cb(U_{n+1}) ≠ Cb(U_n) (including the case where no Cb of U_{n+1} exists, by convention).
Instances For
    source
    @[implicit_reducible]
    instance Discourse.Centering.instDecidableEqTransition :
    DecidableEq Transition
    Equations
    source
    def Discourse.Centering.instReprTransition.repr :
    Transition → ℕ → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[implicit_reducible]
      instance Discourse.Centering.instReprTransition :
      Repr Transition
      Equations
      source
      def Discourse.Centering.Transition.rank :
      Transition → ℕ

      @cite{grosz-joshi-weinstein-1995} Rule 2 preference order: continuation > retaining > shifting.

      Equations
      Instances For
        source
        @[implicit_reducible]
        instance Discourse.Centering.instLinearOrderTransition :
        LinearOrder Transition

        Why a LinearOrder (not just a Bool comparator)? Rule 2 is fundamentally a preference relation: given two candidate next utterances, the centering-preferred one is whichever yields the higher-ranked transition. Exposing this as LinearOrder (via LinearOrder.lift' over the Nat rank) makes <, ≤, max, and Decidable comparisons available for free, and lets downstream code state Rule 2 with the standard order vocabulary instead of a bespoke prefersOver : Transition → Transition → Bool.

        Equations
        source
        theorem Discourse.Centering.continuation_gt_retaining :
        Transition.continuation > Transition.retaining
        source
        theorem Discourse.Centering.retaining_gt_shifting :
        Transition.retaining > Transition.shifting
        source
        def Discourse.Centering.classifyTransitionInternal {E : Type} [DecidableEq E] (curCb : E) (curCp : Option E) (prevCb : E) :
        Transition

        Internal transition classifier, given that both Cbs are known. Captures the segment-internal case shared by the strict and extended versions: equal Cbs continue/retain (depending on Cp alignment); unequal Cbs shift.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Discourse.Centering.classifyTransitionStrict {E R : Type} [DecidableEq E] [CfRankerOf E R] {U : Type} [Realizes U E] (prev : Utterance E R) (cur : U) (curCp prevCb : Option E) :
          Option Transition

          Strict transition classification, faithful to @cite{grosz-joshi-weinstein-1995} Def 4: returns none precisely when the paper's definition is silent (segment-initial case where the prior Cb is undefined but the current Cb exists).

          Equations
          Instances For
            source
            def Discourse.Centering.classifyTransitionExtended {E R : Type} [DecidableEq E] [CfRankerOf E R] {U : Type} [Realizes U E] (prev : Utterance E R) (cur : U) (curCp prevCb : Option E) :
            Transition

            Extended transition classification, applying the worked-example convention for the segment-initial case (paper §4): when there is no prior Cb, treat it as if prevCb = curCb so the segment-initial pair becomes a continuation iff the current Cb equals the current Cp, and a retaining otherwise.

            This matches the labels used in the paper for Discourses 1 and 20 even though Definition 4 does not formally cover the segment-initial pair.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              theorem Discourse.Centering.extended_eq_strict_when_defined {E R : Type} [DecidableEq E] [CfRankerOf E R] {U : Type} [Realizes U E] (prev : Utterance E R) (cur : U) (curCp prevCb : Option E) (t : Transition) (h : classifyTransitionStrict prev cur curCp prevCb = some t) :
              classifyTransitionExtended prev cur curCp prevCb = t

              The two classifications agree whenever the strict variant is defined. Both delegate to classifyTransitionInternal in the segment-internal case, so the agreement is essentially by construction; only the curCb = none and segment-initial branches need handling.