def HPSG.Coreference.isNominalCat (c : UD.UPOS) : Bool

Is this a nominal category?

Equations

• HPSG.Coreference.isNominalCat c = (c == UD.UPOS.PROPN || c == UD.UPOS.NOUN || c == UD.UPOS.PRON)

def HPSG.Coreference.classifyMode (w : Word) : Option Mode

Derive MODE feature from a word.

Per @cite{sag-wasow-bender-2003} Ch. 7:

• Reflexives and reciprocals → [MODE ana]
• Personal pronouns and R-expressions → [MODE ref]

Equations

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

def HPSG.Coreference.isAnaphor (w : Word) : Bool

Is this word an anaphor ([MODE ana])?

Equations

• HPSG.Coreference.isAnaphor w = (HPSG.Coreference.classifyMode w == some HPSG.Mode.ana)

def HPSG.Coreference.isReflexive (w : Word) : Bool

Is this word a reflexive specifically?

Equations

• HPSG.Coreference.isReflexive w = decide (w.form ∈ ["himself", "herself", "themselves", "myself", "yourself", "ourselves"])

def HPSG.Coreference.isReciprocal (w : Word) : Bool

Is this word a reciprocal?

Equations

• HPSG.Coreference.isReciprocal w = decide (w.form ∈ ["each other", "one another"])

inductive HPSG.Coreference.NominalType : Type

Types of nominal expressions for coreference.

Implementation convenience for dispatching agreement checks. Both pronoun and rExpression map to [MODE ref] in SWB2003.

• reflexive : NominalType
• reciprocal : NominalType
• pronoun : NominalType
• rExpression : NominalType

@[implicit_reducible]

instance HPSG.Coreference.instReprNominalType : Repr NominalType

Equations

• HPSG.Coreference.instReprNominalType = { reprPrec := HPSG.Coreference.instReprNominalType.repr }

def HPSG.Coreference.instReprNominalType.repr : NominalType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance HPSG.Coreference.instDecidableEqNominalType : DecidableEq NominalType

Equations

• HPSG.Coreference.instDecidableEqNominalType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def HPSG.Coreference.classifyNominal (w : Word) : Option NominalType

Classify a word as a nominal type.

This maps to MODE as follows:

• reflexive, reciprocal → [MODE ana]
• pronoun, rExpression → [MODE ref]

The pronoun/rExpression distinction is useful for implementation (e.g., agreement checks) but both are [MODE ref] in SWB2003.

Equations

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

structure HPSG.Coreference.SimpleClause : Type

Simple clause structure with ARG-ST for binding.

ARG-ST is implicitly [subject, object] — subject at position 0 outranks object at position 1.

• subject : Word
• verb : Word
• object : Option Word
• semanticPl : Bool

  Whether the subject denotes a plurality. Defaults to matching syntactic number. Override for languages where syntactic and semantic number diverge (@cite{rakosi-2019}).

@[implicit_reducible]

instance HPSG.Coreference.instReprSimpleClause : Repr SimpleClause

Equations

• HPSG.Coreference.instReprSimpleClause = { reprPrec := HPSG.Coreference.instReprSimpleClause.repr }

def HPSG.Coreference.instReprSimpleClause.repr : SimpleClause → ℕ → Std.Format

Equations

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

def HPSG.Coreference.parseSimpleClause (ws : List Word) : Option SimpleClause

Parse a simple transitive sentence into a clause.

Equations

• One or more equations did not get rendered due to their size.
• HPSG.Coreference.parseSimpleClause [subj, v] = if (HPSG.Coreference.isNominalCat subj.cat && v.cat == UD.UPOS.VERB) = true then some { subject := subj, verb := v, object := none } else none
• HPSG.Coreference.parseSimpleClause ws = none

def HPSG.Coreference.SimpleClause.toArgSt (clause : SimpleClause) : ArgSt

Build the ARG-ST for a simple clause from its arguments.

ARG-ST = [subject, object] — the verb's argument structure list, ordered by obliqueness (@cite{sag-wasow-bender-2003} Ch. 7).

Equations

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

def HPSG.Coreference.subjectOutranksObject (clause : SimpleClause) : Bool

Does the subject outrank the object on ARG-ST?

Derived from ArgSt.outranks: subject at position 0 outranks object at position 1 iff 0 < 1 ∧ 1 < args.length.

Equations

• HPSG.Coreference.subjectOutranksObject clause = clause.toArgSt.outranks 0 1

def HPSG.Coreference.sameArgSt (clause : SimpleClause) : Bool

Subject and object are on the same ARG-ST list: both are valid indices in the ARG-ST built from the verb's argument structure.

Equations

• HPSG.Coreference.sameArgSt clause = match clause.object with | none => true | some val => decide (1 < clause.toArgSt.args.length)

def HPSG.Coreference.phiAgree (w1 w2 : Word) : Bool

Anaphoric Agreement Principle (AAP): coindexed elements must agree.

Per @cite{sag-wasow-bender-2003} Ch. 7: "Coindexed NPs agree."

Equations

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

def HPSG.Coreference.reflexiveLicensed (clause : SimpleClause) : Bool

Principle A (SWB2003): An anaphor ([MODE ana]) must be outranked by a coindexed element on the same ARG-ST list.

For reflexives, the coindexed antecedent must also satisfy the AAP.

Equations

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

def HPSG.Coreference.reciprocalLicensed (clause : SimpleClause) : Bool

Principle A for reciprocals: a reciprocal ([MODE ana]) must be outranked by a semantically plural coindexed element. The plurality requirement is semantic (LF), not morphosyntactic — reciprocals are licensed by quantified NPs, singular coordinate DPs, and collective nouns that are syntactically singular (@cite{rakosi-2019}).

Equations

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

def HPSG.Coreference.refLocallyFree (clause : SimpleClause) : Bool

Principle B (SWB2003): A [MODE ref] element must NOT be outranked by a coindexed element on the same ARG-ST list.

This applies to both pronouns and R-expressions (both are [MODE ref]). In a simple clause, the subject outranks the object, so any [MODE ref] object that is coindexed with the subject violates Principle B.

Note: grammaticalForCoreference only tests this for pronouns, since R-expression objects are typically not coindexed with the subject. computeCoreferenceStatus applies Principle B to all [MODE ref] elements for explicit coindexation queries.

Equations

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

def HPSG.Coreference.grammaticalForCoreference (ws : List Word) : Bool

Is a sentence free of binding violations under HPSG binding theory?

Checks Principle A (anaphors must be outranked) and Principle B (pronouns must not be locally bound).

For R-expression objects, no binding violation arises because coindexation with the subject is not assumed. Use computeCoreferenceStatus for explicit coindexation queries.

Equations

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

def HPSG.Coreference.reflexiveLicensedInSentence (ws : List Word) : Bool

Check if reflexive is licensed in a sentence

Equations

• HPSG.Coreference.reflexiveLicensedInSentence ws = match HPSG.Coreference.parseSimpleClause ws with | none => false | some clause => HPSG.Coreference.reflexiveLicensed clause

def HPSG.Coreference.localCoreferenceBlocked (ws : List Word) : Bool

Check if local coreference is blocked by Principle B ([MODE ref]).

Applies to both pronouns and R-expressions.

Equations

• HPSG.Coreference.localCoreferenceBlocked ws = match HPSG.Coreference.parseSimpleClause ws with | none => false | some clause => !HPSG.Coreference.refLocallyFree clause

def HPSG.Coreference.capturesCoreferenceMinimalPair (pair : Paradigms.AcceptabilityJudgment.MinimalPair) : Bool

Check if HPSG correctly predicts a minimal pair for coreference

Grammatical sentence should pass, ungrammatical should fail.

Equations

• HPSG.Coreference.capturesCoreferenceMinimalPair pair = (HPSG.Coreference.grammaticalForCoreference pair.grammatical && !HPSG.Coreference.grammaticalForCoreference pair.ungrammatical)

def HPSG.Coreference.capturesCoreferenceData (phenom : Paradigms.AcceptabilityJudgment.PhenomenonData) : Bool

Check all pairs in a PhenomenonData

Equations

• HPSG.Coreference.capturesCoreferenceData phenom = phenom.pairs.all HPSG.Coreference.capturesCoreferenceMinimalPair

theorem HPSG.Coreference.reflexive_pairs_captured : (grammaticalForCoreference [john✝, sees✝, himself✝] = true ∧ grammaticalForCoreference [himself✝, sees✝, john✝] = false) ∧ (grammaticalForCoreference [mary✝, sees✝, herself✝] = true ∧ grammaticalForCoreference [herself✝, sees✝, mary✝] = false) ∧ (grammaticalForCoreference [they✝, see✝, themselves✝] = true ∧ grammaticalForCoreference [themselves✝, see✝, them✝] = false) ∧ (grammaticalForCoreference [john✝, sees✝, himself✝] = true ∧ grammaticalForCoreference [john✝, sees✝, herself✝] = false) ∧ (grammaticalForCoreference [they✝, see✝, themselves✝] = true ∧ grammaticalForCoreference [they✝, see✝, himself✝] = false) ∧ (grammaticalForCoreference [they✝, see✝, eachOther✝] = true ∧ grammaticalForCoreference [eachOther✝, see✝, them✝] = false) ∧ grammaticalForCoreference [they✝, see✝, eachOther✝] = true ∧ grammaticalForCoreference [john✝, sees✝, eachOther✝] = false

Check each pair individually for reflexive coreference

def HPSG.Coreference.computeCoreferenceStatus (clause : SimpleClause) (i j : ℕ) : Features.CoreferenceStatus

Compute coreference status for positions i and j using ARG-ST outranking.

Position 0 = subject, position 2 = object.

Applies both binding principles uniformly:

• Principle A: [MODE ana] at j outranked by coindexed i → obligatory
• Principle B: [MODE ref] at j outranked by coindexed i → blocked

Equations

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