Coreference Theory

Abstract interface for coreference predictions.

inductive Interfaces.CoreferenceStatus : Type

The possible coreference relationships between two positions.

• obligatory : CoreferenceStatus

  Coreference is obligatory (reflexives with local antecedent)

• possible : CoreferenceStatus

  Coreference is possible but not required

• blocked : CoreferenceStatus

  Coreference is blocked (Principle B/C violations)

• unspecified : CoreferenceStatus

  No prediction (positions not in relevant configuration)

def Interfaces.instReprCoreferenceStatus.repr : CoreferenceStatus → Nat → Std.Format

Equations

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

instance Interfaces.instReprCoreferenceStatus : Repr CoreferenceStatus

Equations

• Interfaces.instReprCoreferenceStatus = { reprPrec := Interfaces.instReprCoreferenceStatus.repr }

instance Interfaces.instDecidableEqCoreferenceStatus : DecidableEq CoreferenceStatus

Equations

• Interfaces.instDecidableEqCoreferenceStatus x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

class Interfaces.CoreferenceTheory (T : Type) : Type 1

A theory that makes predictions about coreference patterns.

• Structure : Type

  The theory's internal representation of a sentence/structure

• parse : List Word → Option (Structure T)

  Parse a list of words into the theory's representation. Returns none if the theory can't parse this input.

• coreferenceStatus : Structure T → Nat → Nat → CoreferenceStatus

  Predict the coreference status between positions i and j.

  Positions are indexed from the word list:

  • "John sees himself" → position 0 = John, position 2 = himself

  Returns the theory's prediction about whether these positions can/must/cannot corefer.

• grammaticalForCoreference : Structure T → Bool

  Does the theory predict this sentence is grammatical for coreference?

  A sentence is "grammatical for coreference" if:

  • All obligatory coreferences have valid antecedents
  • No blocked coreferences are forced

  This is the primary prediction we test against empirical data.

def Interfaces.canCorefer {T : Type} [CoreferenceTheory T] (s : CoreferenceTheory.Structure T) (i j : Nat) : Bool

Check if coreference is possible at positions i, j

Equations

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

def Interfaces.mustCorefer {T : Type} [CoreferenceTheory T] (s : CoreferenceTheory.Structure T) (i j : Nat) : Bool

Check if coreference is obligatory at positions i, j

Equations

• Interfaces.mustCorefer s i j = match Interfaces.CoreferenceTheory.coreferenceStatus s i j with | Interfaces.CoreferenceStatus.obligatory => true | x => false

def Interfaces.cannotCorefer {T : Type} [CoreferenceTheory T] (s : CoreferenceTheory.Structure T) (i j : Nat) : Bool

Check if coreference is blocked at positions i, j

Equations

• Interfaces.cannotCorefer s i j = match Interfaces.CoreferenceTheory.coreferenceStatus s i j with | Interfaces.CoreferenceStatus.blocked => true | x => false

def Interfaces.capturesMinimalPair {T : Type} [CoreferenceTheory T] (pair : MinimalPair) : Bool

Does the theory correctly predict a minimal pair?

Equations

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

def Interfaces.capturesPhenomenon {T : Type} [CoreferenceTheory T] (data : PhenomenonData) : Bool

Does the theory capture all pairs in a phenomenon dataset?

Equations

• Interfaces.capturesPhenomenon data = data.pairs.all Interfaces.capturesMinimalPair

def Interfaces.theoriesAgreeOn {T1 T2 : Type} [CoreferenceTheory T1] [CoreferenceTheory T2] (ws : List Word) : Bool

Two theories agree on a sentence if they make the same grammaticality prediction

Equations

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

def Interfaces.theoriesAgreeOnAll {T1 T2 : Type} [CoreferenceTheory T1] [CoreferenceTheory T2] (sentences : List (List Word)) : Bool

Two theories agree on all sentences in a list

Equations

• Interfaces.theoriesAgreeOnAll sentences = sentences.all Interfaces.theoriesAgreeOn

def Interfaces.theoriesAgreeOnPhenomenon {T1 T2 : Type} [CoreferenceTheory T1] [CoreferenceTheory T2] (data : PhenomenonData) : Bool

Two theories agree on a phenomenon dataset

Equations

• Interfaces.theoriesAgreeOnPhenomenon data = data.pairs.all fun (pair : MinimalPair) => Interfaces.theoriesAgreeOn pair.grammatical && Interfaces.theoriesAgreeOn pair.ungrammatical

def Interfaces.ExtensionallyEquivalentOn {T1 T2 : Type} [CoreferenceTheory T1] [CoreferenceTheory T2] (sentences : List (List Word)) : Prop

Two theories are extensionally equivalent on a class of sentences.

Equations

• Interfaces.ExtensionallyEquivalentOn sentences = ∀ (ws : List Word), ws ∈ sentences → Interfaces.theoriesAgreeOn ws = true