Gender assignment is local

[Ada24] proposes the Gender Locality Hypothesis: the gender feature on a nominalizer n is valued within nP. An inalienable possessor sits in Spec,nP and can therefore determine a noun's gender; an alienable possessor sits in Spec,PossP and cannot. The hypothesis itself is DistributedMorphology.genderLocalityHypothesis. This file derives the paper's case studies from it and from the shared Vocabulary Insertion and Impoverishment engines.

Main definitions

• Teop.relationalN, Teop.alienatorN: the two nominalizers available to a body-part or kinship root — one licensing an inalienable possessor, the other stacked above it to close the possessor slot.
• Teop.outerGender: the gender of a nominal, read off its highest n.
• Teop.articles: the article vocabulary, the paper's (32).
• Teop.ipossessedDenot, Teop.freeDenot: the two nominalizers' denotations, Barker's relationalizer and its possessor-closing inverse.
• Jarawara.impoverish, Jarawara.decl, Jarawara.mano: gender impoverishment feeding the declarative agreement marker and the possessed noun mano ~ mani.
• possesseeGender: the two ways a possessor can fix a possessee's gender.

Main results

• Teop.article_eq_articleForm: the Subset Principle over (32) yields the Fragment's article paradigm, including the cross-identity of singular gender I with plural gender II.
• Teop.switch: one body-part root is gender I under the possessor-licensing nominalizer and gender II under the alienator; Teop.freeDenot_iff is the semantic side of the same switch.
• Jarawara.mano_eq_manoForm: impoverishment followed by insertion derives the possessed-noun paradigm of Table 6.
• Italian.aPlural_changes_gender: number on n changes gender; number on Num does not.

Implementation notes

A nominal is a stack of heads, innermost first, and its gender is that of the highest n — the paper's rule for stacked nominalizers. Jarawara's features [masc], [pl], [participant] are privative, as in the paper; the secondary feature [marked] of (A7) is rendered as one Vocabulary Item per marked feature.

The Gender Locality Hypothesis

theorem Adamson2024.possession_asymmetry : DistributedMorphology.PossessionType.inalienable.canAffectGender = true ∧ DistributedMorphology.PossessionType.alienable.canAffectGender = false

The asymmetry of (16): an inalienable possessor can bear on gender, an alienable one cannot.

def Adamson2024.possesseeGender {G : Type u_1} : DistributedMorphology.PossessionGenderMechanism → G → G → G

What fixes a possessee's gender under each mechanism of §2.3: its own nominalizer (possessee gender, Teop and Jarawara) or its iPossessor's gender (inherited gender, Yanyuwa and Coastal Marind, the probe of (90)).

Equations

• Adamson2024.possesseeGender DistributedMorphology.PossessionGenderMechanism.possesseeGender x✝¹ x✝ = x✝¹
• Adamson2024.possesseeGender DistributedMorphology.PossessionGenderMechanism.inheritedGender x✝¹ x✝ = x✝

theorem Adamson2024.inheritedGender_eq_possessor {G : Type u_1} (own possessor : G) : possesseeGender DistributedMorphology.PossessionGenderMechanism.inheritedGender own possessor = possessor

Under inherited gender the possessee matches its possessor (fn. 8).

Teop: possessee gender (§3.1)

def Adamson2024.Teop.relationalN (selectsD : Bool) : DistributedMorphology.Categorizer.Head

The nominalizer of a body-part or kinship root: it introduces the relation and bears u[animate], with or without the selectional feature {D} that licenses an iPossessor ((36), (43)).

Equations

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

def Adamson2024.Teop.alienatorN : DistributedMorphology.Categorizer.Head

The alienator, a further n of gender II that closes the possessor slot ((43)).

Equations

• Adamson2024.Teop.alienatorN = DistributedMorphology.Categorizer.Head.n_plain

def Adamson2024.Teop.Animate (h : DistributedMorphology.Categorizer.Head) : Prop

A head bears the gender I feature [animate] ((24)).

Equations

• Adamson2024.Teop.Animate h = (Option.map (fun (x : DistributedMorphology.GenderFeature) => x.val.dim) h.phi.gender = some Gender.Dimension.anim)

@[instance_reducible]

instance Adamson2024.Teop.instDecidablePredHeadAnimate : DecidablePred Animate

Equations

• Adamson2024.Teop.instDecidablePredHeadAnimate h = Adamson2024.Teop.instDecidablePredHeadAnimate._aux_1 h

def Adamson2024.Teop.outerGender (stack : List DistributedMorphology.Categorizer.Head) : Teop.Gender

The gender of a nominal, read off its highest n: gender II is the absence of [animate].

Equations

• Adamson2024.Teop.outerGender stack = match stack.getLast? with | some h => if Adamson2024.Teop.Animate h then Teop.Gender.gI else Teop.Gender.gII | none => Teop.Gender.gII

def Adamson2024.Teop.ipossessed : List DistributedMorphology.Categorizer.Head

The iPossessed body-part noun: the root under the {D} nominalizer ((36)).

Equations

• Adamson2024.Teop.ipossessed = [Adamson2024.Teop.relationalN true]

def Adamson2024.Teop.free : List DistributedMorphology.Categorizer.Head

The free (or aPossessed, or compounded) body-part noun: the {D}-less nominalizer under the alienator ((43), (44)–(47)).

Equations

• Adamson2024.Teop.free = [Adamson2024.Teop.relationalN false, Adamson2024.Teop.alienatorN]

theorem Adamson2024.Teop.switch : outerGender ipossessed = Teop.Gender.gI ∧ outerGender free = Teop.Gender.gII

The gender switch of (39)–(40): a bina-naa 'my spleen' is gender I, o bina 'the spleen' gender II.

inductive Adamson2024.Teop.ArticleFeature : Type

The article vocabulary (32), features percolated to D by concord: [animate] is gender I, [proper] the proprial class.

• animate : ArticleFeature
• pl : ArticleFeature
• proper : ArticleFeature

@[instance_reducible]

instance Adamson2024.Teop.instDecidableEqArticleFeature : DecidableEq ArticleFeature

Equations

• Adamson2024.Teop.instDecidableEqArticleFeature x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Adamson2024.Teop.instReprArticleFeature : Repr ArticleFeature

Equations

• Adamson2024.Teop.instReprArticleFeature = { reprPrec := Adamson2024.Teop.instReprArticleFeature.repr }

def Adamson2024.Teop.instReprArticleFeature.repr : ArticleFeature → ℕ → Std.Format

Equations

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

def Adamson2024.Teop.articles : List (DistributedMorphology.VocabularyItem ArticleFeature String)

The items of (32), in the paper's order.

Equations

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

def Adamson2024.Teop.articleFeatures (c : Teop.ArticleCtx) : List ArticleFeature

The article's bundle for a Fragment ArticleCtx.

Equations

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

def Adamson2024.Teop.article (c : Teop.ArticleCtx) : Option String

The article the Subset Principle inserts.

Equations

• Adamson2024.Teop.article c = DistributedMorphology.subsetPrinciple Adamson2024.Teop.articles (DistributedMorphology.Neighborhood.ofBundle (Adamson2024.Teop.articleFeatures c))

theorem Adamson2024.Teop.article_eq_articleForm (c : Teop.ArticleCtx) : article c = some (Teop.articleForm c)

(32) derives the Fragment's paradigm, including the cross-identities of (25)–(26) and the neutralization of the proprial article in the plural (29).

theorem Adamson2024.Teop.cross_identity : article { gender := Teop.Gender.gI, plural := false } = article { gender := Teop.Gender.gII, plural := true } ∧ article { gender := Teop.Gender.gI, plural := true } = article { gender := Teop.Gender.gII, plural := false }

The cross-identity: i.sg and ii.pl share a, i.pl and ii.sg share o.

theorem Adamson2024.Teop.bodyPart_article : article { gender := outerGender ipossessed, plural := false } = some "a" ∧ article { gender := outerGender free, plural := false } = some "o"

The body-part noun's article follows its nominalizer: a iPossessed, o free ((39)).

theorem Adamson2024.Teop.possessor_gender_immaterial (possessor : Teop.Gender) : possesseeGender DistributedMorphology.PossessionGenderMechanism.possesseeGender (outerGender ipossessed) possessor = Teop.Gender.gI

The iPossessor's own gender is immaterial ((48)–(49)): possessee gender reads the nominalizer, not the possessor.

theorem Adamson2024.Teop.kinship : article { gender := outerGender ipossessed, plural := false, proprial := true } = some "e" ∧ article { gender := outerGender free, plural := false } = some "o"

Kinship roots take the proprial article when iPossessed ((41), (50)) and switch to gender II under the alienator -na ((51)).

The denotations of (36) and (43)

def Adamson2024.Teop.ipossessedDenot {E : Type u_1} {S : Type u_2} (isSpleen : E → S → Prop) (bodyPartOf : E → E → S → Prop) : E → E → S → Prop

The iPossessed body-part noun ((36)): the root relationalized by the body-part-of relation — Barker's π, possessor first — awaiting its possessor.

Equations

• Adamson2024.Teop.ipossessedDenot isSpleen bodyPartOf = ArgumentStructure.Relational.π isSpleen bodyPartOf

def Adamson2024.Teop.freeDenot {E : Type u_1} {S : Type u_2} (isSpleen : E → S → Prop) (bodyPartOf : E → E → S → Prop) : E → S → Prop

The free body-part noun ((43)): the alienator closes the possessor slot.

Equations

• Adamson2024.Teop.freeDenot isSpleen bodyPartOf = ArgumentStructure.Relational.ExPossessor (ArgumentStructure.Relational.π isSpleen bodyPartOf)

theorem Adamson2024.Teop.freeDenot_iff {E : Type u_1} {S : Type u_2} (isSpleen : E → S → Prop) (bodyPartOf : E → E → S → Prop) (y : E) (s : S) : freeDenot isSpleen bodyPartOf y s ↔ isSpleen y s ∧ ∃ (x : E), bodyPartOf x y s

One root, two types: the possessor slot is open under the {D} nominalizer and existentially closed under the alienator.

Jarawara: possessee gender and agreement (§3.2)

inductive Adamson2024.Jarawara.Phi : Type

The privative φ-features of §3.2: [masc] ((58)), [pl], and [participant] for first and second person.

• masc : Phi
• pl : Phi
• participant : Phi

@[instance_reducible]

instance Adamson2024.Jarawara.instDecidableEqPhi : DecidableEq Phi

Equations

• Adamson2024.Jarawara.instDecidableEqPhi x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Adamson2024.Jarawara.instReprPhi : Repr Phi

Equations

• Adamson2024.Jarawara.instReprPhi = { reprPrec := Adamson2024.Jarawara.instReprPhi.repr }

def Adamson2024.Jarawara.instReprPhi.repr : Phi → ℕ → Std.Format

Equations

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

def Adamson2024.Jarawara.possessorPhi (p : Jarawara.Possessor) : List Phi

The features a possessor contributes to agreement.

Equations

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

def Adamson2024.Jarawara.impoverishment : List (DistributedMorphology.ImpoverishmentRule (List Phi) Phi)

Gender impoverishment (63): [masc] is deleted next to [pl] and next to [participant], two paradigmatic rules on the shared engine.

Equations

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

def Adamson2024.Jarawara.impoverish (φ : List Phi) : List Phi

The φ-bundle after (63).

Equations

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

def Adamson2024.Jarawara.declarative : List (DistributedMorphology.VocabularyItem Phi String)

The declarative marker's items (59): decl[masc] ↔ ka, decl ↔ ke.

Equations

• Adamson2024.Jarawara.declarative = [DistributedMorphology.VocabularyItem.ofFeatures [Adamson2024.Jarawara.Phi.masc] "ka", DistributedMorphology.VocabularyItem.ofFeatures [] "ke"]

def Adamson2024.Jarawara.decl (φ : List Phi) : Option String

The declarative marker agreeing with a nominal of features φ.

Equations

• Adamson2024.Jarawara.decl φ = DistributedMorphology.subsetPrinciple Adamson2024.Jarawara.declarative (DistributedMorphology.Neighborhood.ofBundle (Adamson2024.Jarawara.impoverish φ))

theorem Adamson2024.Jarawara.decl_masc_only : decl [Phi.masc] = some "ka" ∧ decl [] = some "ke" ∧ decl [Phi.participant] = some "ke" ∧ decl [Phi.masc, Phi.pl] = some "ke"

Masculine singular takes ka, everything else ke ((54), (60)–(62)): impoverishment bleeds the specific exponent.

def Adamson2024.Jarawara.manV : List (DistributedMorphology.VocabularyItem Phi String)

The possessed noun mano 'arm' (A7): mano for a marked feature — [participant] or a surviving [masc] — and mani elsewhere.

Equations

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

def Adamson2024.Jarawara.mano (p : Jarawara.Possessor) : Option String

The form of mano agreeing with possessor p.

Equations

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

def Adamson2024.Jarawara.tableSix : List Jarawara.Possessor

The cells of Table 6.

Equations

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

theorem Adamson2024.Jarawara.mano_eq_manoForm (p : Jarawara.Possessor) : p ∈ tableSix → mano p = some (match Jarawara.manoForm p with | Jarawara.PossessedForm.mascForm => "mano" | Jarawara.PossessedForm.femForm => "mani")

Impoverishment then insertion derives the Fragment's paradigm of Table 6: the 3.m.pl mani is the one cell where (63) does the work.

Number on n (§5.1)

theorem Adamson2024.Italian.aPlural_changes_gender : (∀ n ∈ Italian.NumberGender.aPluralNouns, n.pluralClass.canAffectGender = true ∧ n.genderChanges = true) ∧ ∀ n ∈ Italian.NumberGender.regularNouns, n.pluralClass.canAffectGender = false ∧ n.genderChanges = false

The -a plurals of (99) carry number on n, within the GLH's reach, and change gender; regular plurals carry number on Num and do not.