Binding principles over a command relation

[BP90] [Cho81] [PS94]

A framework-neutral binding engine. The binding principles (A/B/C) and the coreference-status computation are stated once, parameterized by a CommandRelation — the structural-prominence order they range over. The three syntactic frameworks formalized in linglib supply that relation and inherit the principles unchanged:

• Minimalism — c-command (tree geometry)
• HPSG — ARG-ST outranking (obliqueness)
• Dependency grammar — d-command (dependency subgraph)

[BP90] give the general notion of which c-command, m-command, and the rest are instances; the linglib frameworks' command notions are further instances. Stating the principles over the abstract relation makes the cross-framework convergence a theorem rather than a coincidence: any two CommandRelations that agree on a clause predict the same binding facts.

Main declarations

• Pos — a binding position in a simple clause (subject / object).
• SimpleClause / parseSimpleClause — the clause representation the principles range over, and a surface-list parser.
• CommandRelation — the abstract command relation + locality (the only piece a framework supplies).
• reflexiveLicensed / reciprocalLicensed / pronounLocallyFree / rExpressionFree — Principles A / B / C, derived over [CommandRelation], Word.Agree, and a binding-class classifier.
• grammaticalForCoreference, computeCoreferenceStatus — top-level predictions, derived once.

Implementation notes

The binding-class classifier (Word → Option BindingClass) is a language parameter, orthogonal to the framework parameter CommandRelation; it is passed explicitly rather than baked in, so the engine imports no Fragment. A language (English, …) supplies the classifier; a framework supplies the command relation; a study combines them.

inductive Binding.Pos : Type

A binding position in a simple clause. The verb is not a binding position.

• subject : Pos
• object : Pos

@[implicit_reducible]

instance Binding.instDecidableEqPos : DecidableEq Pos

Equations

• Binding.instDecidableEqPos x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Binding.instReprPos : Repr Pos

Equations

• Binding.instReprPos = { reprPrec := Binding.instReprPos.repr }

def Binding.instReprPos.repr : Pos → ℕ → Std.Format

Equations

• Binding.instReprPos.repr Binding.Pos.subject prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Binding.Pos.subject")).group prec✝
• Binding.instReprPos.repr Binding.Pos.object prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Binding.Pos.object")).group prec✝

structure Binding.SimpleClause : Type

A simple (mono-clausal, transitive-or-intransitive) clause: the representation binding principles range over. semanticPl records whether the subject denotes a plurality, which can diverge from morphosyntactic number ([Rak19]); it defaults to the syntactic number.

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

@[implicit_reducible]

instance Binding.instReprSimpleClause : Repr SimpleClause

Equations

• Binding.instReprSimpleClause = { reprPrec := Binding.instReprSimpleClause.repr }

def Binding.instReprSimpleClause.repr : SimpleClause → ℕ → Std.Format

Equations

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

def Binding.SimpleClause.at? (c : SimpleClause) : Pos → Option Word

The Word at a position, if present.

Equations

• c.at? Binding.Pos.subject = some c.subject
• c.at? Binding.Pos.object = c.object

def Binding.isNominalCat (cat : UD.UPOS) : Bool

Is this a nominal part-of-speech (proper noun, common noun, or pronoun)? A theory-neutral UPOS check the clause parser uses to recognize arguments.

Equations

• Binding.isNominalCat cat = (cat == UD.UPOS.PROPN || cat == UD.UPOS.NOUN || cat == UD.UPOS.PRON)

def Binding.bindingClassOf : Features.BindingSource Word

The canonical, language-neutral binding-class source: a word's Principle A/B/C class read off its own UD morphology (Reflex, PronType) and category — no lexicon and no surface-form lookup. Reflexive morphology → anaphor; reciprocal PronType → reciprocal anaphor; any other pronoun → pronominal; a proper/common-noun category → R-expression; a non-nominal → none. This is the framework- and language-neutral default Features.BindingSource Word, replacing per-language form-string classifiers ([Cho81]'s A/B/C classes as morphology).

Equations

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

def Binding.parseSimpleClause (ws : List Word) : Option SimpleClause

Parse a surface word list into a simple clause: [subj, verb, obj] or [subj, verb], requiring nominal subject/object and a verb.

Equations

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

class Binding.CommandRelation : Type

A command relation ([BP90]): the structural-prominence order binding principles are defined over, together with the locality (same-binding-domain) restriction. The frameworks' c-command, ARG-ST outranking, and d-command are instances. This is the only component a syntactic framework must supply to obtain the binding principles.

• commands : SimpleClause → Pos → Pos → Prop

  Does the element at position i structurally command the element at j?

• sameDomain : SimpleClause → Pos → Pos → Prop

  Are positions i and j within the same binding (locality) domain?

• commandsDec (c : SimpleClause) (i j : Pos) : Decidable (commands c i j)

  commands is decidable — frameworks compute it from concrete structure.

• sameDomainDec (c : SimpleClause) (i j : Pos) : Decidable (sameDomain c i j)

  sameDomain is decidable.

@[implicit_reducible]

instance Binding.instDecidableCommands [CommandRelation] (c : SimpleClause) (i j : Pos) : Decidable (CommandRelation.commands c i j)

Equations

• Binding.instDecidableCommands c i j = Binding.CommandRelation.commandsDec c i j

@[implicit_reducible]

instance Binding.instDecidableSameDomain [CommandRelation] (c : SimpleClause) (i j : Pos) : Decidable (CommandRelation.sameDomain c i j)

Equations

• Binding.instDecidableSameDomain c i j = Binding.CommandRelation.sameDomainDec c i j

Principle A (anaphors)

def Binding.reflexiveLicensed [CommandRelation] (classify : Word → Option Features.BindingClass) (c : SimpleClause) : Prop

Principle A. A reflexive object is licensed iff it is commanded by the subject within the local domain and agrees with it in φ-features (Word.Agree). Vacuously true when the object is not a reflexive.

Equations

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

@[implicit_reducible]

instance Binding.instDecidableReflexiveLicensed [CommandRelation] (classify : Word → Option Features.BindingClass) (c : SimpleClause) : Decidable (reflexiveLicensed classify c)

Equations

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

def Binding.reciprocalLicensed [CommandRelation] (classify : Word → Option Features.BindingClass) (c : SimpleClause) : Prop

Principle A for reciprocals: licensed iff commanded by the subject in the local domain and the subject denotes a plurality (an LF condition — semantic, not morphosyntactic, plurality; [Rak19]).

Equations

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

@[implicit_reducible]

instance Binding.instDecidableReciprocalLicensed [CommandRelation] (classify : Word → Option Features.BindingClass) (c : SimpleClause) : Decidable (reciprocalLicensed classify c)

Equations

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

Principle B (pronouns)

def Binding.pronounLocallyFree [CommandRelation] (classify : Word → Option Features.BindingClass) (c : SimpleClause) : Prop

Principle B. A pronoun object must be free in its local domain: it must not be both commanded by the subject and in the same domain.

Equations

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

@[implicit_reducible]

instance Binding.instDecidablePronounLocallyFree [CommandRelation] (classify : Word → Option Features.BindingClass) (c : SimpleClause) : Decidable (pronounLocallyFree classify c)

Equations

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

Principle C (R-expressions)

def Binding.rExpressionFree [CommandRelation] (classify : Word → Option Features.BindingClass) (c : SimpleClause) : Prop

Principle C. An R-expression object coindexed with a pronominal subject is blocked when the subject commands it.

Equations

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

@[implicit_reducible]

instance Binding.instDecidableRExpressionFree [CommandRelation] (classify : Word → Option Features.BindingClass) (c : SimpleClause) : Decidable (rExpressionFree classify c)

Equations

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

Top-level acceptability

def Binding.grammaticalForCoreference [CommandRelation] (classify : Word → Option Features.BindingClass) (ws : List Word) : Prop

Is a surface word list grammatical for coreference? Anaphors cannot be subjects (no commander); a pronoun object locally commanded by the subject violates Principle B; reflexive/reciprocal objects must be licensed.

Equations

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

@[implicit_reducible]

instance Binding.instDecidableGrammaticalForCoreference [CommandRelation] (classify : Word → Option Features.BindingClass) (ws : List Word) : Decidable (grammaticalForCoreference classify ws)

Equations

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

def Binding.computeCoreferenceStatus [CommandRelation] (classify : Word → Option Features.BindingClass) (c : SimpleClause) (i j : Pos) : Features.CoreferenceStatus

Coreference status of positions i, j under the command relation: Principle A makes a commanded anaphor obligatorily coreferent; Principle B/C block a commanded pronoun/R-expression; otherwise coreference is possible.

Equations

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

Cross-framework convergence

Stated over the abstract relation, the principles depend on the framework only through CommandRelation. Two frameworks that agree on a clause's command and locality facts therefore make identical binding predictions — by construction, not coincidence.

theorem Binding.reflexiveLicensed_congr (R₁ R₂ : CommandRelation) (classify : Word → Option Features.BindingClass) (c : SimpleClause) (hc : CommandRelation.commands c Pos.subject Pos.object ↔ CommandRelation.commands c Pos.subject Pos.object) (hd : CommandRelation.sameDomain c Pos.subject Pos.object ↔ CommandRelation.sameDomain c Pos.subject Pos.object) : reflexiveLicensed classify c ↔ reflexiveLicensed classify c

If two command relations agree on the relevant command and locality facts of a clause, they license a reflexive identically. The cross-framework convergence the prose comparisons assert, made a theorem.