Centering theory: centers and the pronominalization rule

Grosz, Joshi, and Weinstein's centering theory tracks the entities an utterance is about. An utterance realizes entities in grammatical roles; its forward-looking centers are those entities ranked by role, the first of them its preferred center, and its backward-looking center is the highest-ranked forward-looking center of the previous utterance that it realizes. Rule 1 says that if the utterance pronominalizes any forward-looking center of the previous one, it pronominalizes its backward-looking center.

Main declarations

• Discourse.Centering.Realization and Discourse.Centering.Utterance: a noun phrase realizing an entity in a role, by a pronoun or not, and an utterance as its realizations in surface order. e ∈ u says that u realizes e.
• Utterance.ranked, Utterance.cf, Utterance.cp: the realizations in rank order, the forward-looking centers, and the preferred center.
• Discourse.Centering.cb: the backward-looking center, for any current utterance with decidable membership, characterized by cb_eq_some_iff and role_le_of_cb.
• Discourse.Centering.PronominalizationConstraint and CbPronominalized: Rule 1 and Gordon, Grosz, and Gilliom's unconditional strengthening of it.

Implementation notes

The ranking of forward-looking centers is a LinearOrder on the role type, higher meaning more prominent; two realizations in the same role tie, and the sort is stable, so ties keep surface order. An entity realized twice is listed twice among the forward-looking centers, which leaves the backward-looking center, the preferred center, and Rule 1 unaffected.

The current utterance of cb is any type with decidable entity membership, so that a study can let an utterance realize an entity indirectly, as in [PSDEH04].

References

• [GJW95]
• [GGG93]
• [Kam86]
• [PSDEH04]

structure Discourse.Centering.Realization (E : Type u_3) (R : Type u_4) : Type (max u_3 u_4)

A noun phrase realizing entity in the grammatical role role, a pronoun or not.

• entity : E
• role : R
• isPronoun : Bool

def Discourse.Centering.instReprRealization.repr {E✝ : Type u_3} {R✝ : Type u_4} [Repr E✝] [Repr R✝] : Realization E✝ R✝ → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Discourse.Centering.instReprRealization {E✝ : Type u_3} {R✝ : Type u_4} [Repr E✝] [Repr R✝] : Repr (Realization E✝ R✝)

Equations

• Discourse.Centering.instReprRealization = { reprPrec := Discourse.Centering.instReprRealization.repr }

@[instance_reducible]

instance Discourse.Centering.instDecidableEqRealization {E✝ : Type u_3} {R✝ : Type u_4} [DecidableEq E✝] [DecidableEq R✝] : DecidableEq (Realization E✝ R✝)

Equations

• Discourse.Centering.instDecidableEqRealization = Discourse.Centering.instDecidableEqRealization.decEq

def Discourse.Centering.instDecidableEqRealization.decEq {E✝ : Type u_3} {R✝ : Type u_4} [DecidableEq E✝] [DecidableEq R✝] (x✝ x✝¹ : Realization E✝ R✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

structure Discourse.Centering.Utterance (E : Type u_3) (R : Type u_4) : Type (max u_3 u_4)

An utterance as its noun-phrase realizations in surface order.

• realizations : List (Realization E R)

def Discourse.Centering.instReprUtterance.repr {E✝ : Type u_3} {R✝ : Type u_4} [Repr E✝] [Repr R✝] : Utterance E✝ R✝ → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Discourse.Centering.instReprUtterance {E✝ : Type u_3} {R✝ : Type u_4} [Repr E✝] [Repr R✝] : Repr (Utterance E✝ R✝)

Equations

• Discourse.Centering.instReprUtterance = { reprPrec := Discourse.Centering.instReprUtterance.repr }

@[instance_reducible]

instance Discourse.Centering.instDecidableEqUtterance {E✝ : Type u_3} {R✝ : Type u_4} [DecidableEq E✝] [DecidableEq R✝] : DecidableEq (Utterance E✝ R✝)

Equations

• Discourse.Centering.instDecidableEqUtterance = Discourse.Centering.instDecidableEqUtterance.decEq

def Discourse.Centering.instDecidableEqUtterance.decEq {E✝ : Type u_3} {R✝ : Type u_4} [DecidableEq E✝] [DecidableEq R✝] (x✝ x✝¹ : Utterance E✝ R✝) : Decidable (x✝ = x✝¹)

Equations

• Discourse.Centering.instDecidableEqUtterance.decEq { realizations := a } { realizations := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Discourse.Centering.Utterance.instMembership {E : Type u_1} {R : Type u_2} : Membership E (Utterance E R)

e ∈ u when some realization in u is of e.

Equations

• One or more equations did not get rendered due to their size.

theorem Discourse.Centering.Utterance.mem_iff {E : Type u_1} {R : Type u_2} {u : Utterance E R} {e : E} : e ∈ u ↔ ∃ (r : Realization E R), r ∈ u.realizations ∧ r.entity = e

def Discourse.Centering.Utterance.Pronominalizes {E : Type u_1} {R : Type u_2} (u : Utterance E R) (e : E) : Prop

u realizes e by a pronoun.

Equations

• u.Pronominalizes e = ∃ (r : Discourse.Centering.Realization E R), r ∈ u.realizations ∧ r.entity = e ∧ r.isPronoun = true

@[instance_reducible]

instance Discourse.Centering.Utterance.instDecidableMem {E : Type u_1} {R : Type u_2} [DecidableEq E] (u : Utterance E R) (e : E) : Decidable (e ∈ u)

Equations

• u.instDecidableMem e = List.decidableBEx (fun (r : Discourse.Centering.Realization E R) => r.entity = e) u.realizations

@[instance_reducible]

instance Discourse.Centering.Utterance.instDecidablePronominalizes {E : Type u_1} {R : Type u_2} [DecidableEq E] (u : Utterance E R) (e : E) : Decidable (u.Pronominalizes e)

Equations

• u.instDecidablePronominalizes e = Discourse.Centering.Utterance.instDecidablePronominalizes._aux_1 u e

Forward-looking centers

def Discourse.Centering.Utterance.ranked {E : Type u_1} {R : Type u_2} [LinearOrder R] (u : Utterance E R) : List (Realization E R)

The realizations of u in rank order: descending by role, ties in surface order.

Equations

• u.ranked = List.insertionSort (fun (a b : Discourse.Centering.Realization E R) => b.role ≤ a.role) u.realizations

theorem Discourse.Centering.Utterance.ranked_perm {E : Type u_1} {R : Type u_2} [LinearOrder R] (u : Utterance E R) : u.ranked.Perm u.realizations

@[simp]

theorem Discourse.Centering.Utterance.mem_ranked {E : Type u_1} {R : Type u_2} [LinearOrder R] (u : Utterance E R) {r : Realization E R} : r ∈ u.ranked ↔ r ∈ u.realizations

theorem Discourse.Centering.Utterance.ranked_pairwise {E : Type u_1} {R : Type u_2} [LinearOrder R] (u : Utterance E R) : List.Pairwise (fun (a b : Realization E R) => b.role ≤ a.role) u.ranked

The rank order is descending by role.

def Discourse.Centering.Utterance.cf {E : Type u_1} {R : Type u_2} [LinearOrder R] (u : Utterance E R) : List E

The forward-looking centers of u: its entities in rank order.

Equations

• u.cf = List.map (fun (x : Discourse.Centering.Realization E R) => x.entity) u.ranked

def Discourse.Centering.Utterance.cp {E : Type u_1} {R : Type u_2} [LinearOrder R] (u : Utterance E R) : Option E

The preferred center of u: its highest-ranked forward-looking center.

Equations

• u.cp = u.cf.head?

@[simp]

theorem Discourse.Centering.Utterance.cf_mk_nil {E : Type u_1} {R : Type u_2} [LinearOrder R] : { realizations := [] }.cf = []

@[simp]

theorem Discourse.Centering.Utterance.cp_mk_nil {E : Type u_1} {R : Type u_2} [LinearOrder R] : { realizations := [] }.cp = none

@[simp]

theorem Discourse.Centering.Utterance.mem_cf {E : Type u_1} {R : Type u_2} [LinearOrder R] (u : Utterance E R) {e : E} : e ∈ u.cf ↔ e ∈ u

The forward-looking centers of u are the entities it realizes.

theorem Discourse.Centering.Utterance.cp_mem_cf {E : Type u_1} {R : Type u_2} [LinearOrder R] (u : Utterance E R) {e : E} (h : u.cp = some e) : e ∈ u.cf

theorem Discourse.Centering.Utterance.cp_mem {E : Type u_1} {R : Type u_2} [LinearOrder R] (u : Utterance E R) {e : E} (h : u.cp = some e) : e ∈ u

The backward-looking center

def Discourse.Centering.cb {E : Type u_1} {R : Type u_2} [LinearOrder R] {U : Type u_3} [Membership E U] [(u : U) → (e : E) → Decidable (e ∈ u)] (prev : Utterance E R) (cur : U) : Option E

The backward-looking center of cur after prev: the highest-ranked forward-looking center of prev that cur realizes, if any.

Equations

• Discourse.Centering.cb prev cur = List.find? (fun (x : E) => decide (x ∈ cur)) prev.cf

@[simp]

theorem Discourse.Centering.cb_mk_nil {E : Type u_1} {R : Type u_2} [LinearOrder R] {U : Type u_3} [Membership E U] [(u : U) → (e : E) → Decidable (e ∈ u)] (cur : U) : cb { realizations := [] } cur = none

theorem Discourse.Centering.cb_mem_cf {E : Type u_1} {R : Type u_2} [LinearOrder R] {U : Type u_3} [Membership E U] [(u : U) → (e : E) → Decidable (e ∈ u)] {prev : Utterance E R} {cur : U} {e : E} (h : cb prev cur = some e) : e ∈ prev.cf

The backward-looking center is a forward-looking center of the previous utterance.

theorem Discourse.Centering.mem_of_cb {E : Type u_1} {R : Type u_2} [LinearOrder R] {U : Type u_3} [Membership E U] [(u : U) → (e : E) → Decidable (e ∈ u)] {prev : Utterance E R} {cur : U} {e : E} (h : cb prev cur = some e) : e ∈ cur

The backward-looking center is realized in the current utterance.

theorem Discourse.Centering.cb_eq_some_iff {E : Type u_1} {R : Type u_2} [LinearOrder R] {U : Type u_3} [Membership E U] [(u : U) → (e : E) → Decidable (e ∈ u)] {prev : Utterance E R} {cur : U} {e : E} : cb prev cur = some e ↔ e ∈ cur ∧ ∃ (l₁ : List E), ∃ (l₂ : List E), prev.cf = l₁ ++ e :: l₂ ∧ ∀ (e' : E), e' ∈ l₁ → ¬e' ∈ cur

cur has e as backward-looking center after prev iff e is a forward-looking center of prev realized in cur with no higher-ranked forward-looking center realized in cur.

theorem Discourse.Centering.cb_eq_none_iff {E : Type u_1} {R : Type u_2} [LinearOrder R] {U : Type u_3} [Membership E U] [(u : U) → (e : E) → Decidable (e ∈ u)] {prev : Utterance E R} {cur : U} : cb prev cur = none ↔ ∀ (e : E), e ∈ prev.cf → ¬e ∈ cur

cur has no backward-looking center after prev iff it realizes no forward-looking center of prev.

theorem Discourse.Centering.role_le_of_cb {E : Type u_1} {R : Type u_2} [LinearOrder R] {U : Type u_3} [Membership E U] [(u : U) → (e : E) → Decidable (e ∈ u)] {prev : Utterance E R} {cur : U} {e : E} (h : cb prev cur = some e) {r : Realization E R} (hr : r ∈ prev.realizations) (hcur : r.entity ∈ cur) : ∃ (r' : Realization E R), r' ∈ prev.realizations ∧ r'.entity = e ∧ r.role ≤ r'.role

No forward-looking center of prev realized in cur outranks the backward-looking center: every realization in prev of an entity realized in cur is ranked at or below some realization of the center.

Rule 1

def Discourse.Centering.CbPronominalized {E : Type u_1} {R : Type u_2} [DecidableEq E] [LinearOrder R] (prev cur : Utterance E R) : Prop

The backward-looking center of cur after prev, if any, is pronominalized: Gordon, Grosz, and Gilliom's unconditional strengthening of Rule 1, motivated by the repeated-name penalty.

Equations

• Discourse.Centering.CbPronominalized prev cur = ∀ (c : E), c ∈ Discourse.Centering.cb prev cur → cur.Pronominalizes c

@[instance_reducible]

instance Discourse.Centering.instDecidableCbPronominalized {E : Type u_1} {R : Type u_2} [DecidableEq E] [LinearOrder R] (prev cur : Utterance E R) : Decidable (CbPronominalized prev cur)

Equations

• Discourse.Centering.instDecidableCbPronominalized prev cur = Discourse.Centering.instDecidableCbPronominalized._aux_1 prev cur

def Discourse.Centering.PronominalizationConstraint {E : Type u_1} {R : Type u_2} [DecidableEq E] [LinearOrder R] (prev cur : Utterance E R) : Prop

Rule 1 of [GJW95]: if cur pronominalizes any forward-looking center of prev, it pronominalizes its backward-looking center.

Equations

• Discourse.Centering.PronominalizationConstraint prev cur = ((∃ (e : E), e ∈ prev.cf ∧ cur.Pronominalizes e) → Discourse.Centering.CbPronominalized prev cur)

@[instance_reducible]

instance Discourse.Centering.instDecidablePronominalizationConstraint {E : Type u_1} {R : Type u_2} [DecidableEq E] [LinearOrder R] (prev cur : Utterance E R) : Decidable (PronominalizationConstraint prev cur)

Equations

• One or more equations did not get rendered due to their size.

theorem Discourse.Centering.CbPronominalized.constraint {E : Type u_1} {R : Type u_2} [DecidableEq E] [LinearOrder R] {prev cur : Utterance E R} (h : CbPronominalized prev cur) : PronominalizationConstraint prev cur

The unconditional strengthening implies Rule 1.

theorem Discourse.Centering.pronominalizationConstraint_of_forall_not {E : Type u_1} {R : Type u_2} [DecidableEq E] [LinearOrder R] {prev cur : Utterance E R} (h : ∀ (e : E), ¬cur.Pronominalizes e) : PronominalizationConstraint prev cur

Rule 1 holds vacuously when cur uses no pronoun.