Centering Theory — Cb, Cf, Cp

@cite{grosz-joshi-weinstein-1995} §3

The basic forward/backward-looking center operations, parameterized by the role type (via [CfRankerOf E R]) and the realizes-semantics (via [Realizes U E]).

• Utterance.cf — forward-looking centers, ordered by role rank (descending), with surface order as tie-breaker. Implemented by insertion sort so that decide reduces it in the kernel for the paper's worked examples.

• Utterance.cp — preferred (top-ranked) Cf element.

• cb prev cur — backward-looking center: highest-ranked element of prev.cf realized in cur. The current utterance type is generic via [Realizes U E], so the same cb works for an Utterance E R, a DRSExpr, or any future representation that supplies a Realizes instance.

The "unique Cb" claim of @cite{grosz-joshi-weinstein-1995} §3 is enforced by the type Option E, not by a separate theorem.

@[implicit_reducible]

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

For a list-of-realizations utterance, realizes is list-membership of the entity among the realizations' entities.

Equations

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

@[implicit_reducible]

instance Discourse.Centering.utterancePronominalizes {E R : Type} [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} [DecidableEq E] : Realizes (List E) E

A flat list of entities also realizes — an entity e is realized by es : List E iff it appears in es. This is the minimal "bag of referents" representation, useful when role/pronoun annotations are unavailable (corpus-extracted referent traces, simple toy examples).

Together with utteranceRealizes and the DRSExpr instance in the DRT bridge, this confirms that the Realizes typeclass abstracts cleanly over multiple representations.

Equations

• Discourse.Centering.listRealizes = { decide := fun (es : List E) (e : E) => es.contains e }

@[simp]

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

theorem Discourse.Centering.Utterance.realizes_iff {E R : Type} [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, useful for proofs.

theorem Discourse.Centering.Utterance.pronominalizes_iff {E R : Type} [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.

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

Insert r into a Cf list (ordered by CfRankerOf.rank descending), placing r after any equally-ranked elements so the original surface order acts as a stable tiebreaker.

Concretely: walk the list, insert r at the first position where the existing element has strictly smaller rank.

Uses the generalized CfRankerOf E R (per-realization) typeclass rather than CfRanker R (per-role); when only the role matters, the default instance cfRankerOf_of_role (in Defs.lean) lifts automatically.

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 R : Type} [CfRankerOf E R] (u : Utterance E R) : List E

Forward-looking centers, ranked highest-first by role rank with surface order as tiebreaker. Implemented by foldr cfInsert [] — insertion sort — so that decide reduces it in the kernel for the paper's worked examples.

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 R : Type} [CfRankerOf E R] (u : Utterance E R) : Option E

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

Equations

• u.cp = u.cf.head?

@[simp]

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

@[simp]

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

theorem Discourse.Centering.Utterance.mem_cfInsert_iff {E R : Type} [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 R : Type} [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 R : Type} [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 R : Type} [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.

def Discourse.Centering.cb {E R : Type} [DecidableEq E] [CfRankerOf E R] {U : Type} [Realizes U E] (prev : Utterance E R) (cur : U) : Option E

Backward-looking center of cur with respect to prev: the highest-ranked element of prev.cf that is realized in cur. none if no such element exists.

The current utterance cur can be anything with a Realizes U E instance — including a DRSExpr via the DRT bridge.

Equations

• Discourse.Centering.cb prev cur = List.find? (Discourse.Centering.Realizes.decide cur) prev.cf

theorem Discourse.Centering.cb_mem_prev_cf {E R : Type} [DecidableEq E] [CfRankerOf E R] {U : Type} [Realizes U E] {prev : Utterance E R} {cur : U} {e : E} (h : cb prev cur = some e) : e ∈ prev.cf

Locality of Cb (@cite{grosz-joshi-weinstein-1995} §4, claim 5): when cb prev cur returns some entity, that entity is in prev.cf — the backward-looking center is strictly local, drawn only from the previous utterance's forward-looking centers, never from Cf(U_{n-2}) or earlier.

theorem Discourse.Centering.decide_of_cb {E R : Type} [DecidableEq E] [CfRankerOf E R] {U : Type} [Realizes U E] {prev : Utterance E R} {cur : U} {e : E} (h : cb prev cur = some e) : Realizes.decide cur e = true

The Cb is realized in the current utterance: when cb prev cur is some e, the realizes-relation holds of (cur, e).

theorem Discourse.Centering.cb_eq_some_iff {E R : Type} [DecidableEq E] [CfRankerOf E R] {U : Type} [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.decide cur e' = false) ∧ Realizes.decide cur e = true

Characterization of cb: cb prev cur = some e iff e is in prev.cf realized in cur, and no earlier element of prev.cf (i.e., none more highly ranked) is realized in cur. This is the "first realized in cf-order" definition unfolded.

theorem Discourse.Centering.cb_eq_none_iff {E R : Type} [DecidableEq E] [CfRankerOf E R] {U : Type} [Realizes U E] {prev : Utterance E R} {cur : U} : cb prev cur = none ↔ ∀ e ∈ prev.cf, Realizes.decide cur e = false

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

@[simp]

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

def Discourse.Centering.cbAll {E R : Type} [DecidableEq E] [CfRankerOf E R] {U : Type} [Realizes U E] (prev : Utterance E R) (cur : U) : List E

All entities tied at the highest rank-among-realized, deduplicated.

Under a total ranking, this list has length ≤ 1 (one CB or zero, matching cb's Option E typing). Under a partial ranking, two realizations can tie at the maximum and both qualify as CBs — the case that drives @cite{poesio-stevenson-eugenio-hitzeman-2004} §5.3.4 (their two-CB corner-cupboard / Branicki example, paper §4.1.1 example (10)). PSDH propose decomposing Constraint 1 into "CB Uniqueness" (this list has length ≤ 1) and "Entity Continuity" (this list has length ≥ 1) — the substrate decomposition theorem lives in Constraints.lean.

Structural identity with single-constraint OT (cf. Core.Constraint.OT.Tableau.optimal): the realizations realized in cur form the candidate set; CfRankerOf.rank is a single (sign- flipped) violation profile; cbAll returns the entity-projection of the OT-optimal candidates. @cite{poesio-stevenson-eugenio-hitzeman-2004} §3.1 fn 12 endorses this reformulation, citing Beaver 2004's "The Optimization of Discourse Anaphora." Both substrates here use List.argmax from Mathlib.Data.List.MinMax as the underlying extremum-selection primitive; the bridge theorem connecting them will live in Phenomena/Reference/Studies/Beaver2004.lean (a future commit). The deliberate non-bridging follows mathlib's PMF vs Measure precedent: each substrate keeps its own vocabulary, with cross-framework identities anchored in the paper that argues them.

Equations

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

@[simp]

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

theorem Discourse.Centering.mem_cbAll_exists_realization {E R : Type} [DecidableEq E] [CfRankerOf E R] {U : Type} [Realizes U E] {prev : Utterance E R} {cur : U} {e : E} (h : e ∈ cbAll prev cur) : ∃ r ∈ prev.realizations, r.entity = e ∧ Realizes.decide cur r.entity = true

Every entity in cbAll prev cur corresponds to some realization in prev whose entity is realized in cur. The substantive characterization of cbAll (modulo argmax-rank reasoning, which a future commit can expose via mem_cbAll_iff).

theorem Discourse.Centering.mem_cbAll_realized {E R : Type} [DecidableEq E] [CfRankerOf E R] {U : Type} [Realizes U E] {prev : Utterance E R} {cur : U} {e : E} (h : e ∈ cbAll prev cur) : Realizes.decide cur e = true

Every entity in cbAll prev cur is realized in cur.

theorem Discourse.Centering.mem_cbAll_mem_prev_cf {E R : Type} [DecidableEq E] [CfRankerOf E R] {U : Type} [Realizes U E] {prev : Utterance E R} {cur : U} {e : E} (h : e ∈ cbAll prev cur) : e ∈ prev.cf

Every entity in cbAll prev cur is in prev.cf — the multi-CB set is a subset of the previous utterance's forward-looking centers, mirroring cb_mem_prev_cf for the single-CB case.