Documentation

Linglib.Discourse.Centering.Transition

Centering Theory — Transitions #

[GJW95] [Str98] [BFP87]

The three transition types (continuation / retaining / shifting), their classification, the discourse-level scan (transitions, cbs, coherenceScore), and their preference structure: the LinearOrder and pairRank ("Rule 2" of [GJW95], stated over sequences) and [Str98]'s cheap/expensive distinction (isCheap). classifyTransitionStrict is faithful to GJW Def 4; classifyTransitionExtended applies the worked-example convention for the segment-initial case. The [BFP87] 4-way variant lives in Studies/PoesioEtAl2004.lean.

Transition Type #

source
inductive Discourse.Centering.Transition :
Type

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

Instances For
    source
    @[instance_reducible]
    instance Discourse.Centering.instDecidableEqTransition :
    DecidableEq Transition
    Equations
    source
    @[instance_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
        @[instance_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.classifyTransitionStrict {E : Type u_1} {R : Type u_2} [DecidableEq E] [CfRankerOf E R] (prev cur : Utterance E R) (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] (prev cur : Utterance E R) (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] (prev cur : Utterance E R) (prevCb : Option E) (t : Transition) (h : classifyTransitionStrict prev cur prevCb = some t) :
            classifyTransitionExtended prev cur prevCb = t

            The two classifications agree whenever the strict variant is defined.

            Discourse-level scan #

            source
            def Discourse.Centering.cbs {E : Type u_1} {R : Type u_2} [DecidableEq E] [CfRankerOf E R] :
            List (Utterance E R) → List (Option E)

            The backward-looking center of each adjacent pair along a discourse.

            Equations
            Instances For
              source
              def Discourse.Centering.transitionsFrom {E : Type u_1} {R : Type u_2} [DecidableEq E] [CfRankerOf E R] (prevCb : Option E) :
              List (Utterance E R) → List Transition

              Transition sequence along a discourse from a given prior Cb, threading each pair's Cb as the next pair's prior Cb.

              Equations
              Instances For
                source
                def Discourse.Centering.transitions {E : Type u_1} {R : Type u_2} [DecidableEq E] [CfRankerOf E R] (d : List (Utterance E R)) :
                List Transition

                Transition sequence of a discourse segment (segment-initial prior Cb undefined).

                Equations
                Instances For
                  source
                  def Discourse.Centering.coherenceScore {E : Type u_1} {R : Type u_2} [DecidableEq E] [CfRankerOf E R] (d : List (Utterance E R)) :
                  ℕ

                  Sum-of-ranks coherence measure over a discourse's transition sequence — the sequence form of "Rule 2" ([GJW95]).

                  Equations
                  Instances For

                    Transition preference #

                    source
                    def Discourse.Centering.pairRank (t₁ t₂ : Transition) :
                    ℕ

                    Sequence preference ("Rule 2" of [GJW95]) compares pairs of transitions by sum-of-ranks.

                    Equations
                    Instances For
                      source
                      def Discourse.Centering.isCheap {E : Type u_1} {R : Type u_2} [CfRankerOf E R] {U : Type u_3} [Realizes U E] (prev : Utterance E R) (cur : U) (prevCp : Option E) :
                      Prop

                      A transition is cheap ([Str98]) if CB(U_n) = CP(U_{n-1}): the previous utterance's preferred center predicts the current CB.

                      Equations
                      Instances For
                        source
                        @[instance_reducible]
                        instance Discourse.Centering.isCheap.decidable {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) (prevCp : Option E) :
                        Decidable (isCheap prev cur prevCp)
                        Equations