Mwaghavul Phonological Fragment

[AF26] [Fwa18]

Mwaghavul (ISO 639-3: sur, Glottocode: mwag1236) is an A3 West Chadic (Afro-Asiatic) language spoken by more than 700,000 people in Plateau State, Nigeria ([CB92]).

Tone system

Mwaghavul contrasts three level tones — high (H), mid (M), and low (L) — plus an LH rising contour. The tone-bearing unit (TBU) is the syllable. All tonal co-occurrences on bisyllabic roots are attested except M-LH ([AF26] Table 3).

Ideophones

Mwaghavul has a rich inventory of ideophones — "an open class of marked words that depict sensory imagery" ([Din19]:16). Ideophones share the same grammatical classes as nonideophonic words (nouns, verbs, adjectives, adverbs) and occur in comparable morphosyntactic environments.

Verbalisation

All tonally derived verbs in Mwaghavul have ideophonic bases. The verb formation is morphophonologically marked through one of two lexically determined tonal alternations triggered by segmentally null verbalisers:

1. M verbaliser (VBZ₁): overwrites every TBU with M
2. M-H verbaliser (VBZ₂): overwrites nonfinal TBUs with M, final with H

The M-H melody is attested only in derived verbs — no underived verb has this pattern. Data from [AF26] and [Fwa18].

def Mwaghavul.wordProsodicType : Tone.WordProsodicType

Mwaghavul is a three-level tone language with syllable TBUs.

Equations

• Mwaghavul.wordProsodicType = Tone.WordProsodicType.toneBased

def Mwaghavul.tbuKind : Tone.TBUKind

Equations

• Mwaghavul.tbuKind = Tone.TBUKind.syllable

inductive Mwaghavul.VerbalizerChoice : Type

The two lexically specific suppletive allomorphs of the verbaliser morpheme ([AF26] (17)).

• m : VerbalizerChoice
• mh : VerbalizerChoice

@[implicit_reducible]

instance Mwaghavul.instDecidableEqVerbalizerChoice : DecidableEq VerbalizerChoice

Equations

• Mwaghavul.instDecidableEqVerbalizerChoice x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Mwaghavul.instReprVerbalizerChoice.repr : VerbalizerChoice → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Mwaghavul.instReprVerbalizerChoice : Repr VerbalizerChoice

Equations

• Mwaghavul.instReprVerbalizerChoice = { reprPrec := Mwaghavul.instReprVerbalizerChoice.repr }

def Mwaghavul.verbM : Tone.Spec

The M-tone verbaliser (VBZ₁): targets only unreduplicated ideophones. Overwrites every TBU of the host with M.

Equations

• Mwaghavul.verbM = { name := "VBZ₁", melody := [Tone.TRN.M], window := Tone.ValuationWindow.whole }

def Mwaghavul.verbMH : Tone.Spec

The M-H verbaliser (VBZ₂): targets both unreduplicated and reduplicated ideophones. Nonfinal TBUs get M, final gets H.

Equations

• Mwaghavul.verbMH = { name := "VBZ₂", melody := [Tone.TRN.M, Tone.TRN.H], window := Tone.ValuationWindow.nonfinalFinal }

structure Mwaghavul.Ideophone : Type

An ideophone entry: base form, gloss, lexical tones, and which verbaliser it selects. Tone pattern is listed left-to-right matching syllable order.

Whether an ideophone undergoes M or M-H alternation is lexically determined and not predictable from syllable structure or tone ([AF26] §3.1).

• form : String
• gloss : String
• tones : List Tone.TRN
• verbType : VerbalizerChoice

def Mwaghavul.instReprIdeophone.repr : Ideophone → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Mwaghavul.instReprIdeophone : Repr Ideophone

Equations

• Mwaghavul.instReprIdeophone = { reprPrec := Mwaghavul.instReprIdeophone.repr }

def Mwaghavul.Ideophone.nSyl (i : Ideophone) : ℕ

Number of syllables, derived from the tone list.

Equations

• i.nSyl = i.tones.length

def Mwaghavul.zut : Ideophone

Equations

• Mwaghavul.zut = { form := "zùt", gloss := "how solid substance ejects", tones := [Tone.TRN.L], verbType := Mwaghavul.VerbalizerChoice.m }

def Mwaghavul.diis : Ideophone

Equations

• Mwaghavul.diis = { form := "dìːs", gloss := "blood sucking", tones := [Tone.TRN.L], verbType := Mwaghavul.VerbalizerChoice.m }

def Mwaghavul.kwaaj : Ideophone

Equations

• Mwaghavul.kwaaj = { form := "kwàj", gloss := "bubbling hot water", tones := [Tone.TRN.L], verbType := Mwaghavul.VerbalizerChoice.m }

def Mwaghavul.vjaar : Ideophone

Equations

• Mwaghavul.vjaar = { form := "vjàr", gloss := "pouring of urine", tones := [Tone.TRN.L], verbType := Mwaghavul.VerbalizerChoice.m }

def Mwaghavul.shweer : Ideophone

Equations

• Mwaghavul.shweer = { form := "ʃwèr", gloss := "how water falls", tones := [Tone.TRN.L], verbType := Mwaghavul.VerbalizerChoice.m }

def Mwaghavul.wuulash : Ideophone

Equations

• Mwaghavul.wuulash = { form := "wùlàʃ", gloss := "wide open", tones := [Tone.TRN.L, Tone.TRN.L], verbType := Mwaghavul.VerbalizerChoice.m }

def Mwaghavul.fooyoop : Ideophone

Equations

• Mwaghavul.fooyoop = { form := "fɔ̀yɔ̀p", gloss := "oily", tones := [Tone.TRN.L, Tone.TRN.L], verbType := Mwaghavul.VerbalizerChoice.m }

def Mwaghavul.vjayaap : Ideophone

Equations

• Mwaghavul.vjayaap = { form := "vjàyàp", gloss := "liquid ejects from a fruit", tones := [Tone.TRN.L, Tone.TRN.L], verbType := Mwaghavul.VerbalizerChoice.m }

def Mwaghavul.bishool : Ideophone

Equations

• Mwaghavul.bishool = { form := "bìʃɔ̀l", gloss := "shabbily dressed", tones := [Tone.TRN.L, Tone.TRN.L], verbType := Mwaghavul.VerbalizerChoice.mh }

def Mwaghavul.kitiif : Ideophone

Equations

• Mwaghavul.kitiif = { form := "kìtíf", gloss := "untidy", tones := [Tone.TRN.L, Tone.TRN.H], verbType := Mwaghavul.VerbalizerChoice.mh }

def Mwaghavul.kodzoong : Ideophone

Equations

• Mwaghavul.kodzoong = { form := "kɔ̀dʒɔ̀ŋ", gloss := "walking effortfully", tones := [Tone.TRN.L, Tone.TRN.L], verbType := Mwaghavul.VerbalizerChoice.mh }

def Mwaghavul.kitfor : Ideophone

Equations

• Mwaghavul.kitfor = { form := "kìtʃɔ̀r", gloss := "old-sounding vehicle", tones := [Tone.TRN.L, Tone.TRN.L], verbType := Mwaghavul.VerbalizerChoice.mh }

def Mwaghavul.korjong : Ideophone

Equations

• Mwaghavul.korjong = { form := "kɔ̀rjɔ̀ŋ", gloss := "crooked", tones := [Tone.TRN.L, Tone.TRN.L], verbType := Mwaghavul.VerbalizerChoice.mh }

def Mwaghavul.mondos : Ideophone

Equations

• Mwaghavul.mondos = { form := "mɔ̀ndɔ̀s", gloss := "big nose", tones := [Tone.TRN.L, Tone.TRN.L], verbType := Mwaghavul.VerbalizerChoice.mh }

def Mwaghavul.vwaplas : Ideophone

Equations

• Mwaghavul.vwaplas = { form := "vwàplàs", gloss := "oversized", tones := [Tone.TRN.L, Tone.TRN.L], verbType := Mwaghavul.VerbalizerChoice.mh }

def Mwaghavul.jalpat : Ideophone

Equations

• Mwaghavul.jalpat = { form := "jàlpàt", gloss := "hanging loose", tones := [Tone.TRN.L, Tone.TRN.L], verbType := Mwaghavul.VerbalizerChoice.mh }

def Mwaghavul.hanlayap : Ideophone

Equations

• Mwaghavul.hanlayap = { form := "háŋláyáp", gloss := "light-weighted", tones := [Tone.TRN.H, Tone.TRN.H, Tone.TRN.H], verbType := Mwaghavul.VerbalizerChoice.mh }

def Mwaghavul.hamhoyof : Ideophone

Equations

• Mwaghavul.hamhoyof = { form := "hámhɔ̀yɔ̀ʃ", gloss := "dryness of cracked feet", tones := [Tone.TRN.H, Tone.TRN.L, Tone.TRN.L], verbType := Mwaghavul.VerbalizerChoice.mh }

structure Mwaghavul.Syl : Type

A toned Mwaghavul syllable.

• ipa : String

@[implicit_reducible]

instance Mwaghavul.instDecidableEqSyl : DecidableEq Syl

Equations

• Mwaghavul.instDecidableEqSyl = Mwaghavul.instDecidableEqSyl.decEq

def Mwaghavul.instDecidableEqSyl.decEq (x✝ x✝¹ : Syl) : Decidable (x✝ = x✝¹)

Equations

• Mwaghavul.instDecidableEqSyl.decEq { ipa := a } { ipa := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def Mwaghavul.instReprSyl.repr : Syl → ℕ → Std.Format

Equations

• Mwaghavul.instReprSyl.repr x✝ prec✝ = Std.Format.bracket "{ " (Std.Format.nil ++ Std.Format.text "ipa" ++ Std.Format.text " := " ++ (Std.Format.nest 7 (repr x✝.ipa)).group) " }"

@[implicit_reducible]

instance Mwaghavul.instReprSyl : Repr Syl

Equations

• Mwaghavul.instReprSyl = { reprPrec := Mwaghavul.instReprSyl.repr }

@[reducible, inline]

abbrev Mwaghavul.TSyl : Type

Convenience: a toned Mwaghavul syllable.

Equations

• Mwaghavul.TSyl = Tone.TBU Mwaghavul.Syl

def Mwaghavul.mkTSyl (ipa : String) (t : Tone.TRN) : TSyl

Build a toned syllable from IPA and tone.

Equations

• Mwaghavul.mkTSyl ipa t = { seg := { ipa := ipa }, tone := t }

def Mwaghavul.deriveVerb (base : Ideophone) : List Tone.TRN

Derive a verb from an ideophone using its verbaliser spec. Returns the output tonal pattern.

Equations

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

theorem Mwaghavul.wuulash_verb : deriveVerb wuulash = [Tone.TRN.M, Tone.TRN.M]

theorem Mwaghavul.diis_verb : deriveVerb diis = [Tone.TRN.M]

theorem Mwaghavul.bishool_verb : deriveVerb bishool = [Tone.TRN.M, Tone.TRN.H]

theorem Mwaghavul.hanlayap_verb : deriveVerb hanlayap = [Tone.TRN.M, Tone.TRN.M, Tone.TRN.H]

theorem Mwaghavul.kitiif_verb : deriveVerb kitiif = [Tone.TRN.M, Tone.TRN.H]

theorem Mwaghavul.jalpat_verb : deriveVerb jalpat = [Tone.TRN.M, Tone.TRN.H]

theorem Mwaghavul.m_verb_uniform (i : Ideophone) (h : i.verbType = VerbalizerChoice.m) : deriveVerb i = List.map (fun (x : Tone.TRN) => Tone.TRN.M) i.tones

All M-tone derived verbs produce uniform M across all TBUs (13a).

theorem Mwaghavul.mh_verb_bisyllabic_pattern (i : Ideophone) (h : i.verbType = VerbalizerChoice.mh) (h2 : i.tones.length = 2) : deriveVerb i = [Tone.TRN.M, Tone.TRN.H]

M-H derived verbs have M on nonfinal TBUs and H on the final TBU. Verified on bisyllabic bases.