Beaver (2004): The Optimization of Discourse Anaphora

Centering's BFP algorithm ([BFP87]) is restated as six ranked OT constraints, COT (4): AGREE > DISJOINT > PRO-TOP > FAM-DEF > COHERE > ALIGN. Three of the six are Centering primitives this library already carries — PRO-TOP is Rule 1 without its if-clause (CbPronominalized), COHERE and ALIGN are the transition-classification tests (cb, cp) — so on those the correspondence with BFP holds by construction. The paper's Theorem (20) says COT and BFP resolve anaphora identically; its core is table (19), which matches COHERE/ALIGN violation patterns to the transition ranking, proved here in general. Because COT constraints are rerankable, demoting PRO-TOP below FAM-DEF (§4.1) recovers the coreferential reading of (2c) that BFP wrongly filters out.

Main statements

• cot_iff_bfp: table (19) — for candidates tied on the four higher-ranked constraints, the COT profile comparison is the BFP transition preference.
• d2_canonical_picks_two_marys, d2_demoted_picks_bound: the §4.1 reranking flips (2c) from the two-Marys reading to the coreferential one.
• cohere_factors_through_cb, align_factors_through_cb_and_cp: the reused constraints see a candidate only through cb (and cp).

References

• [Bea04]: The optimization of discourse anaphora. Linguistics and Philosophy 27.
• [BFP87]: A centering approach to pronouns.
• [GJW95]: Centering: a framework for modeling the local coherence of discourse.
• [GGG93]: Pronouns, names, and the centering of attention in discourse.
• [Str98]: Never look back: an alternative to centering.
• [PSDEH04]: Centering: a parametric theory and its instantiations.

Candidates

structure Beaver2004.Candidate (E R : Type) : Type

A COT candidate: a fully-resolved utterance (pronouns bound to entities) plus verdict flags for the three constraints whose inputs the Utterance substrate does not carry — φ-features (AGREE), predicate-argument structure (DISJOINT) and definiteness/familiarity (FAM-DEF).

• utt : Discourse.Centering.Utterance E R

  The resolved utterance.

• agreementOK : Bool

  AGREE verdict: pronoun–antecedent number/gender match.

• argDisjointOK : Bool

  DISJOINT verdict: co-arguments of each predicate are distinct.

• famDefOK : Bool

  FAM-DEF verdict: every definite NP is familiar.

@[instance_reducible]

instance Beaver2004.instReprCandidate {E✝ R✝ : Type} [Repr E✝] [Repr R✝] : Repr (Candidate E✝ R✝)

Equations

• Beaver2004.instReprCandidate = { reprPrec := Beaver2004.instReprCandidate.repr }

def Beaver2004.instReprCandidate.repr {E✝ R✝ : Type} [Repr E✝] [Repr R✝] : Candidate E✝ R✝ → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Beaver2004.instDecidableEqCandidate {E✝ R✝ : Type} [DecidableEq E✝] [DecidableEq R✝] : DecidableEq (Candidate E✝ R✝)

Equations

• Beaver2004.instDecidableEqCandidate = Beaver2004.instDecidableEqCandidate.decEq

def Beaver2004.instDecidableEqCandidate.decEq {E✝ R✝ : Type} [DecidableEq E✝] [DecidableEq R✝] (x✝ x✝¹ : Candidate E✝ R✝) : Decidable (x✝ = x✝¹)

Equations

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

The six constraints (4)

def Beaver2004.agree {E R : Type} : OptimalityTheory.Constraint (Candidate E R)

AGREE: anaphoric expressions agree with their antecedents in number and gender.

Equations

• Beaver2004.agree = OptimalityTheory.Constraint.binary fun (c : Beaver2004.Candidate E R) => ¬c.agreementOK = true

def Beaver2004.disjoint {E R : Type} : OptimalityTheory.Constraint (Candidate E R)

DISJOINT: co-arguments of a predicate are disjoint (the effect of Principle B).

Equations

• Beaver2004.disjoint = OptimalityTheory.Constraint.binary fun (c : Beaver2004.Candidate E R) => ¬c.argDisjointOK = true

def Beaver2004.proTop {E R : Type} [DecidableEq E] [LinearOrder R] (prev : Discourse.Centering.Utterance E R) : OptimalityTheory.Constraint (Candidate E R)

PRO-TOP: the topic is pronominalized — Rule 1 without its if-clause, via the unconditional CbPronominalized ([GGG93]). With no pronoun in the sentence every candidate violates PRO-TOP alike (p. 16), so the conditional Rule-1 form would be the wrong primitive.

Equations

• Beaver2004.proTop prev = OptimalityTheory.Constraint.binary fun (c : Beaver2004.Candidate E R) => ¬Discourse.Centering.CbPronominalized prev c.utt

def Beaver2004.famDef {E R : Type} : OptimalityTheory.Constraint (Candidate E R)

FAM-DEF: each definite NP is familiar.

Equations

• Beaver2004.famDef = OptimalityTheory.Constraint.binary fun (c : Beaver2004.Candidate E R) => ¬c.famDefOK = true

def Beaver2004.cohere {E R : Type} [DecidableEq E] [LinearOrder R] (prev : Discourse.Centering.Utterance E R) (priorTopic : Option E) : OptimalityTheory.Constraint (Candidate E R)

COHERE: the topic of the current sentence is the topic of the previous one — satisfied only when both are defined and equal (p. 17); an undefined topic counts as a violation.

Equations

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

def Beaver2004.align {E R : Type} [DecidableEq E] [LinearOrder R] (prev : Discourse.Centering.Utterance E R) : OptimalityTheory.Constraint (Candidate E R)

ALIGN: the topic is in subject position — for canonical sentences, the topic is the preferred center (p. 18); an undefined topic counts as a violation.

Equations

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

def Beaver2004.cotRanking {E R : Type} [DecidableEq E] [LinearOrder R] (prev : Discourse.Centering.Utterance E R) (priorTopic : Option E) : List (OptimalityTheory.Constraint (Candidate E R))

The COT ranking (4): AGREE > DISJOINT > PRO-TOP > FAM-DEF > COHERE > ALIGN.

Equations

• Beaver2004.cotRanking prev priorTopic = [Beaver2004.agree, Beaver2004.disjoint, Beaver2004.proTop prev, Beaver2004.famDef, Beaver2004.cohere prev priorTopic, Beaver2004.align prev]

def Beaver2004.cotRankingDemoted {E R : Type} [DecidableEq E] [LinearOrder R] (prev : Discourse.Centering.Utterance E R) (priorTopic : Option E) : List (OptimalityTheory.Constraint (Candidate E R))

The §4.1 reranking: PRO-TOP demoted below FAM-DEF.

Equations

• Beaver2004.cotRankingDemoted prev priorTopic = [Beaver2004.agree, Beaver2004.disjoint, Beaver2004.famDef, Beaver2004.proTop prev, Beaver2004.cohere prev priorTopic, Beaver2004.align prev]

COHERE and ALIGN factor through cb (and cp)

theorem Beaver2004.cohere_factors_through_cb {E R : Type} [DecidableEq E] [LinearOrder R] (prev : Discourse.Centering.Utterance E R) (priorTopic : Option E) (c1 c2 : Candidate E R) (h : Discourse.Centering.cb prev c1.utt = Discourse.Centering.cb prev c2.utt) : cohere prev priorTopic c1 = cohere prev priorTopic c2

COHERE cannot distinguish candidates whose cb agrees.

theorem Beaver2004.align_factors_through_cb_and_cp {E R : Type} [DecidableEq E] [LinearOrder R] (prev : Discourse.Centering.Utterance E R) (c1 c2 : Candidate E R) (h_cb : Discourse.Centering.cb prev c1.utt = Discourse.Centering.cb prev c2.utt) (h_cp : c1.utt.cp = c2.utt.cp) : align prev c1 = align prev c2

ALIGN cannot distinguish candidates whose cb and cp both agree.

Table (19): the COT ranking is the BFP transition preference

inductive Beaver2004.BFPTransition : Type

BFP's four transition types.

• continue_ : BFPTransition
• retain : BFPTransition
• smoothShift : BFPTransition
• roughShift : BFPTransition

@[instance_reducible]

instance Beaver2004.instDecidableEqBFPTransition : DecidableEq BFPTransition

Equations

• Beaver2004.instDecidableEqBFPTransition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Beaver2004.instReprBFPTransition.repr : BFPTransition → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Beaver2004.instReprBFPTransition : Repr BFPTransition

Equations

• Beaver2004.instReprBFPTransition = { reprPrec := Beaver2004.instReprBFPTransition.repr }

def Beaver2004.BFPTransition.rank : BFPTransition → ℕ

The BFP preference: continue > retain > smooth shift > rough shift.

Equations

• Beaver2004.BFPTransition.continue_.rank = 3
• Beaver2004.BFPTransition.retain.rank = 2
• Beaver2004.BFPTransition.smoothShift.rank = 1
• Beaver2004.BFPTransition.roughShift.rank = 0

def Beaver2004.bfpTransition {E R : Type} [DecidableEq E] [LinearOrder R] (prev : Discourse.Centering.Utterance E R) (priorTopic : Option E) (c : Candidate E R) : BFPTransition

The transition a candidate realizes, read off its COHERE and ALIGN verdicts: topic kept and aligned is a continuation, kept but unaligned a retain, changed but aligned a smooth shift, changed and unaligned a rough shift.

Equations

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

theorem Beaver2004.cot_iff_bfp {E R : Type} [DecidableEq E] [LinearOrder R] (prev : Discourse.Centering.Utterance E R) (priorTopic : Option E) (c1 c2 : Candidate E R) (h : ∀ (i : Fin 6), ↑i < 4 → toLex (fun (x : Fin (cotRanking prev priorTopic).length) => (cotRanking prev priorTopic).get x c1) i = toLex (fun (x : Fin (cotRanking prev priorTopic).length) => (cotRanking prev priorTopic).get x c2) i) : ((toLex fun (x : Fin (cotRanking prev priorTopic).length) => (cotRanking prev priorTopic).get x c1) < toLex fun (x : Fin (cotRanking prev priorTopic).length) => (cotRanking prev priorTopic).get x c2) ↔ (bfpTransition prev priorTopic c2).rank < (bfpTransition prev priorTopic c1).rank

Table (19), in general: for two candidates tied on AGREE, DISJOINT, PRO-TOP and FAM-DEF, the COT profile comparison under the canonical ranking coincides with the BFP preference between the transitions they realize — the core of the equivalence Theorem (20).

Example (12): a retain

@[reducible, inline]

abbrev Beaver2004.D12.Utt : Type

Equations

• Beaver2004.D12.Utt = Discourse.Centering.Utterance String Discourse.Centering.GrammaticalRole

def Beaver2004.D12.a : Utt

(12a) "Jane is happy."

Equations

• Beaver2004.D12.a = { realizations := [{ entity := "Jane", role := Discourse.Centering.GrammaticalRole.subject, isPronoun := false }] }

def Beaver2004.D12.b : Utt

(12b) "She was congratulated by Freda." She = Jane.

Equations

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

def Beaver2004.D12.c_l_eq_i : Utt

(12c) with her = Jane: the winner.

Equations

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

def Beaver2004.D12.c_l_eq_j : Utt

(12c) with her = Freda: the loser.

Equations

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

def Beaver2004.D12.cand_l_eq_i : Candidate String Discourse.Centering.GrammaticalRole

her = Jane, wrapped: AGREE, DISJOINT and FAM-DEF are all satisfied.

Equations

• Beaver2004.D12.cand_l_eq_i = { utt := Beaver2004.D12.c_l_eq_i, agreementOK := true, argDisjointOK := true, famDefOK := true }

def Beaver2004.D12.cand_l_eq_j : Candidate String Discourse.Centering.GrammaticalRole

her = Freda, wrapped.

Equations

• Beaver2004.D12.cand_l_eq_j = { utt := Beaver2004.D12.c_l_eq_j, agreementOK := true, argDisjointOK := true, famDefOK := true }

def Beaver2004.D12.priorTopic : Option String

The prior topic, from (12a) → (12b): Jane.

Equations

• Beaver2004.D12.priorTopic = Discourse.Centering.cb Beaver2004.D12.a Beaver2004.D12.b

def Beaver2004.d12_profile_l_eq_i : OptimalityTheory.ViolationProfile 6

The (12c) winner's profile under the canonical ranking.

Equations

• Beaver2004.d12_profile_l_eq_i = toLex fun (x : Fin 6) => (Beaver2004.cotRanking Beaver2004.D12.b Beaver2004.D12.priorTopic).get x Beaver2004.D12.cand_l_eq_i

def Beaver2004.d12_profile_l_eq_j : OptimalityTheory.ViolationProfile 6

The (12c) loser's profile.

Equations

• Beaver2004.d12_profile_l_eq_j = toLex fun (x : Fin 6) => (Beaver2004.cotRanking Beaver2004.D12.b Beaver2004.D12.priorTopic).get x Beaver2004.D12.cand_l_eq_j

theorem Beaver2004.d12_lex_picks_l_eq_i : d12_profile_l_eq_i < d12_profile_l_eq_j

Tableau (13): the her = Jane candidate wins the lexicographic comparison.

theorem Beaver2004.d12_transition_retain : bfpTransition D12.b D12.priorTopic D12.cand_l_eq_i = BFPTransition.retain

The (12c) winner realizes a retain: Jane stays topic but leaves subject position.

Example (2): breaking Rule 1 by reranking (§4.1)

@[reducible, inline]

abbrev Beaver2004.D2.Utt : Type

Equations

• Beaver2004.D2.Utt = Discourse.Centering.Utterance String Discourse.Centering.GrammaticalRole

def Beaver2004.D2.a : Utt

(2a) "Mary likes tennis."

Equations

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

def Beaver2004.D2.b : Utt

(2b) "She plays Jim quite often." She = Mary.

Equations

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

def Beaver2004.D2.c_bound : Utt

(2c), coreferential reading: He = Jim, Mary = the (2a) Mary.

Equations

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

def Beaver2004.D2.c_two_marys : Utt

(2c), two-Marys reading: the object "Mary" is a new entity.

Equations

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

def Beaver2004.D2.cand_bound : Candidate String Discourse.Centering.GrammaticalRole

Coreferential candidate: the anaphoric "Mary" is familiar.

Equations

• Beaver2004.D2.cand_bound = { utt := Beaver2004.D2.c_bound, agreementOK := true, argDisjointOK := true, famDefOK := true }

def Beaver2004.D2.cand_two_marys : Candidate String Discourse.Centering.GrammaticalRole

Two-Marys candidate: the new "Mary" is an unfamiliar definite, so FAM-DEF fires.

Equations

• Beaver2004.D2.cand_two_marys = { utt := Beaver2004.D2.c_two_marys, agreementOK := true, argDisjointOK := true, famDefOK := false }

def Beaver2004.D2.priorTopic : Option String

The prior topic for (2c): Mary.

Equations

• Beaver2004.D2.priorTopic = Discourse.Centering.cb Beaver2004.D2.a Beaver2004.D2.b

theorem Beaver2004.d2_canonical_picks_two_marys : (toLex fun (x : Fin (cotRanking D2.b D2.priorTopic).length) => (cotRanking D2.b D2.priorTopic).get x D2.cand_two_marys) < toLex fun (x : Fin (cotRanking D2.b D2.priorTopic).length) => (cotRanking D2.b D2.priorTopic).get x D2.cand_bound

Under the canonical ranking (18), the two-Marys reading wins — BFP's (incorrect) prediction, driven by PRO-TOP over FAM-DEF.

theorem Beaver2004.d2_demoted_picks_bound : (toLex fun (x : Fin (cotRankingDemoted D2.b D2.priorTopic).length) => (cotRankingDemoted D2.b D2.priorTopic).get x D2.cand_bound) < toLex fun (x : Fin (cotRankingDemoted D2.b D2.priorTopic).length) => (cotRankingDemoted D2.b D2.priorTopic).get x D2.cand_two_marys

Under the demoted ranking (21), the coreferential reading wins: FAM-DEF now outranks PRO-TOP, so introducing a second Mary costs more than leaving the topic unpronominalized.

ALIGN and Strube's cheapness

theorem Beaver2004.align_eq_zero_iff {E R : Type} [DecidableEq E] [LinearOrder R] (prev : Discourse.Centering.Utterance E R) (c : Candidate E R) : align prev c = 0 ↔ (Discourse.Centering.cb prev c.utt).isSome = true ∧ Discourse.Centering.cb prev c.utt = c.utt.cp

ALIGN is satisfied exactly when the topic is defined and is the current preferred center — the within-utterance analogue of [Str98]'s cheap transitions, which test the same shape against the previous Cp.