Pronoun capabilities

Typeclass mixins for pronoun-like carriers. A carrier may be a lexical record (Pronoun, PersonalPronoun) or a surface token (Word); a consumer requires exactly the axes it touches.

Main declarations

• Proform — a pro-form takes its antecedents from a fixed form-class, its domain ([Blo33]); Proform.CandidateAntecedent is derived — domain membership plus φ-agreement (HasPhi.Agree, from Features/Phi.lean).
• Bound, HasNumber, HasPerson, HasCase, HasGender instances for the pronoun carriers.
• bindingClassOf_toWord, numberOf_toWord, personOf_toWord, caseOf_toWord, genderOf_toWord — Pronoun.toWord commutes with each axis, up to what UD realization can express: clusivity, minimal/augmented number, and animacy-based gender are lost; case and binding class are preserved.

Implementation notes

Word-class-neutral capabilities live with their domains: Indefinite in Features/Indefinite.lean, Bound in Features/CoreferenceStatus.lean. Three axes are fields, not classes: deficiency (Pronoun.strength, per-series [cardinaletti-starke-1999]), lexical kind (Pronoun.pronType, UD morphology), and register/referential person (PersonalPronoun fields, borne by one carrier).

Proform.CandidateAntecedent is token-level: whether an anaphoric site is a bare pro-form or hosts deleted structure ([hankamer-sag-1976]; [baltin-2012]) is a theory question for study files.

φ instances and the pro-form

@[instance_reducible]

instance instHasPhiPronoun : HasPhi Pronoun

Equations

• instHasPhiPronoun = { phi := fun (p : Pronoun) => p.toWord.phi }

@[instance_reducible]

instance instHasPhiPersonalPronoun : HasPhi PersonalPronoun

Equations

• instHasPhiPersonalPronoun = { phi := fun (p : PersonalPronoun) => p.toWord.phi }

theorem HasPhi.agree_toWord {β : Type u_1} [HasPhi β] (p : Pronoun) (b : β) : Agree p b ↔ Agree p.toWord b

A pronoun agrees exactly as its projected word does.

class Proform (α : Type u_1) : Type u_1

A pro-form takes its antecedents from a fixed form-class — its domain (the notion originates with [Blo33]'s substitutes).

• Domain : α → Morphology.Word → Prop

  w is in the form-class a stands for.

def Proform.CandidateAntecedent {α : Type u_1} [Proform α] [HasPhi α] (a : α) (w : Morphology.Word) : Prop

A candidate antecedent for a pro-form is a domain member that φ-agrees with it.

Equations

• Proform.CandidateAntecedent a w = (Proform.Domain a w ∧ HasPhi.Agree a w)

theorem Proform.CandidateAntecedent.agree {α : Type u_1} [Proform α] [HasPhi α] {a : α} {w : Morphology.Word} (h : CandidateAntecedent a w) : HasPhi.Agree a w

A candidate antecedent φ-agrees with its pro-form.

@[instance_reducible]

instance instProformPronoun : Proform Pronoun

A pronoun's domain is the nominal tokens.

Equations

• instProformPronoun = { Domain := fun (x : Pronoun) (w : Morphology.Word) => Binding.isNominalCat w.cat = true }

@[instance_reducible]

instance instProformPersonalPronoun : Proform PersonalPronoun

Equations

• instProformPersonalPronoun = { Domain := fun (x : PersonalPronoun) (w : Morphology.Word) => Binding.isNominalCat w.cat = true }

@[instance_reducible]

instance instDecidableDomainPronoun (p : Pronoun) (w : Morphology.Word) : Decidable (Proform.Domain p w)

Equations

• instDecidableDomainPronoun p w = instDecidableEqBool (Binding.isNominalCat w.cat) true

@[instance_reducible]

instance instDecidableDomainPersonalPronoun (p : PersonalPronoun) (w : Morphology.Word) : Decidable (Proform.Domain p w)

Equations

• instDecidableDomainPersonalPronoun p w = instDecidableEqBool (Binding.isNominalCat w.cat) true

@[instance_reducible]

instance instDecidableCandidateAntecedentOfDomain {α : Type u_1} [Proform α] [HasPhi α] (a : α) (w : Morphology.Word) [Decidable (Proform.Domain a w)] : Decidable (Proform.CandidateAntecedent a w)

Equations

• instDecidableCandidateAntecedentOfDomain a w = id inferInstance

The pronoun carriers' Bound instances, and the faithfulness certificate

@[instance_reducible]

instance instBoundPronoun : Bound Pronoun

A bare Pronoun's class is its declared bindingClass; an undeclared φ-shell defaults to Principle-B .pronoun ([chomsky-1981]'s elsewhere case).

Equations

• instBoundPronoun = { bindingClass := fun (p : Pronoun) => p.bindingClass.getD Features.BindingClass.pronoun }

@[instance_reducible]

instance instBoundPersonalPronoun : Bound PersonalPronoun

Equations

• instBoundPersonalPronoun = { bindingClass := fun (p : PersonalPronoun) => p.bindingClass.getD Features.BindingClass.pronoun }

theorem bindingClassOf_toWord (p : Pronoun) (h : p.bindingClass ≠ some Features.BindingClass.rExpression) (hr : p.pronType = some UD.PronType.Rcp → p.bindingClass = some Features.BindingClass.reciprocal) : Binding.bindingClassOf p.toWord = Bound.source p

A pronoun's projected word classifies (Binding.bindingClassOf) exactly as its Bound class.

The number axis: HasNumber instances and faithfulness

@[instance_reducible]

instance instHasNumberPronoun : HasNumber Pronoun

Equations

• instHasNumberPronoun = { numberOf := fun (p : Pronoun) => p.number }

@[instance_reducible]

instance instHasNumberPersonalPronoun : HasNumber PersonalPronoun

Equations

• instHasNumberPersonalPronoun = { numberOf := fun (p : PersonalPronoun) => numberOf p.toPronoun }

theorem numberOf_toWord (p : Pronoun) : numberOf p.toWord = p.number.bind fun (n : Number) => n.toUD.bind Number.fromUD

A pronoun's number survives projection to Word exactly on UD-expressible values; the minimal/augmented values are lost, since Number.toUD is partial.

The person axis: HasPerson instances and faithfulness

@[instance_reducible]

instance instHasPersonPronoun : HasPerson Pronoun

Equations

• instHasPersonPronoun = { personOf := fun (p : Pronoun) => p.person }

@[instance_reducible]

instance instHasPersonPersonalPronoun : HasPerson PersonalPronoun

Equations

• instHasPersonPersonalPronoun = { personOf := fun (p : PersonalPronoun) => personOf p.toPronoun }

theorem personOf_toWord (p : Pronoun) : personOf p.toWord = Option.map Person.coarsen (personOf p)

Projection to Word coarsens person, since UD realization has no clusivity.

The case axis: HasCase instances and faithfulness

@[instance_reducible]

instance instHasCasePronoun : HasCase Pronoun

Equations

• instHasCasePronoun = { caseOf := fun (p : Pronoun) => p.case_ }

@[instance_reducible]

instance instHasCasePersonalPronoun : HasCase PersonalPronoun

Equations

• instHasCasePersonalPronoun = { caseOf := fun (p : PersonalPronoun) => caseOf p.toPronoun }

theorem caseOf_toWord (p : Pronoun) : caseOf p.toWord = caseOf p

Projection to Word preserves case, since Case.toUD is a bijection.

The gender axis: HasGender instances and faithfulness

@[instance_reducible]

instance instHasGenderPronoun : HasGender Pronoun

Equations

• instHasGenderPronoun = { genderOf := fun (p : Pronoun) => p.gender }

@[instance_reducible]

instance instHasGenderPersonalPronoun : HasGender PersonalPronoun

Equations

• instHasGenderPersonalPronoun = { genderOf := fun (p : PersonalPronoun) => genderOf p.toPronoun }

theorem genderOf_toWord (p : Pronoun) : genderOf p.toWord = p.gender.bind fun (g : Gender) => Option.map Gender.fromUD g.toUD

A pronoun's gender survives projection to Word exactly on UD-expressible values; the animacy-based labels are lost, since Gender.toUD is partial.