Somali noun gender

This file defines the two Somali controller genders, the remote definite article and the verbal subject prefix each takes in each number, and the nouns the sources cite.

The remote definite article is polar. The masculine singular and the feminine plural take -kii, the feminine singular and the masculine plural -tii, so changing gender or number alone changes the article and changing both restores it. The subject prefix of the verbs that conjugate by prefix, such as imid 'came', is not polar. It is y- for the masculine singular and for both plurals and t- for the feminine singular alone. Masculine nouns whose plural is formed by reduplication, nin ~ niman 'man', keep the singular article in the plural.

Main definitions

• Somali.Gender.Value — the controller genders
• Somali.Gender.Value.article, Somali.Gender.Value.verbPrefix — the article and the verbal prefix by gender and number
• Somali.Gender.Noun, Somali.Gender.allNouns — the nouns, with their plurals

Main results

• Somali.Gender.polar_article — the article is polar
• Somali.Gender.faithful_article, Somali.Gender.faithful_verbPrefix — either exponent distinguishes the two genders

References

• J. Saeed, Somali (1999)
• G. G. Corbett, Gender (1991)
• G. G. Corbett, Morphology and agreement (1998)

Genders and their exponents

inductive Somali.Gender.Value : Type

The two controller genders.

• masc : Value
• fem : Value

@[instance_reducible]

instance Somali.Gender.instDecidableEqValue : DecidableEq Value

Equations

• Somali.Gender.instDecidableEqValue x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Somali.Gender.instReprValue.repr : Value → ℕ → Std.Format

Equations

• Somali.Gender.instReprValue.repr Somali.Gender.Value.masc prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Somali.Gender.Value.masc")).group prec✝
• Somali.Gender.instReprValue.repr Somali.Gender.Value.fem prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Somali.Gender.Value.fem")).group prec✝

@[instance_reducible]

instance Somali.Gender.instReprValue : Repr Value

Equations

• Somali.Gender.instReprValue = { reprPrec := Somali.Gender.instReprValue.repr }

@[instance_reducible]

instance Somali.Gender.instFintypeValue : Fintype Value

Equations

• Somali.Gender.instFintypeValue = { elems := { val := ↑Somali.Gender.Value.enumList, nodup := Somali.Gender.Value.enumList_nodup }, complete := Somali.Gender.instFintypeValue._proof_1 }

inductive Somali.Gender.Article : Type

The basic forms of the remote definite article. After a vowel other than i, -kii is -hii, and after any vowel -tii is -dii.

• kii : Article
• tii : Article

@[instance_reducible]

instance Somali.Gender.instDecidableEqArticle : DecidableEq Article

Equations

• Somali.Gender.instDecidableEqArticle x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Somali.Gender.instReprArticle : Repr Article

Equations

• Somali.Gender.instReprArticle = { reprPrec := Somali.Gender.instReprArticle.repr }

def Somali.Gender.instReprArticle.repr : Article → ℕ → Std.Format

Equations

• Somali.Gender.instReprArticle.repr Somali.Gender.Article.kii prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Somali.Gender.Article.kii")).group prec✝
• Somali.Gender.instReprArticle.repr Somali.Gender.Article.tii prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Somali.Gender.Article.tii")).group prec✝

@[instance_reducible]

instance Somali.Gender.instFintypeArticle : Fintype Article

Equations

• Somali.Gender.instFintypeArticle = { elems := { val := ↑Somali.Gender.Article.enumList, nodup := Somali.Gender.Article.enumList_nodup }, complete := Somali.Gender.instFintypeArticle._proof_1 }

def Somali.Gender.numberSystem : Number.System

Somali distinguishes the singular and the plural.

Equations

• Somali.Gender.numberSystem = Number.System.singularPlural

instance Somali.Gender.instNontrivialSubtypeNumberMemFinsetValuesNumberSystem : Nontrivial ↥numberSystem.values

def Somali.Gender.Value.article (g : Value) : ↥numberSystem.values → Article

The article a gender takes in each number.

Equations

• Somali.Gender.Value.masc.article = Somali.Gender.numberSystem.elim Somali.Gender.Article.kii Somali.Gender.Article.tii Somali.Gender.Value.article._proof_3
• Somali.Gender.Value.fem.article = Somali.Gender.numberSystem.elim Somali.Gender.Article.tii Somali.Gender.Article.kii Somali.Gender.Value.article._proof_3

inductive Somali.Gender.VerbPrefix : Type

The subject prefix of the verbs that conjugate by prefix.

• y : VerbPrefix
• t : VerbPrefix

@[instance_reducible]

instance Somali.Gender.instDecidableEqVerbPrefix : DecidableEq VerbPrefix

Equations

• Somali.Gender.instDecidableEqVerbPrefix x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Somali.Gender.instReprVerbPrefix.repr : VerbPrefix → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Somali.Gender.instReprVerbPrefix : Repr VerbPrefix

Equations

• Somali.Gender.instReprVerbPrefix = { reprPrec := Somali.Gender.instReprVerbPrefix.repr }

@[instance_reducible]

instance Somali.Gender.instFintypeVerbPrefix : Fintype VerbPrefix

Equations

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

def Somali.Gender.Value.verbPrefix (g : Value) : ↥numberSystem.values → VerbPrefix

The verbal prefix a gender takes in each number.

Equations

• Somali.Gender.Value.masc.verbPrefix = Somali.Gender.numberSystem.elim Somali.Gender.VerbPrefix.y Somali.Gender.VerbPrefix.y Somali.Gender.Value.article._proof_3
• Somali.Gender.Value.fem.verbPrefix = Somali.Gender.numberSystem.elim Somali.Gender.VerbPrefix.t Somali.Gender.VerbPrefix.y Somali.Gender.Value.article._proof_3

theorem Somali.Gender.polar_article : Morphology.Polar Value.article

The article is polar.

theorem Somali.Gender.faithful_article : Gender.Faithful Value.article

The article distinguishes the two genders.

theorem Somali.Gender.faithful_verbPrefix : Gender.Faithful Value.verbPrefix

The verbal prefix distinguishes the two genders.

Nouns

structure Somali.Gender.Nounextends GenderedNoun Somali.Gender.Value : Type

A Somali noun with its gender, its plural form and whether that plural is formed by reduplication.

• form : String
• gloss : String
• gender : Somali.Gender.Value
• referentGender : Option ReferentGender
• plural : String

  The plural form.

• reduplicatedPlural : Bool

  Whether the plural is formed by reduplication and so keeps the singular article.

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

Equations

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

@[instance_reducible]

instance Somali.Gender.instDecidableEqNoun : DecidableEq Noun

Equations

• Somali.Gender.instDecidableEqNoun = Somali.Gender.instDecidableEqNoun.decEq

@[instance_reducible]

instance Somali.Gender.instReprNoun : Repr Noun

Equations

• Somali.Gender.instReprNoun = { reprPrec := Somali.Gender.instReprNoun.repr }

def Somali.Gender.instReprNoun.repr : Noun → ℕ → Std.Format

Equations

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

def Somali.Gender.Noun.article (n : Noun) (num : ↥numberSystem.values) : Article

The article a noun takes in the singular and in the plural.

Equations

• n.article num = n.gender.article (if n.reduplicatedPlural = true then Somali.Gender.numberSystem.value Number.singular Somali.Gender.Noun.article._proof_1 else num)

def Somali.Gender.inan : Noun

The noun ìnan 'boy'.

Equations

• Somali.Gender.inan = { form := "ìnan", gloss := "boy", gender := Somali.Gender.Value.masc, referentGender := some ReferentGender.male, plural := "inammá", reduplicatedPlural := false }

def Somali.Gender.inan' : Noun

The noun inán 'girl'.

Equations

• Somali.Gender.inan' = { form := "inán", gloss := "girl", gender := Somali.Gender.Value.fem, referentGender := some ReferentGender.female, plural := "ináma", reduplicatedPlural := false }

def Somali.Gender.nin : Noun

The noun nin 'man', whose plural niman is reduplicated.

Equations

• Somali.Gender.nin = { form := "nin", gloss := "man", gender := Somali.Gender.Value.masc, referentGender := some ReferentGender.male, plural := "niman", reduplicatedPlural := true }

def Somali.Gender.allNouns : List Noun

The nouns the sources cite.

Equations

• Somali.Gender.allNouns = [Somali.Gender.inan, Somali.Gender.inan', Somali.Gender.nin]