Gender on the nominal categorizer

This file defines the gender features of the nominal categorizer n in Distributed Morphology. A gender feature is a binary dimension such as [±FEM] with a sign, and it is interpretable for natural gender and uninterpretable for arbitrary gender. A categorizing head may also bear the selectional feature {D}, which licenses an inalienable possessor.

Agreement in gender is a probe relativized to gender, searching the heads of a nominal from the top; when it finds none, Agree fails and the default gender is spelled out. When several n's are stacked, Kramer's Highest Gender Hypothesis makes the gender of the highest n the agreeing gender. Kramer derives it from cyclicity: each n is a cyclic head that sends the nPs below it to spell-out, so the probe searches the last cycle of the word alone. A plain highest n then leaves the default gender, where a probe searching every n would find the gender of a lower one, and a diminutive that is not an n, bearing no gender, leaves the gender of the n below it.

Main definitions

• GenderValue: a binary gender dimension with a sign.
• GenderFeature: a gender value with its interpretability.
• Categorizer.Head: a categorizer with its gender feature and {D}.
• agreeingGender: the gender a gender probe agrees in, or the default on failed Agree.

Main results

• agreeingGender_lastCycle: the Highest Gender Hypothesis, the agreeing gender of a word being that of its highest cyclic head.
• agreeingGender_lastCycle_plain: a plain highest n gives the default, where a search of every n would not.

References

• [Kra15]
• [Ada24]
• [Myl16]

Gender features

inductive DistributedMorphology.GenderDimension : Type

A binary gender dimension.

• fem : GenderDimension

  [±FEM], as in Amharic, Spanish and Maa.

• masc : GenderDimension

  [±MASC], as in Jarawara.

• anim : GenderDimension

  [±ANIM], as in Lealao Chinantec, Algonquian and Teop.

@[instance_reducible]

instance DistributedMorphology.instDecidableEqGenderDimension : DecidableEq GenderDimension

Equations

• DistributedMorphology.instDecidableEqGenderDimension x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def DistributedMorphology.instReprGenderDimension.repr : GenderDimension → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance DistributedMorphology.instReprGenderDimension : Repr GenderDimension

Equations

• DistributedMorphology.instReprGenderDimension = { reprPrec := DistributedMorphology.instReprGenderDimension.repr }

@[instance_reducible]

instance DistributedMorphology.instFintypeGenderDimension : Fintype GenderDimension

Equations

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

inductive DistributedMorphology.GenderValue.Pole : Type

The sign of a binary feature.

• pos : Pole
• neg : Pole

@[instance_reducible]

instance DistributedMorphology.GenderValue.instDecidableEqPole : DecidableEq Pole

Equations

• DistributedMorphology.GenderValue.instDecidableEqPole x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def DistributedMorphology.GenderValue.instReprPole.repr : Pole → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance DistributedMorphology.GenderValue.instReprPole : Repr Pole

Equations

• DistributedMorphology.GenderValue.instReprPole = { reprPrec := DistributedMorphology.GenderValue.instReprPole.repr }

@[instance_reducible]

instance DistributedMorphology.GenderValue.instFintypePole : Fintype Pole

Equations

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

structure DistributedMorphology.GenderValue : Type

A valued gender feature is a dimension with a sign, as in [+FEM], [−FEM] and [+ANIM].

• dim : GenderDimension

  The dimension.

• pole : Pole

  The sign.

@[instance_reducible]

instance DistributedMorphology.instDecidableEqGenderValue : DecidableEq GenderValue

Equations

• DistributedMorphology.instDecidableEqGenderValue = DistributedMorphology.instDecidableEqGenderValue.decEq

def DistributedMorphology.instDecidableEqGenderValue.decEq (x✝ x✝¹ : GenderValue) : Decidable (x✝ = x✝¹)

Equations

• DistributedMorphology.instDecidableEqGenderValue.decEq { dim := a, pole := a_1 } { dim := b, pole := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance DistributedMorphology.instReprGenderValue : Repr GenderValue

Equations

• DistributedMorphology.instReprGenderValue = { reprPrec := DistributedMorphology.instReprGenderValue.repr }

def DistributedMorphology.instReprGenderValue.repr : GenderValue → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance DistributedMorphology.instFintypeGenderValue : Fintype GenderValue

Equations

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

structure DistributedMorphology.GenderFeature : Type

A gender value together with its interpretability.

• interp : Minimalist.Interpretability

  Whether the feature is legible at LF.

• val : GenderValue

  The value.

def DistributedMorphology.instDecidableEqGenderFeature.decEq (x✝ x✝¹ : GenderFeature) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance DistributedMorphology.instDecidableEqGenderFeature : DecidableEq GenderFeature

Equations

• DistributedMorphology.instDecidableEqGenderFeature = DistributedMorphology.instDecidableEqGenderFeature.decEq

@[instance_reducible]

instance DistributedMorphology.instReprGenderFeature : Repr GenderFeature

Equations

• DistributedMorphology.instReprGenderFeature = { reprPrec := DistributedMorphology.instReprGenderFeature.repr }

def DistributedMorphology.instReprGenderFeature.repr : GenderFeature → ℕ → Std.Format

Equations

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

Categorizing heads

structure DistributedMorphology.Categorizer.Head : Type

A categorizing head with its gender feature and the selectional feature {D}, a head of a ComplexHead.

• categorizer : Categorizer

  The categorizer n, v or a.

• gender : Option GenderFeature

  The gender feature, if any.

• selectsD : Bool

  The selectional feature {D}.

def DistributedMorphology.Categorizer.instDecidableEqHead.decEq (x✝ x✝¹ : Head) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance DistributedMorphology.Categorizer.instDecidableEqHead : DecidableEq Head

Equations

• DistributedMorphology.Categorizer.instDecidableEqHead = DistributedMorphology.Categorizer.instDecidableEqHead.decEq

@[instance_reducible]

instance DistributedMorphology.Categorizer.instReprHead : Repr Head

Equations

• DistributedMorphology.Categorizer.instReprHead = { reprPrec := DistributedMorphology.Categorizer.instReprHead.repr }

def DistributedMorphology.Categorizer.instReprHead.repr : Head → ℕ → Std.Format

Equations

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

def DistributedMorphology.Categorizer.Head.gendered (interp : Minimalist.Interpretability) (v : GenderValue) : Head

The n bearing the gender feature of interpretability interp and value v.

Equations

• DistributedMorphology.Categorizer.Head.gendered interp v = { categorizer := DistributedMorphology.Categorizer.n, gender := some { interp := interp, val := v } }

def DistributedMorphology.Categorizer.Head.n_plain : Head

The n with no gender feature.

Equations

• DistributedMorphology.Categorizer.Head.n_plain = { categorizer := DistributedMorphology.Categorizer.n }

def DistributedMorphology.Categorizer.Head.n_iFem : Head

The n bearing interpretable [+FEM], the natural feminine.

Equations

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

def DistributedMorphology.Categorizer.Head.n_iMasc : Head

The n bearing interpretable [−FEM], the natural masculine.

Equations

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

def DistributedMorphology.Categorizer.Head.n_uFem : Head

The n bearing uninterpretable [+FEM], the arbitrary feminine.

Equations

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

def DistributedMorphology.Categorizer.Head.n_uAnim : Head

The n bearing uninterpretable [+ANIM], the nominalizer of Teop body-part roots.

Equations

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

Agreement in gender

def DistributedMorphology.genderProbe {H : Type u_2} {G : Type u_3} (gender : H → Option G) : Minimalist.Probe H

The probe for gender, relativized to the heads that bear one.

Equations

• DistributedMorphology.genderProbe gender = Minimalist.Probe.relativized fun (h : H) => (gender h).isSome

def DistributedMorphology.agreeingGender {H : Type u_2} {G : Type u_3} (gender : H → Option G) (default : G) (goals : List H) : G

The gender a gender probe agrees in when it searches goals, nearest first, or default when Agree fails.

Equations

• DistributedMorphology.agreeingGender gender default goals = (((DistributedMorphology.genderProbe gender).search goals).bind gender).getD default

@[simp]

theorem DistributedMorphology.agreeingGender_nil {H : Type u_2} {G : Type u_3} {gender : H → Option G} {default : G} : agreeingGender gender default [] = default

theorem DistributedMorphology.agreeingGender_cons_of_eq_some {H : Type u_2} {G : Type u_3} {gender : H → Option G} {default : G} {h : H} {hs : List H} {g : G} (hg : gender h = some g) : agreeingGender gender default (h :: hs) = g

theorem DistributedMorphology.agreeingGender_cons_of_eq_none {H : Type u_2} {G : Type u_3} {gender : H → Option G} {default : G} {h : H} {hs : List H} (hh : gender h = none) : agreeingGender gender default (h :: hs) = agreeingGender gender default hs

theorem DistributedMorphology.agreeingGender_singleton {H : Type u_2} {G : Type u_3} {gender : H → Option G} {default : G} {h : H} : agreeingGender gender default [h] = (gender h).getD default

theorem DistributedMorphology.agreeingGender_append_of_forall_eq_none {H : Type u_2} {G : Type u_3} {gender : H → Option G} {default : G} {l l' : List H} (hl : ∀ a ∈ l, gender a = none) : agreeingGender gender default (l ++ l') = agreeingGender gender default l'

Heads bearing no gender are invisible to the probe.

theorem DistributedMorphology.agreeingGender_lastCycle {R : Type u_1} {H : Type u_2} {G : Type u_3} {gender : H → Option G} {default : G} {h : H} {hs : List H} {cyclic : H → Prop} [DecidablePred cyclic] {r : R} {above : List H} (hc : cyclic h) (ha : ∀ a ∈ above, ¬cyclic a ∧ gender a = none) : agreeingGender gender default ({ root := r, heads := hs ++ h :: above }.lastCycle cyclic) = (gender h).getD default

The Highest Gender Hypothesis. A probe above a word whose highest cyclic head is h, with only noncyclic heads bearing no gender over it, agrees in the gender h gives alone.

theorem DistributedMorphology.agreeingGender_lastCycle_plain {R : Type u_1} {H : Type u_2} {G : Type u_3} {gender : H → Option G} {default : G} {h h' : H} {hs : List H} {g : G} {cyclic : H → Prop} [DecidablePred cyclic] {r : R} (hc : cyclic h) (hh : gender h = none) (hg : gender h' = some g) : agreeingGender gender default ({ root := r, heads := hs ++ [h', h] }.lastCycle cyclic) = default ∧ agreeingGender gender default (hs ++ [h', h]).reverse = g

A plain highest n over an n of gender g gives the default, where a probe searching every head would find g.