Documentation

Linglib.Discourse.Centering.Transition

Centering theory: transitions #

Grosz, Joshi, and Weinstein classify the move from one utterance to the next by whether the backward-looking center is kept and, if so, whether it is the preferred center: continuation, retaining, or shifting. Rule 2 orders the three, continuation first, and prefers sequences of earlier transitions to sequences of later ones. This file classifies a pair of utterances from its centers, scans a discourse for the centers and transitions of each utterance after the first, and carries Rule 2's order as the LinearOrder on Transition.

Main declarations #

Implementation notes #

The paper's definitions presuppose a prior backward-looking center. When there is none, as for the second utterance of a segment, the center counts as kept, so the utterance continues or retains according to whether its center is its preferred center: the proposal of Walker, Iida, and Cote that [PSDEH04] reports, on which the first utterance's center is underspecified until the second is processed. An utterance with no backward-looking center shifts, as the paper's shifting clause reads when the center is undefined.

Rule 2 prefers sequences of continuations to sequences of retentions and those to sequences of shifts, and in particular prefers a pair of continuations to a pair of retentions. The order on Transition is its content on single transitions; a study compares sequences by that order pointwise.

References #

source
inductive Discourse.Centering.Transition :
Type

The transition into an utterance: its backward-looking center is kept and is its preferred center, kept but not preferred, or changed.

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's rank: continuation over retaining over shifting.

      Equations
      Instances For
        source
        @[instance_reducible]
        instance Discourse.Centering.Transition.instLinearOrder :
        LinearOrder Transition

        Rule 2's order on single transitions, continuation the greatest.

        Equations
        source
        theorem Discourse.Centering.Transition.retaining_lt_continuation :
        retaining < continuation
        source
        theorem Discourse.Centering.Transition.shifting_lt_retaining :
        shifting < retaining
        source
        def Discourse.Centering.Transition.ofCenters {E : Type u_1} [DecidableEq E] :
        Option E → Option E → Option E → Transition

        The transition determined by the prior backward-looking center, the current one, and the current preferred center. The center is kept when it is defined and, if the prior center is defined, equal to it.

        Equations
        Instances For
          source
          @[simp]
          theorem Discourse.Centering.Transition.ofCenters_none {E : Type u_1} [DecidableEq E] (prevCb curCp : Option E) :
          ofCenters prevCb none curCp = shifting
          source
          theorem Discourse.Centering.Transition.ofCenters_some {E : Type u_1} [DecidableEq E] (prevCb curCp : Option E) (c : E) :
          ofCenters prevCb (some c) curCp = if ∀ (p : E), p ∈ prevCb → p = c then if curCp = some c then continuation else retaining else shifting
          source
          theorem Discourse.Centering.Transition.ofCenters_some_some {E : Type u_1} [DecidableEq E] (p c : E) (curCp : Option E) :
          ofCenters (some p) (some c) curCp = if p = c then if curCp = some c then continuation else retaining else shifting

          A defined prior center gives the paper's three-way classification.

          source
          def Discourse.Centering.transition {E : Type u_1} {R : Type u_2} [DecidableEq E] [LinearOrder R] (prevCb : Option E) (prev cur : Utterance E R) :
          Transition

          The transition into cur from prev, given the backward-looking center of prev.

          Equations
          Instances For

            Scanning a discourse #

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

            The backward-looking center of each utterance of d after the first.

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

              The transition into each utterance of d after the first, the first of them with no prior center.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                @[simp]
                theorem Discourse.Centering.cbs_nil {E : Type u_1} {R : Type u_2} [DecidableEq E] [LinearOrder R] :
                cbs [] = []
                source
                @[simp]
                theorem Discourse.Centering.cbs_singleton {E : Type u_1} {R : Type u_2} [DecidableEq E] [LinearOrder R] (u : Utterance E R) :
                cbs [u] = []
                source
                @[simp]
                theorem Discourse.Centering.cbs_cons_cons {E : Type u_1} {R : Type u_2} [DecidableEq E] [LinearOrder R] (u₁ u₂ : Utterance E R) (d : List (Utterance E R)) :
                cbs (u₁ :: u₂ :: d) = cb u₁ u₂ :: cbs (u₂ :: d)
                source
                @[simp]
                theorem Discourse.Centering.length_cbs {E : Type u_1} {R : Type u_2} [DecidableEq E] [LinearOrder R] (d : List (Utterance E R)) :
                (cbs d).length = d.length - 1
                source
                @[simp]
                theorem Discourse.Centering.transitions_nil {E : Type u_1} {R : Type u_2} [DecidableEq E] [LinearOrder R] :
                transitions [] = []
                source
                @[simp]
                theorem Discourse.Centering.transitions_singleton {E : Type u_1} {R : Type u_2} [DecidableEq E] [LinearOrder R] (u : Utterance E R) :
                transitions [u] = []
                source
                theorem Discourse.Centering.transitions_cons_cons {E : Type u_1} {R : Type u_2} [DecidableEq E] [LinearOrder R] (u₁ u₂ : Utterance E R) (d : List (Utterance E R)) :
                transitions (u₁ :: u₂ :: d) = transition none u₁ u₂ :: List.zipWith3 Transition.ofCenters (cbs (u₁ :: u₂ :: d)) (cbs (u₂ :: d)) (List.map Utterance.cp d)

                Each transition after the first threads the previous pair's center as its prior center.

                source
                @[simp]
                theorem Discourse.Centering.length_transitions {E : Type u_1} {R : Type u_2} [DecidableEq E] [LinearOrder R] (d : List (Utterance E R)) :
                (transitions d).length = d.length - 1