Minimalist Coreference (Binding)

Coreference constraints via c-command and locality following @cite{chomsky-1981}.

Main definitions

• NominalType, SimpleClause
• reflexiveLicensed, pronounLocallyFree, grammaticalForCoreference

inductive Minimalist.Coreference.NominalType : Type

Types of nominal expressions for coreference

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

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

Equations

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

@[implicit_reducible]

instance Minimalist.Coreference.instReprNominalType : Repr NominalType

Equations

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

@[implicit_reducible]

instance Minimalist.Coreference.instDecidableEqNominalType : DecidableEq NominalType

Equations

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

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

Is this a nominal category?

Equations

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

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

Classify a word as a nominal type. Derives classification from Fragments.English.Pronouns rather than hardcoding string lists. Falls back to UPOS for R-expressions.

Equations

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

structure Minimalist.Coreference.SimpleClause : Type

Simple clause structure for coreference checking. semanticPl tracks whether the subject denotes a plurality, independently of syntactic number. In English, these coincide. In Hungarian, quantified NPs, singular coordinate DPs, and collective nouns are syntactically singular but semantically plural (@cite{rakosi-2019}). Defaults to matching syntactic number.

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

  Whether the subject denotes a plurality (multiple individuals). Defaults to matching the syntactic number feature. Override for languages where syntactic and semantic number diverge.

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

Equations

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

@[implicit_reducible]

instance Minimalist.Coreference.instReprSimpleClause : Repr SimpleClause

Equations

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

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

Equations

• One or more equations did not get rendered due to their size.
• Minimalist.Coreference.parseSimpleClause ws = none

def Minimalist.Coreference.SimpleClause.toSyntacticObject (clause : SimpleClause) : SyntacticObject

Build a phrase structure tree from a simple clause.

Transitive: {subj, {verb, obj}} — subject is specifier, verb–object is a head-complement pair. Intransitive: {subj, verb} — subject and verb are co-daughters.

C-command follows from the tree geometry:

• Subject c-commands object (subject's sister contains object)
• Object does NOT c-command subject (object's sister is verb leaf)

Equations

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

def Minimalist.Coreference.subjectCCommandsObject (clause : SimpleClause) : Prop

Subject c-commands object: derived from the phrase structure tree. In {subj, {verb, obj}}, the subject's sister is {verb, obj}, which contains the object.

Equations

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

@[implicit_reducible]

instance Minimalist.Coreference.instDecidableSubjectCCommandsObject (clause : SimpleClause) : Decidable (subjectCCommandsObject clause)

Equations

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

def Minimalist.Coreference.objectCCommandsSubject (clause : SimpleClause) : Prop

Object does not c-command subject: derived from the tree. In {subj, {verb, obj}}, the object's sister is verb, which does not contain the subject.

Equations

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

@[implicit_reducible]

instance Minimalist.Coreference.instDecidableObjectCCommandsSubject (clause : SimpleClause) : Decidable (objectCCommandsSubject clause)

Equations

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

def Minimalist.Coreference.sameLocalDomain (clause : SimpleClause) : Prop

Same local domain: both subject and object are subterms of the same clause tree (the minimal domain containing a SUBJECT).

Equations

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

@[implicit_reducible]

instance Minimalist.Coreference.instDecidableSameLocalDomain (clause : SimpleClause) : Decidable (sameLocalDomain clause)

Equations

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

def Minimalist.Coreference.inSameBindingDomain (_clause : SimpleClause) (_pos1 _pos2 : String) : Prop

Binding domain check: in a simple clause, all positions share a domain.

Equations

• Minimalist.Coreference.inSameBindingDomain _clause _pos1 _pos2 = True

@[implicit_reducible]

instance Minimalist.Coreference.instDecidableInSameBindingDomain (clause : SimpleClause) (pos1 pos2 : String) : Decidable (inSameBindingDomain clause pos1 pos2)

Equations

• Minimalist.Coreference.instDecidableInSameBindingDomain clause pos1 pos2 = id inferInstance

def Minimalist.Coreference.phiAgree (w1 w2 : Word) : Prop

Phi-feature agreement for coreference. Checks person, number, and gender agreement between antecedent and anaphor. Person and number come from Word.Features; gender uses Fragments.English.Pronouns.genderAgrees since Word currently lacks a gender field.

Equations

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

@[implicit_reducible]

instance Minimalist.Coreference.instDecidablePhiAgree (w1 w2 : Word) : Decidable (phiAgree w1 w2)

Equations

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

def Minimalist.Coreference.reflexiveLicensed (clause : SimpleClause) : Prop

Principle A: Reflexives must be bound locally

Equations

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

@[implicit_reducible]

instance Minimalist.Coreference.instDecidableReflexiveLicensed (clause : SimpleClause) : Decidable (reflexiveLicensed clause)

Equations

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

def Minimalist.Coreference.reciprocalLicensed (clause : SimpleClause) : Prop

Reciprocals must be locally c-commanded by a semantically plural antecedent. Unlike reflexive licensing (which uses narrow-syntactic φ-agreement, hence requires morphosyntactic plurality), reciprocal licensing is an LF interpretive condition under the Y-model: the antecedent must denote a plurality, but need not bear plural morphology or trigger plural verb agreement. @cite{rakosi-2019}: Hungarian egymás is licensed by quantified NPs, singular coordinate DPs, and collective nouns — all syntactically singular but semantically plural.

Equations

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

@[implicit_reducible]

instance Minimalist.Coreference.instDecidableReciprocalLicensed (clause : SimpleClause) : Decidable (reciprocalLicensed clause)

Equations

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

def Minimalist.Coreference.pronounLocallyFree (clause : SimpleClause) : Prop

Principle B: Pronouns must be free locally

Equations

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

@[implicit_reducible]

instance Minimalist.Coreference.instDecidablePronounLocallyFree (clause : SimpleClause) : Decidable (pronounLocallyFree clause)

Equations

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

def Minimalist.Coreference.rExpressionFree (clause : SimpleClause) : Prop

Principle C: R-expressions must be free everywhere.

An R-expression is free iff no coreferential pronoun c-commands it. In a simple clause {subj, {verb, obj}}, a pronominal subject c-commands the object (via tree-relative cCommandsIn), so subject–object coreference with an R-expression object is blocked.

Note: WLM (@cite{takahashi-hulsey-2009}, @cite{gong-2022}) can bleed Condition C by merging the NP restrictor at a chain position above the binder. This function checks the surface tree; the WLM escape is modeled via wlmAvoidsCondC in LateMerger.lean.

Equations

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

@[implicit_reducible]

instance Minimalist.Coreference.instDecidableRExpressionFree (clause : SimpleClause) : Decidable (rExpressionFree clause)

Equations

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

def Minimalist.Coreference.grammaticalForCoreference (ws : List Word) : Prop

Grammatical for coreference under Minimalist binding

Equations

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

@[implicit_reducible]

instance Minimalist.Coreference.instDecidableGrammaticalForCoreference (ws : List Word) : Decidable (grammaticalForCoreference ws)

Equations

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

def Minimalist.Coreference.reflexiveLicensedInSentence (ws : List Word) : Prop

Equations

• Minimalist.Coreference.reflexiveLicensedInSentence ws = match Minimalist.Coreference.parseSimpleClause ws with | none => False | some clause => Minimalist.Coreference.reflexiveLicensed clause

@[implicit_reducible]

instance Minimalist.Coreference.instDecidableReflexiveLicensedInSentence (ws : List Word) : Decidable (reflexiveLicensedInSentence ws)

Equations

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

def Minimalist.Coreference.pronounCoreferenceBlocked (ws : List Word) : Prop

Equations

• Minimalist.Coreference.pronounCoreferenceBlocked ws = match Minimalist.Coreference.parseSimpleClause ws with | none => False | some clause => ¬Minimalist.Coreference.pronounLocallyFree clause

@[implicit_reducible]

instance Minimalist.Coreference.instDecidablePronounCoreferenceBlocked (ws : List Word) : Decidable (pronounCoreferenceBlocked ws)

Equations

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

structure Minimalist.Coreference.MinimalistCoreferenceGrammar : Type

• strictLocality : Bool

def Minimalist.Coreference.defaultGrammar : MinimalistCoreferenceGrammar

Equations

• Minimalist.Coreference.defaultGrammar = { }

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

Equations

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