Teop Noun Inventory @cite{adamson-2024}

Gender I and gender II nouns in Teop (Austronesian, Oceanic), drawn from @cite{adamson-2024} 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 Fragments.Teop.Gender : Type

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

• gI : Gender
• gII : Gender

instance Fragments.Teop.instDecidableEqGender : DecidableEq Gender

Equations

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

def Fragments.Teop.instBEqGender.beq : Gender → Gender → Bool

Equations

• Fragments.Teop.instBEqGender.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Fragments.Teop.instBEqGender : BEq Gender

Equations

• Fragments.Teop.instBEqGender = { beq := Fragments.Teop.instBEqGender.beq }

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

Equations

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

instance Fragments.Teop.instReprGender : Repr Gender

Equations

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

structure Fragments.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.

instance Fragments.Teop.instDecidableEqNoun : DecidableEq Noun

Equations

• Fragments.Teop.instDecidableEqNoun = Fragments.Teop.instDecidableEqNoun.decEq

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

Equations

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

instance Fragments.Teop.instBEqNoun : BEq Noun

Equations

• Fragments.Teop.instBEqNoun = { beq := Fragments.Teop.instBEqNoun.beq }

def Fragments.Teop.instBEqNoun.beq : Noun → Noun → Bool

Equations

• One or more equations did not get rendered due to their size.
• Fragments.Teop.instBEqNoun.beq x✝¹ x✝ = false

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

Equations

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

instance Fragments.Teop.instReprNoun : Repr Noun

Equations

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

def Fragments.Teop.moon : Noun

Equations

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

def Fragments.Teop.beikoo : Noun

Equations

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

def Fragments.Teop.keusu : Noun

Equations

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

def Fragments.Teop.naovana : Noun

Equations

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

def Fragments.Teop.overe_c : Noun

Equations

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

def Fragments.Teop.pauna : Noun

Equations

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

def Fragments.Teop.kepaa : Noun

Equations

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

def Fragments.Teop.anoo : Noun

Equations

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

def Fragments.Teop.tabaani : Noun

Equations

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

def Fragments.Teop.tahii : Noun

Equations

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

def Fragments.Teop.huan : Noun

Equations

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

def Fragments.Teop.uruuru : Noun

Equations

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

def Fragments.Teop.paka : Noun

Equations

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

def Fragments.Teop.pus : Noun

Equations

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

def Fragments.Teop.hinahoo : Noun

Equations

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

def Fragments.Teop.sinivi : Noun

Equations

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

def Fragments.Teop.overe_p : Noun

Equations

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

def Fragments.Teop.overe_bt : Noun

Equations

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

def Fragments.Teop.kurita : Noun

Equations

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

def Fragments.Teop.demdem : Noun

Equations

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

def Fragments.Teop.paku : Noun

Equations

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

def Fragments.Teop.suraa : Noun

Equations

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

def Fragments.Teop.giigii : Noun

Equations

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

def Fragments.Teop.koara : Noun

Equations

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

def Fragments.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

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

def Fragments.Teop.kuri : Noun

Equations

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

def Fragments.Teop.iru : Noun

Equations

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

def Fragments.Teop.vuha : Noun

Equations

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

def Fragments.Teop.ihu : Noun

Equations

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

def Fragments.Teop.revasin : Noun

Equations

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

def Fragments.Teop.hena : Noun

Equations

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

def Fragments.Teop.moo : Noun

Equations

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

def Fragments.Teop.iPossessedGender (n : Noun) : Gender

Body-part nouns when iPossessed switch to gender I.

Equations

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

structure Fragments.Teop.ArticleCtx : Type

Teop articles, conditioned by gender and number. Gender Ie (proprial e) is treated as gender I with a proprial feature, following @cite{adamson-2024} §3.1.

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

instance Fragments.Teop.instDecidableEqArticleCtx : DecidableEq ArticleCtx

Equations

• Fragments.Teop.instDecidableEqArticleCtx = Fragments.Teop.instDecidableEqArticleCtx.decEq

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

Equations

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

def Fragments.Teop.instBEqArticleCtx.beq : ArticleCtx → ArticleCtx → Bool

Equations

• Fragments.Teop.instBEqArticleCtx.beq { gender := a, plural := a_1, proprial := a_2 } { gender := b, plural := b_1, proprial := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• Fragments.Teop.instBEqArticleCtx.beq x✝¹ x✝ = false

instance Fragments.Teop.instBEqArticleCtx : BEq ArticleCtx

Equations

• Fragments.Teop.instBEqArticleCtx = { beq := Fragments.Teop.instBEqArticleCtx.beq }

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

Equations

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

instance Fragments.Teop.instReprArticleCtx : Repr ArticleCtx

Equations

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

def Fragments.Teop.articleForm : ArticleCtx → String

Equations

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

def Fragments.Teop.genderINouns : List Noun

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

Equations

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

def Fragments.Teop.genderIINouns : List Noun

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

Equations

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

def Fragments.Teop.bodyPartNouns : List Noun

Equations

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

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

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

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

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

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

theorem Fragments.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 Fragments.Teop.spleen_unpossessed_article : articleForm { gender := bina.gender, plural := false } = "o"

def Fragments.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

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

theorem Fragments.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 Fragments.Teop.gII_no_gender : Gender.gII.toCatHead.phi.gender = none

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

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

Body-part nouns when iPossessed switch to n with u[+ANIM] (@cite{adamson-2024} §3.1).

Equations

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

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

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