Centering Theory — Cb, Cf, Cp

[GJW95] Forward- and backward-looking center operations, parameterized by role ranker ([CfRankerOf E R]) and realizes-semantics ([Realizes U E]). GJW's "unique Cb" claim is enforced by cb's Option E return type.

Default Realizes / Pronominalizes for Utterance

@[implicit_reducible]

instance Discourse.Centering.utteranceRealizes {E : Type u_1} {R : Type u_2} [DecidableEq E] : Realizes (Utterance E R) E

For a list-of-realizations utterance, realizes is existence of a realization whose entity is the target.

Equations

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

@[implicit_reducible]

instance Discourse.Centering.utterancePronominalizes {E : Type u_1} {R : Type u_2} [DecidableEq E] : Pronominalizes (Utterance E R) E

For a list-of-realizations utterance, pronominalizes requires a realization of e whose isPronoun flag is true.

Equations

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

@[implicit_reducible]

instance Discourse.Centering.listRealizes {E : Type u_1} [DecidableEq E] : Realizes (List E) E

A flat list of entities realizes by membership (minimal "bag of referents" representation).

Equations

• Discourse.Centering.listRealizes = { Rel := fun (es : List E) (e : E) => e ∈ es, decRel := fun (x : List E) (x_1 : E) => inferInstance }

@[simp]

theorem Discourse.Centering.realizes_list_iff {E : Type u_1} [DecidableEq E] (es : List E) (e : E) : realizes es e ↔ e ∈ es

theorem Discourse.Centering.Utterance.realizes_iff {E : Type u_1} {R : Type u_2} [DecidableEq E] (u : Utterance E R) (e : E) : realizes u e ↔ ∃ r ∈ u.realizations, r.entity = e

Existential characterization of realizes on a list-of-realizations utterance.

theorem Discourse.Centering.Utterance.pronominalizes_iff {E : Type u_1} {R : Type u_2} [DecidableEq E] (u : Utterance E R) (e : E) : pronominalizes u e ↔ ∃ r ∈ u.realizations, r.entity = e ∧ r.isPronoun = true

Existential characterization of pronominalizes on a list-of-realizations utterance.

Cf, Cp via insertion sort on rank

def Discourse.Centering.Utterance.cfInsert {E : Type u_1} {R : Type u_2} [CfRankerOf E R] (r : Realization E R) : List (Realization E R) → List (Realization E R)

Insert r into a rank-descending Cf list, after any equally-ranked elements (surface order as stable tiebreaker).

Equations

• One or more equations did not get rendered due to their size.
• Discourse.Centering.Utterance.cfInsert r [] = [r]

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

Forward-looking centers via insertion-sort by rank (decide-reducible).

Equations

• u.cf = List.map (fun (x : Discourse.Centering.Realization E R) => x.entity) (List.foldr Discourse.Centering.Utterance.cfInsert [] u.realizations)

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

The top-ranked Cf element ("preferred center", Cp).

Equations

• u.cp = u.cf.head?

cf / cp characterization API

@[simp]

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

@[simp]

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

theorem Discourse.Centering.Utterance.mem_cfInsert_iff {E : Type u_1} {R : Type u_2} [CfRankerOf E R] (r : Realization E R) (xs : List (Realization E R)) (x : Realization E R) : x ∈ cfInsert r xs ↔ x = r ∨ x ∈ xs

cfInsert preserves membership: every element of the result is either the inserted element or already in the list.

theorem Discourse.Centering.Utterance.cfInsert_perm {E : Type u_1} {R : Type u_2} [CfRankerOf E R] (r : Realization E R) (xs : List (Realization E R)) : (cfInsert r xs).Perm (r :: xs)

cfInsert r xs is a permutation of r :: xs — insertion sort rearranges but doesn't drop or duplicate.

theorem Discourse.Centering.Utterance.cfRealizations_perm {E : Type u_1} {R : Type u_2} [CfRankerOf E R] (u : Utterance E R) : (List.foldr cfInsert [] u.realizations).Perm u.realizations

The internal sorted list (before mapping to entities) is a permutation of the surface realization list.

theorem Discourse.Centering.Utterance.mem_cf_iff {E : Type u_1} {R : Type u_2} [CfRankerOf E R] (u : Utterance E R) (e : E) : e ∈ u.cf ↔ ∃ r ∈ u.realizations, r.entity = e

Characterization of cf: an entity is in the forward-looking centers iff some realization in the utterance refers to it. The insertion-sort implementation is a permutation, so membership is preserved.

Cb (backward-looking center)

def Discourse.Centering.cb {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) : Option E

Backward-looking center: the highest-ranked element of prev.cf realized in cur. Polymorphic in cur's type via Realizes U E.

Equations

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

theorem Discourse.Centering.cb_mem_prev_cf {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} {e : E} (h : cb prev cur = some e) : e ∈ prev.cf

Locality of Cb ([GJW95]): cb prev cur is always drawn from prev.cf, never further back.

theorem Discourse.Centering.realizes_of_cb {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} {e : E} (h : cb prev cur = some e) : realizes cur e

The Cb is realized in the current utterance: when cb prev cur is some e, realizes cur e holds.

theorem Discourse.Centering.cb_eq_some_iff {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} {e : E} : cb prev cur = some e ↔ ∃ (l₁ : List E) (l₂ : List E), prev.cf = l₁ ++ e :: l₂ ∧ (∀ e' ∈ l₁, ¬realizes cur e') ∧ realizes cur e

cb prev cur = some e iff e ∈ prev.cf is realized in cur with no higher-ranked element of prev.cf also realized in cur.

theorem Discourse.Centering.cb_eq_none_iff {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} : cb prev cur = none ↔ ∀ e ∈ prev.cf, ¬realizes cur e

cb is none iff no element of prev.cf is realized in cur.

@[simp]

theorem Discourse.Centering.cb_empty_prev {E : Type u_1} {R : Type u_2} [DecidableEq E] [CfRankerOf E R] {U : Type u_3} [Realizes U E] (cur : U) : cb { realizations := [] } cur = none

cbAll (multi-CB under partial ranking)

def Discourse.Centering.cbAll {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) : List E

Multi-CB: entities tied at the highest rank-among-realized, deduplicated. Length ≤ 1 under total rankings; can exceed 1 under partial rankings (PSDH §5.3.4).

Equations

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

@[simp]

theorem Discourse.Centering.cbAll_empty_prev {E : Type u_1} {R : Type u_2} [DecidableEq E] [CfRankerOf E R] {U : Type u_3} [Realizes U E] (cur : U) : cbAll { realizations := [] } cur = []

theorem Discourse.Centering.mem_cbAll_exists_realization {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} {e : E} (h : e ∈ cbAll prev cur) : ∃ r ∈ prev.realizations, r.entity = e ∧ realizes cur r.entity

Every entity in cbAll prev cur corresponds to some realization in prev realized in cur.

theorem Discourse.Centering.mem_cbAll_realized {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} {e : E} (h : e ∈ cbAll prev cur) : realizes cur e

Every entity in cbAll prev cur is realized in cur.

theorem Discourse.Centering.mem_cbAll_mem_prev_cf {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} {e : E} (h : e ∈ cbAll prev cur) : e ∈ prev.cf

The multi-CB set is a subset of prev.cf (locality for cbAll).