Documentation

Linglib.Discourse.Centering.Rule1

Centering Theory — Rule 1 (Pronominalization Constraint) #

[GJW95] [GGG93] [PSDEH04] Three variants of Rule 1, each making a different empirical claim: GJW 95 (conditional on any pronominalization), GJW 83 (conditional on CB stability), Gordon (unconditional). Each is its own predicate with implication theorems where they hold.

Rule 1 (GJW 1995) — the standard formulation #

source
def Discourse.Centering.Rule1GJW95 {E : Type u_1} {R : Type u_2} [DecidableEq E] [CfRankerOf E R] {U : Type u_3} [Realizes U E] [Pronominalizes U E] (prev : Utterance E R) (cur : U) :
Prop

Rule 1 (GJW 95): if any element of Cf(U_{i-1}) is pronominalized in U_i, then Cb(U_i) is pronominalized too. Vacuously satisfied when no Cb exists.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[implicit_reducible]
    instance Discourse.Centering.Rule1GJW95.decidable {E : Type u_1} {R : Type u_2} [DecidableEq E] [CfRankerOf E R] {U : Type u_3} [Realizes U E] [Pronominalizes U E] (prev : Utterance E R) (cur : U) :
    Decidable (Rule1GJW95 prev cur)
    Equations
    • One or more equations did not get rendered due to their size.

    Rule 1 (GJW 1983) — conditional on CB stability #

    source
    def Discourse.Centering.Rule1GJW83 {E : Type u_1} {R : Type u_2} [DecidableEq E] [CfRankerOf E R] {U : Type u_3} [Realizes U E] [Pronominalizes U E] (prev : Utterance E R) (cur : U) (prevCb : Option E) :
    Prop

    Rule 1 (GJW 83): if the current CB equals the previous CB, use a pronoun. Conditional on CB stability; prevCb is an explicit parameter.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[implicit_reducible]
      instance Discourse.Centering.Rule1GJW83.decidable {E : Type u_1} {R : Type u_2} [DecidableEq E] [CfRankerOf E R] {U : Type u_3} [Realizes U E] [Pronominalizes U E] (prev : Utterance E R) (cur : U) (prevCb : Option E) :
      Decidable (Rule1GJW83 prev cur prevCb)
      Equations
      • One or more equations did not get rendered due to their size.

      Rule 1 (Gordon, Grosz, Gilliom 1993) — unconditional #

      source
      def Discourse.Centering.Rule1Gordon {E : Type u_1} {R : Type u_2} [DecidableEq E] [CfRankerOf E R] {U : Type u_3} [Realizes U E] [Pronominalizes U E] (prev : Utterance E R) (cur : U) :
      Prop

      Rule 1 (Gordon, motivated by the repeated-name penalty, [GGG93]): the CB must always be pronominalized. Unconditional on what else is pronominalized.

      Equations
      Instances For
        source
        @[implicit_reducible]
        instance Discourse.Centering.Rule1Gordon.decidable {E : Type u_1} {R : Type u_2} [DecidableEq E] [CfRankerOf E R] {U : Type u_3} [Realizes U E] [Pronominalizes U E] (prev : Utterance E R) (cur : U) :
        Decidable (Rule1Gordon prev cur)
        Equations
        • One or more equations did not get rendered due to their size.

        Implication theorems #

        source
        theorem Discourse.Centering.Rule1Gordon_implies_GJW95 {E : Type u_1} {R : Type u_2} [DecidableEq E] [CfRankerOf E R] {U : Type u_3} [Realizes U E] [Pronominalizes U E] {prev : Utterance E R} {cur : U} (h : Rule1Gordon prev cur) :
        Rule1GJW95 prev cur

        Gordon ⇒ GJW 95: unconditional CB pronominalization implies the conditional version. One-directional (GJW 95 is vacuously true when no pronouns appear).