Documentation

Linglib.Discourse.Centering.Transition

Centering Theory — Transitions #

[GJW95] The three transition types (continuation / retaining / shifting) and their classification. classifyTransitionStrict is faithful to GJW Def 4; classifyTransitionExtended applies the worked-example convention for the segment-initial case.

Transition Type #

source
inductive Discourse.Centering.Transition :
Type

Three transition types between consecutive utterances ([GJW95] Def 4).

Instances For
    source
    @[implicit_reducible]
    instance Discourse.Centering.instDecidableEqTransition :
    DecidableEq Transition
    Equations
    source
    @[implicit_reducible]
    instance Discourse.Centering.instReprTransition :
    Repr 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
      def Discourse.Centering.Transition.rank :
      Transition → ℕ

      Rule 2 preference order: continuation > retaining > shifting.

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

        LinearOrder via rank, exposing <, ≤, max for Rule 2 statements.

        Equations
        source
        theorem Discourse.Centering.continuation_gt_retaining :
        Transition.continuation > Transition.retaining
        source
        theorem Discourse.Centering.retaining_gt_shifting :
        Transition.retaining > Transition.shifting

        Strict and Extended Classification #

        source
        def Discourse.Centering.classifyTransitionInternal {E : Type u_1} [DecidableEq E] (curCb : E) (curCp : Option E) (prevCb : E) :
        Transition

        Internal classifier given both Cbs: equal Cbs continue/retain by 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 : Type u_1} {R : Type u_2} [DecidableEq E] [CfRankerOf E R] {U : Type u_3} [Realizes U E] (prev : Utterance E R) (cur : U) (curCp prevCb : Option E) :
          Option Transition

          Strict classification (faithful to GJW Def 4): returns none in the segment-initial case where the prior Cb is undefined.

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

            Extended classification: applies the worked-example convention for the segment-initial case (treats missing prior Cb as if equal to current Cb).

            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 : Type u_1} {R : Type u_2} [DecidableEq E] [CfRankerOf E R] {U : Type u_3} [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.