Teop Noun Inventory [Ada24]

Gender I and gender II nouns in Teop (Austronesian, Oceanic), drawn from [Ada24] Table 1 (sampled from Mosel & Spriggs 2000:336–40).

Teop has two genders distinguished by article form:

• Gender I (article a): animates — encoded via [±ANIM] on n
• Gender II (article o): inanimates — plain n

Body-part nouns appear in both genders depending on possession: iPossessed (with n_{body-part{D}}) → gender I; unpossessed or aPossessed (with n_{alienator}) → gender II.

inductive Teop.Gender : Type

Teop gender: two classes (Mosel & Spriggs 2000, Mosel 2014).

• gI : Gender
• gII : Gender

@[implicit_reducible]

instance Teop.instDecidableEqGender : DecidableEq Gender

Equations

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

@[implicit_reducible]

instance Teop.instReprGender : Repr Gender

Equations

• Teop.instReprGender = { reprPrec := Teop.instReprGender.repr }

def Teop.instReprGender.repr : Gender → ℕ → Std.Format

Equations

• Teop.instReprGender.repr Teop.Gender.gI prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Teop.Gender.gI")).group prec✝
• Teop.instReprGender.repr Teop.Gender.gII prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Teop.Gender.gII")).group prec✝

structure Teop.Noun : Type

A Teop noun with its gloss and gender assignment.

• form : String
• gloss : String
• gender : Gender
• isBodyPart : Bool

  Body-part nouns can be iPossessed, switching to gender I.

@[implicit_reducible]

instance Teop.instDecidableEqNoun : DecidableEq Noun

Equations

• Teop.instDecidableEqNoun = Teop.instDecidableEqNoun.decEq

def Teop.instDecidableEqNoun.decEq (x✝ x✝¹ : Noun) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Teop.instReprNoun : Repr Noun

Equations

• Teop.instReprNoun = { reprPrec := Teop.instReprNoun.repr }

def Teop.instReprNoun.repr : Noun → ℕ → Std.Format

Equations

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

def Teop.moon : Noun

Equations

• Teop.moon = { form := "moon", gloss := "woman", gender := Teop.Gender.gI }

def Teop.beikoo : Noun

Equations

• Teop.beikoo = { form := "beikoo", gloss := "child", gender := Teop.Gender.gI }

def Teop.keusu : Noun

Equations

• Teop.keusu = { form := "keusu", gloss := "rat", gender := Teop.Gender.gI }

def Teop.naovana : Noun

Equations

• Teop.naovana = { form := "naovana", gloss := "bird", gender := Teop.Gender.gI }

def Teop.overe_c : Noun

Equations

• Teop.overe_c = { form := "overe", gloss := "coconut", gender := Teop.Gender.gI }

def Teop.pauna : Noun

Equations

• Teop.pauna = { form := "pauna", gloss := "banana", gender := Teop.Gender.gI }

def Teop.kepaa : Noun

Equations

• Teop.kepaa = { form := "kepaa", gloss := "clay pot", gender := Teop.Gender.gI }

def Teop.anoo : Noun

Equations

• Teop.anoo = { form := "anoo", gloss := "peeler (pearl shell)", gender := Teop.Gender.gI }

def Teop.tabaani : Noun

Equations

• Teop.tabaani = { form := "taba'ani", gloss := "food", gender := Teop.Gender.gI }

def Teop.tahii : Noun

Equations

• Teop.tahii = { form := "tahii", gloss := "sea", gender := Teop.Gender.gI }

def Teop.huan : Noun

Equations

• Teop.huan = { form := "huan", gloss := "rain", gender := Teop.Gender.gI }

def Teop.uruuru : Noun

Equations

• Teop.uruuru = { form := "uruuru", gloss := "love", gender := Teop.Gender.gI }

def Teop.paka : Noun

Equations

• Teop.paka = { form := "paka", gloss := "leaf", gender := Teop.Gender.gII }

def Teop.pus : Noun

Equations

• Teop.pus = { form := "pus", gloss := "stump", gender := Teop.Gender.gII }

def Teop.hinahoo : Noun

Equations

• Teop.hinahoo = { form := "hinahoo", gloss := "taro planting stick", gender := Teop.Gender.gII }

def Teop.sinivi : Noun

Equations

• Teop.sinivi = { form := "sinivi", gloss := "canoe", gender := Teop.Gender.gII }

def Teop.overe_p : Noun

Equations

• Teop.overe_p = { form := "overe", gloss := "coconut palm", gender := Teop.Gender.gII }

def Teop.overe_bt : Noun

Equations

• Teop.overe_bt = { form := "overe", gloss := "banana tree", gender := Teop.Gender.gII }

def Teop.kurita : Noun

Equations

• Teop.kurita = { form := "kurita", gloss := "octopus", gender := Teop.Gender.gII }

def Teop.demdem : Noun

Equations

• Teop.demdem = { form := "demdem", gloss := "snail", gender := Teop.Gender.gII }

def Teop.paku : Noun

Equations

• Teop.paku = { form := "paku", gloss := "feast", gender := Teop.Gender.gII }

def Teop.suraa : Noun

Equations

• Teop.suraa = { form := "suraa", gloss := "fire", gender := Teop.Gender.gII }

def Teop.giigii : Noun

Equations

• Teop.giigii = { form := "giigii", gloss := "shooting star", gender := Teop.Gender.gII }

def Teop.koara : Noun

Equations

• Teop.koara = { form := "koara", gloss := "language", gender := Teop.Gender.gII }

def Teop.bina : Noun

Body-part nouns: gender I when iPossessed, gender II when free. The gender field records the UNPOSSESSED (default) gender II; iPossession switches them to gender I via n_{body-part{D}}.

Equations

• Teop.bina = { form := "bina", gloss := "spleen", gender := Teop.Gender.gII, isBodyPart := true }

def Teop.kuri : Noun

Equations

• Teop.kuri = { form := "kuri", gloss := "hand", gender := Teop.Gender.gII, isBodyPart := true }

def Teop.iru : Noun

Equations

• Teop.iru = { form := "iru", gloss := "back of head", gender := Teop.Gender.gII, isBodyPart := true }

def Teop.vuha : Noun

Equations

• Teop.vuha = { form := "vuha", gloss := "heart", gender := Teop.Gender.gII, isBodyPart := true }

def Teop.ihu : Noun

Equations

• Teop.ihu = { form := "ihu", gloss := "nose", gender := Teop.Gender.gII, isBodyPart := true }

def Teop.revasin : Noun

Equations

• Teop.revasin = { form := "revasin", gloss := "blood", gender := Teop.Gender.gII, isBodyPart := true }

def Teop.hena : Noun

Equations

• Teop.hena = { form := "hena", gloss := "name", gender := Teop.Gender.gII, isBodyPart := true }

def Teop.moo : Noun

Equations

• Teop.moo = { form := "moo", gloss := "leg", gender := Teop.Gender.gII, isBodyPart := true }

def Teop.iPossessedGender (n : Noun) : Gender

Body-part nouns when iPossessed switch to gender I.

Equations

• Teop.iPossessedGender n = if n.isBodyPart = true then Teop.Gender.gI else n.gender

structure Teop.ArticleCtx : Type

Teop articles, conditioned by gender and number. Gender Ie (proprial e) is treated as gender I with a proprial feature, following [Ada24] §3.1.

• gender : Gender
• plural : Bool
• proprial : Bool

def Teop.instDecidableEqArticleCtx.decEq (x✝ x✝¹ : ArticleCtx) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Teop.instDecidableEqArticleCtx : DecidableEq ArticleCtx

Equations

• Teop.instDecidableEqArticleCtx = Teop.instDecidableEqArticleCtx.decEq

@[implicit_reducible]

instance Teop.instReprArticleCtx : Repr ArticleCtx

Equations

• Teop.instReprArticleCtx = { reprPrec := Teop.instReprArticleCtx.repr }

def Teop.instReprArticleCtx.repr : ArticleCtx → ℕ → Std.Format

Equations

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

def Teop.articleForm : ArticleCtx → String

Equations

• Teop.articleForm { gender := Teop.Gender.gI, plural := plural, proprial := true } = "e"
• Teop.articleForm { gender := Teop.Gender.gI, plural := false } = "a"
• Teop.articleForm { gender := Teop.Gender.gI, plural := true } = "ra"
• Teop.articleForm { gender := Teop.Gender.gII, plural := false, proprial := proprial } = "o"
• Teop.articleForm { gender := Teop.Gender.gII, plural := true, proprial := proprial } = "ro"

def Teop.genderINouns : List Noun

Gender I nouns are animate (Mosel & Spriggs 2000:337–38).

Equations

• Teop.genderINouns = [Teop.moon, Teop.beikoo, Teop.keusu, Teop.naovana, Teop.overe_c, Teop.pauna, Teop.kepaa, Teop.anoo, Teop.tabaani, Teop.tahii, Teop.huan, Teop.uruuru]

def Teop.genderIINouns : List Noun

Gender II nouns are inanimate (Mosel & Spriggs 2000:338–40).

Equations

• Teop.genderIINouns = [Teop.paka, Teop.pus, Teop.hinahoo, Teop.sinivi, Teop.overe_p, Teop.overe_bt, Teop.kurita, Teop.demdem, Teop.paku, Teop.suraa, Teop.giigii, Teop.koara]

def Teop.bodyPartNouns : List Noun

Equations

• Teop.bodyPartNouns = [Teop.bina, Teop.kuri, Teop.iru, Teop.vuha, Teop.ihu, Teop.revasin, Teop.hena, Teop.moo]

theorem Teop.genderI_all_gI : (genderINouns.all fun (x : Noun) => x.gender == Gender.gI) = true

theorem Teop.genderII_all_gII : (genderIINouns.all fun (x : Noun) => x.gender == Gender.gII) = true

theorem Teop.bodyParts_all_marked : (bodyPartNouns.all fun (x : Noun) => x.isBodyPart) = true

theorem Teop.bodyParts_default_gII : (bodyPartNouns.all fun (x : Noun) => x.gender == Gender.gII) = true

theorem Teop.bodyParts_iPossessed_gI : (bodyPartNouns.all fun (x : Noun) => iPossessedGender x == Gender.gI) = true

theorem Teop.spleen_ipossessed_article : articleForm { gender := iPossessedGender bina, plural := false } = "a"

The article paradigm: iPossessed body part gets a, unpossessed body part gets o.

theorem Teop.spleen_unpossessed_article : articleForm { gender := bina.gender, plural := false } = "o"

def Teop.Gender.toGender : Gender → _root_.Gender

Map Teop gender classes to the shared surface-level gender type. Gender I (animates) → animate; Gender II (inanimates) → inanimate.

Equations

• Teop.Gender.gI.toGender = Gender.animate
• Teop.Gender.gII.toGender = Gender.inanimate

def Teop.Gender.toCatHead : Gender → Morphology.DM.CatHead

Map Teop gender classes to their DM categorizing heads. Gender I (animates) ↔ n i[+ANIM]; Gender II (inanimates) ↔ plain n.

Equations

• Teop.Gender.gI.toCatHead = Morphology.DM.CatHead.n_iAnim
• Teop.Gender.gII.toCatHead = Morphology.DM.CatHead.n_plain

theorem Teop.gI_natural_gender : Gender.gI.toCatHead.phi.gender = some { interp := Morphology.DM.Interpretability.i, val := { dim := Morphology.DM.GenderDimension.anim, pol := Morphology.DM.Polarity.pos } }

Gender I maps to a natural (interpretable) gender feature.

theorem Teop.gII_no_gender : Gender.gII.toCatHead.phi.gender = none

Gender II maps to plain n (no gender feature).

def Teop.iPossessedCatHead (n : Noun) : Morphology.DM.CatHead

Body-part nouns when iPossessed switch to n with u[+ANIM] ([Ada24] §3.1).

Equations

• Teop.iPossessedCatHead n = if n.isBodyPart = true then Morphology.DM.CatHead.n_uAnim else n.gender.toCatHead

theorem Teop.spleen_ipossessed_cathead : iPossessedCatHead bina = Morphology.DM.CatHead.n_uAnim

theorem Teop.spleen_free_cathead : bina.gender.toCatHead = Morphology.DM.CatHead.n_plain