Documentation

Linglib.Theories.Discourse.Centering.Constraints

Centering Theory — Constraint 1 and Its Decomposition #

@cite{poesio-stevenson-eugenio-hitzeman-2004} @cite{grosz-joshi-weinstein-1995}

@cite{grosz-joshi-weinstein-1995} stated Constraint 1 (sometimes called the "uniqueness" or "entity coherence" constraint) as a single claim: every utterance after the first has exactly one CB. @cite{poesio-stevenson-eugenio-hitzeman-2004} §5.3.2 (p. 356-357) propose unpacking this into two separate, independently testable claims:

We feel this work has greatly helped our understanding of the theory and believe that it would be similarly useful to unpack Constraint 1 into two separate claims, as well: one about uniqueness of the CB, and one about entity coherence.

Specifically:

In their own notation:

This file formalizes both predicates as length-properties of cbAll (Basic.lean §4) and proves the decomposition theorem. The length formulation makes the decomposition trivial — it falls out by omega once the predicates are stated in their canonical list-arithmetic form.

Why list arithmetic and not separate Props. The mathlib idiom encodes "at most one X" via the type system (Option, List.length ≤ 1, Subsingleton) rather than a parallel Unique predicate. Per the audit, cb : prev → cur → Option E already encodes uniqueness by type (at most one), and cbAll : prev → cur → List E exposes the multi-CB case PSDH study; the constraint-1 decomposition is then list arithmetic.

Total-ranking hypothesis. CB Uniqueness fails under partial rankings (PSDH §5.3.4 (10)): two realizations tied at the highest rank both qualify as CBs, so (cbAll prev cur).length = 2. Under a total ranking, ties cannot occur, so CB Uniqueness holds by construction. The unconditional decomposition theorem holds at the length level (length = 1 ↔ length ≤ 1 ∧ length ≥ 1), independent of the ranking; the empirical content of PSDH's analysis is which CenteringConfig instantiations make CB Uniqueness empirically high — that lives in the PoesioEtAl2004 study file, not in this substrate file.

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

CB Uniqueness (@cite{poesio-stevenson-eugenio-hitzeman-2004} §5.3.2 p. 357): the utterance pair (prev, cur) admits at most one candidate CB. Phrased as (cbAll prev cur).length ≤ 1.

Holds by construction under a total Cf-ranker. Fails under partial rankings when two realizations tie at the highest rank and both are realized in cur (PSDH §5.3.4 example (10)).

Equations
Instances For
    source
    def Discourse.Centering.EntityContinuity {E R : Type} [DecidableEq E] [CfRankerOf E R] {U : Type} [Realizes U E] (prev : Utterance E R) (cur : U) :
    Prop

    Entity Continuity (@cite{poesio-stevenson-eugenio-hitzeman-2004} §5.3.2 p. 357): the utterance pair (prev, cur) shares at least one CF entity — there exists a candidate CB. Phrased as (cbAll prev cur).length ≥ 1.

    PSDH equivalently formulate this as CF(U_{i-1}) ∩ CF(U_i) ≠ ∅; the cbAll formulation is the one consistent with cb's "highest-ranked realized" semantics.

    Equations
    Instances For
      source
      def Discourse.Centering.Constraint1Strong {E R : Type} [DecidableEq E] [CfRankerOf E R] {U : Type} [Realizes U E] (prev : Utterance E R) (cur : U) :
      Prop

      Strong Constraint 1 (@cite{grosz-joshi-weinstein-1995} §3, @cite{poesio-stevenson-eugenio-hitzeman-2004} §5.3.2): the pair has exactly one CB. Equivalently: CB Uniqueness ∧ Entity Continuity (the decomposition PSDH advocate).

      Equations
      Instances For

        Note on "Weak Constraint 1": PSDH §5.3.2 cite Walker, Joshi & Prince 1998 fn 2 p. 3 for the convention that "Weak C1" = just CB Uniqueness (vs. Strong C1 = Uniqueness ∧ Continuity). A previous version of this file declared Constraint1Weak prev cur := CBUniqueness prev cur plus weakC1_eq_uniqueness : Constraint1Weak ↔ CBUniqueness := Iff.rfl — the canonical naCanBridge = true := rfl anti-pattern (mathlib-reviewer audit-flagged). Use CBUniqueness directly when the "Weak C1" terminology is needed.

        source
        @[implicit_reducible]
        instance Discourse.Centering.CBUniqueness.decidable {E R : Type} [DecidableEq E] [CfRankerOf E R] {U : Type} [Realizes U E] (prev : Utterance E R) (cur : U) :
        Decidable (CBUniqueness prev cur)
        Equations
        source
        @[implicit_reducible]
        instance Discourse.Centering.EntityContinuity.decidable {E R : Type} [DecidableEq E] [CfRankerOf E R] {U : Type} [Realizes U E] (prev : Utterance E R) (cur : U) :
        Decidable (EntityContinuity prev cur)
        Equations
        source
        @[implicit_reducible]
        instance Discourse.Centering.Constraint1Strong.decidable {E R : Type} [DecidableEq E] [CfRankerOf E R] {U : Type} [Realizes U E] (prev : Utterance E R) (cur : U) :
        Decidable (Constraint1Strong prev cur)
        Equations
        source
        theorem Discourse.Centering.strongC1_iff_uniqueness_and_continuity {E R : Type} [DecidableEq E] [CfRankerOf E R] {U : Type} [Realizes U E] (prev : Utterance E R) (cur : U) :
        Constraint1Strong prev cur ↔ CBUniqueness prev cur ∧ EntityContinuity prev cur

        PSDH §5.3.2 decomposition (p. 356-357): Strong Constraint 1 is equivalent to the conjunction of CB Uniqueness and Entity Continuity. The proof falls out by omega from the canonical length = 1 ↔ length ≤ 1 ∧ length ≥ 1 arithmetic on Nat.

        PSDH propose this decomposition as a theoretical clarification: earlier work treated Constraint 1 as a single empirical claim, while in their corpus evaluation the two clauses behave differently — Weak C1 (CB Uniqueness alone) is verified by 82.7% of utterances under the vanilla instantiation, while Strong C1 holds for only 34.4% (PSDH Table 2, p. 328).

        source
        theorem Discourse.Centering.strong_implies_uniqueness {E R : Type} [DecidableEq E] [CfRankerOf E R] {U : Type} [Realizes U E] {prev : Utterance E R} {cur : U} (h : Constraint1Strong prev cur) :
        CBUniqueness prev cur

        Strong implies Weak: a unique CB implies at most one CB.