Features.CoreferenceStatus

Cross-framework coreference verdict enum. Syntactic frameworks (HPSG, Dependency Grammar, Minimalism) each provide a computeCoreferenceStatus : ... → CoreferenceStatus function — the shared return type is what makes their predictions comparable rather than each framework's verdict living in a private namespace.

inductive Features.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 Features.instReprCoreferenceStatus.repr : CoreferenceStatus → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Features.instReprCoreferenceStatus : Repr CoreferenceStatus

Equations

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

@[implicit_reducible]

instance Features.instDecidableEqCoreferenceStatus : DecidableEq CoreferenceStatus

Equations

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

inductive Features.BindingClass : Type

The binding-theoretic class of a nominal expression, shared across the syntactic frameworks (HPSG, Dependency Grammar, Minimalism) so their binding-class sources return the same type. The canonical source reads the class off a word's own UD morphology (Binding.bindingClassOf).

The binding-distribution axis (anaphor/pronominal/r-expression, with the anaphor class split into reflexive/reciprocal) — orthogonal to a nominal's Semantics.Definiteness.Description (definiteness/reference flavor) and to a pronoun's lexical kind.

• reflexive : BindingClass

  Reflexive anaphor (himself, herself, themselves).

• reciprocal : BindingClass

  Reciprocal anaphor (each other, one another).

• pronoun : BindingClass

  Personal/other pronoun (he, she, they, …).

• rExpression : BindingClass

  Referring expression (proper name, full NP).

@[implicit_reducible]

instance Features.instReprBindingClass : Repr BindingClass

Equations

• Features.instReprBindingClass = { reprPrec := Features.instReprBindingClass.repr }

def Features.instReprBindingClass.repr : BindingClass → Nat → Std.Format

Equations

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

def Features.instBEqBindingClass.beq : BindingClass → BindingClass → Bool

Equations

• Features.instBEqBindingClass.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance Features.instBEqBindingClass : BEq BindingClass

Equations

• Features.instBEqBindingClass = { beq := Features.instBEqBindingClass.beq }

@[implicit_reducible]

instance Features.instDecidableEqBindingClass : DecidableEq BindingClass

Equations

• Features.instDecidableEqBindingClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[reducible, inline]

abbrev Features.BindingSource (α : Type u_1) : Type u_1

A binding-class source: where an expression's BindingClass comes from. Theories source it differently — a word's own UD morphology (Binding.bindingClassOf, the canonical language-neutral source), a lexical declaration (Pronoun.bindingClass), a structural sort (HPSG), or the syntactic context (minimal-pronoun / DM). The framework-neutral binding engine is polymorphic over the source: it takes a BindingSource and stays agnostic to where the class came from.

Equations

• Features.BindingSource α = (α → Option Features.BindingClass)

The Bound capability: total binding class on a carrier

The typeclass face of the binding-class axis, beside its partial companion Features.BindingSource. The class is theory-neutral and lives here; each carrier's instance lives with the carrier (Pronoun in Syntax/Pronoun/Capabilities.lean, Italian clitics and Turkish anaphors in their Fragments).

class Bound (α : Type u_1) : Type u_1

A carrier whose every element carries a (total) Features.BindingClass — its Principle A/B/C role. The typed companion to Features.BindingSource (α → Option BindingClass, the partial source the framework-neutral binding engine consumes): Bound is the case where the kind fixes the class for the whole carrier.

• bindingClass : α → Features.BindingClass

  The Principle A anaphor / B pronominal / C R-expression class.

def Bound.source {α : Type u_1} [Bound α] : Features.BindingSource α

A [Bound α] carrier's Features.BindingSource — the canonical mixin → source bridge: every element classifies, so the source is total (some everywhere).

Equations

• Bound.source a = some (Bound.bindingClass a)

class Anaphoric (α : Type u_1) [Bound α] : Prop

Principle-A carrier: every element is an anaphor (reflexive or reciprocal).

• isAnaphor (a : α) : Bound.bindingClass a = Features.BindingClass.reflexive ∨ Bound.bindingClass a = Features.BindingClass.reciprocal

class Pronominal (α : Type u_1) [Bound α] : Prop

Principle-B carrier: every element is a pronominal.

• isPronominal (a : α) : Bound.bindingClass a = Features.BindingClass.pronoun

class Referring (α : Type u_1) [Bound α] : Prop

Principle-C carrier: every element is a referring expression (an R-expression — proper name, full NP). Named for the adjectival parallel with Anaphoric/Pronominal.

• isReferring (a : α) : Bound.bindingClass a = Features.BindingClass.rExpression

def Bound.IsAnaphor {α : Type u_1} [Bound α] (a : α) : Prop

a is a Principle-A anaphor (reflexive or reciprocal) — the A/B/C partition as an element predicate over any [Bound α] carrier (a Pronoun, an Italian clitic, a Turkish anaphor, …). The element-level companion to the carrier-level Anaphoric type-marker.

Equations

• Bound.IsAnaphor a = (Bound.bindingClass a = Features.BindingClass.reflexive ∨ Bound.bindingClass a = Features.BindingClass.reciprocal)

def Bound.IsPronominal {α : Type u_1} [Bound α] (a : α) : Prop

a is a Principle-B pronominal.

Equations

• Bound.IsPronominal a = (Bound.bindingClass a = Features.BindingClass.pronoun)

def Bound.IsRExpression {α : Type u_1} [Bound α] (a : α) : Prop

a is a Principle-C R-expression.

Equations

• Bound.IsRExpression a = (Bound.bindingClass a = Features.BindingClass.rExpression)

@[implicit_reducible]

instance instDecidableIsAnaphor {α : Type u_1} [Bound α] (a : α) : Decidable (Bound.IsAnaphor a)

Equations

• instDecidableIsAnaphor a = id inferInstance

@[implicit_reducible]

instance instDecidableIsPronominal {α : Type u_1} [Bound α] (a : α) : Decidable (Bound.IsPronominal a)

Equations

• instDecidableIsPronominal a = id inferInstance

@[implicit_reducible]

instance instDecidableIsRExpression {α : Type u_1} [Bound α] (a : α) : Decidable (Bound.IsRExpression a)

Equations

• instDecidableIsRExpression a = id inferInstance