Centering Theory — Core Definitions

[GJW95] [Kam86] [Sid79] Theory-neutral types for Centering: realizations, utterances, and typeclass plug-ins for ranking schemes (CfRanker/CfRankerOf), realization (Realizes), and pronominalization (Pronominalizes). Role type R is a parameter; Instances/ provides per-paper rankers.

Cf Ranking Plug-In

class Discourse.Centering.CfRanker (R : Type u_1) : Type u_1

Numeric rank over a role type for ordering forward-looking centers (higher rank ⇒ more prominent in Cf).

• rank : R → ℕ

@[reducible, inline]

abbrev Discourse.Centering.CfRanker.toLinearOrder (R : Type u_1) [CfRanker R] [DecidableEq R] [Fintype R] (h : ∀ (a b : R), rank a = rank b → a = b := by decide) : LinearOrder R

Lift a CfRanker instance to a LinearOrder. For finite-enum role types, the injectivity obligation is dischargeable by decide.

Equations

• Discourse.Centering.CfRanker.toLinearOrder R h = LinearOrder.lift' Discourse.Centering.CfRanker.rank h

Realization and Utterance

structure Discourse.Centering.Realization (E : Type u_1) (R : Type u_2) : Type (max u_1 u_2)

A noun-phrase realization: entity, role, pronoun flag.

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

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

def Discourse.Centering.instDecidableEqRealization.decEq {E✝ : Type u_1} {R✝ : Type u_2} [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_1) (R : Type u_2) : Type (max u_1 u_2)

An utterance as a list of NP realizations in surface order.

• realizations : List (Realization E R)

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

Equations

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

@[implicit_reducible]

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

Equations

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

def Discourse.Centering.instDecidableEqUtterance.decEq {E✝ : Type u_1} {R✝ : Type u_2} [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 ⋯

@[implicit_reducible]

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

Equations

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

Generalized Cf Ranking (per-realization)

class Discourse.Centering.CfRankerOf (E : Type u_1) (R : Type u_2) : Type (max u_1 u_2)

Rank a full Realization (not just its role). Needed by rankers that depend on surface position (Rambow 1993) or information status (Strube-Hahn 1999); CfRanker R lifts here via cfRankerOf_of_role.

• rank : Realization E R → ℕ

@[implicit_reducible, instance 100]

instance Discourse.Centering.cfRankerOf_of_role {E : Type u_1} {R : Type u_2} [r : CfRanker R] : CfRankerOf E R

Default lift: rank by role only via r.role. Low priority so per-realization instances win.

Equations

• Discourse.Centering.cfRankerOf_of_role = { rank := fun (rl : Discourse.Centering.Realization E R) => Discourse.Centering.CfRanker.rank rl.role }

Realizes / Pronominalizes Plug-Ins

class Discourse.Centering.Realizes (U : Type u_1) (E : outParam (Type u_2)) : Type (max u_1 u_2)

"u realizes e": the entity e is among the referents contributed by u. outParam E so typeclass search infers entity type from U.

• Rel : U → E → Prop

  The predicate "u realizes e".

• decRel (u : U) (e : E) : Decidable (Rel u e)

  The relation is pointwise decidable.

@[reducible, inline]

abbrev Discourse.Centering.realizes {U : Type u_1} {E : Type u_2} [Realizes U E] (u : U) (e : E) : Prop

"u realizes e", as a Prop. Ergonomic alias for Realizes.Rel.

Equations

• Discourse.Centering.realizes u e = Discourse.Centering.Realizes.Rel u e

class Discourse.Centering.Pronominalizes (U : Type u_1) (E : outParam (Type u_2)) : Type (max u_1 u_2)

"u pronominalizes e": some realization of e in u is pronominal.

• Rel : U → E → Prop

  The predicate "u pronominalizes e".

• decRel (u : U) (e : E) : Decidable (Rel u e)

  The relation is pointwise decidable.

@[reducible, inline]

abbrev Discourse.Centering.pronominalizes {U : Type u_1} {E : Type u_2} [Pronominalizes U E] (u : U) (e : E) : Prop

"u pronominalizes e", as a Prop. Ergonomic alias for Pronominalizes.Rel.

Equations

• Discourse.Centering.pronominalizes u e = Discourse.Centering.Pronominalizes.Rel u e