Reflexive pronouns

A reflexive pronoun is a pronoun whose kind fixes its binding class: it is an anaphor, bound in its local domain. Some reflexives, as Japanese zibun and Icelandic sig, also take an antecedent outside that domain; what licenses the distant antecedent is a matter of analysis and is not recorded on the entry.

Main definitions

• ReflexivePronoun: a pronoun of the reflexive kind.
• ReflexivePronoun.paradigm: the forms an inventory offers for each category its person and number realize.
• ReflexivePronoun.toWord: its token, marked reflexive.

Main statements

• ReflexivePronoun.bindingClassOf_toWord: the token of a reflexive classifies as a reflexive anaphor.

References

• [Cho81]

structure ReflexivePronounextends Pronoun : Type

A reflexive pronoun is a Pronoun of the reflexive kind.

• form : String
• person : Option Person
• number : Option Number
• case_ : Option Case
• gender : Option Gender
• script : Option String
• strength : Option Strength

@[instance_reducible]

instance instDecidableEqReflexivePronoun : DecidableEq ReflexivePronoun

Equations

• instDecidableEqReflexivePronoun = instDecidableEqReflexivePronoun.decEq

def instDecidableEqReflexivePronoun.decEq (x✝ x✝¹ : ReflexivePronoun) : Decidable (x✝ = x✝¹)

Equations

• instDecidableEqReflexivePronoun.decEq { toPronoun := a } { toPronoun := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def instReprReflexivePronoun.repr : ReflexivePronoun → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance instReprReflexivePronoun : Repr ReflexivePronoun

Equations

• instReprReflexivePronoun = { reprPrec := instReprReflexivePronoun.repr }

def ReflexivePronoun.paradigm : Finset ReflexivePronoun → Person.Category → Finset String

The paradigm of an inventory assigns each category the forms of the reflexives whose person and number realize it. A reflexive denotes what its antecedent does, so its cells are those of its agreement features.

Equations

• ReflexivePronoun.paradigm = Morphology.formsAt (fun (x : ReflexivePronoun) => x.categories) fun (x : ReflexivePronoun) => x.form

theorem ReflexivePronoun.mem_paradigm {I : Finset ReflexivePronoun} {c : Person.Category} {f : String} : f ∈ paradigm I c ↔ ∃ p ∈ I, c ∈ p.categories ∧ p.form = f

def ReflexivePronoun.toWord (p : ReflexivePronoun) : Morphology.Word

A reflexive's token is of UD pronoun type Prs and marked reflexive.

Equations

• p.toWord = p.toWord (some UD.PronType.Prs) true

@[simp]

theorem ReflexivePronoun.bindingClassOf_toWord (p : ReflexivePronoun) : Binding.bindingClassOf p.toWord = some Binding.BindingClass.reflexive

A reflexive pronoun is a reflexive anaphor.