Guébie: vowels, ATR, and particle verbs

Lexical substrate for Guébie (Kru; Côte d'Ivoire): the ten-vowel ±ATR inventory ([San22] §3.2, [SCD26] (1)) and the particle-verb lexicon ([SCD26] (10)–(12)). Particle verbs are phrasal idioms — a prefixing particle plus a verb, with noncompositional meaning; the particle harmonizes with the verb root in ATR when both are spelled out in the same phase, and carries its lexical value otherwise.

Main definitions

• Guebie.Vowel, Guebie.Vowel.atr: the ten-vowel inventory and its ±ATR split.
• Guebie.Morpheme: a transcription with vowel skeleton; Morpheme.atr is its lexical ATR value (morpheme-internal vowels agree, Morpheme.ATRUniform).
• Guebie.ParticleVerb, Guebie.particleVerbs: the (10) inventory plus the (11)–(12) /jɔkʊ/+/ni/ 'see' pair; harmonizedParticleATR is the SAuxOV surface value.

inductive Guebie.Vowel : Type

The ten Guébie vowels ([San22] §3.2). Constructor names ASCII-ize the IPA (capital = lax −ATR counterpart): schwa = ə, I = ɪ, E = ɛ, O = ɔ, U = ʊ.

• i : Vowel
• e : Vowel
• schwa : Vowel
• o : Vowel
• u : Vowel
• I : Vowel
• E : Vowel
• a : Vowel
• O : Vowel
• U : Vowel

@[implicit_reducible]

instance Guebie.instDecidableEqVowel : DecidableEq Vowel

Equations

• Guebie.instDecidableEqVowel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Guebie.instReprVowel.repr : Vowel → ℕ → Std.Format

Equations

• Guebie.instReprVowel.repr Guebie.Vowel.i prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Guebie.Vowel.i")).group prec✝
• Guebie.instReprVowel.repr Guebie.Vowel.e prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Guebie.Vowel.e")).group prec✝
• Guebie.instReprVowel.repr Guebie.Vowel.schwa prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Guebie.Vowel.schwa")).group prec✝
• Guebie.instReprVowel.repr Guebie.Vowel.o prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Guebie.Vowel.o")).group prec✝
• Guebie.instReprVowel.repr Guebie.Vowel.u prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Guebie.Vowel.u")).group prec✝
• Guebie.instReprVowel.repr Guebie.Vowel.I prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Guebie.Vowel.I")).group prec✝
• Guebie.instReprVowel.repr Guebie.Vowel.E prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Guebie.Vowel.E")).group prec✝
• Guebie.instReprVowel.repr Guebie.Vowel.a prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Guebie.Vowel.a")).group prec✝
• Guebie.instReprVowel.repr Guebie.Vowel.O prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Guebie.Vowel.O")).group prec✝
• Guebie.instReprVowel.repr Guebie.Vowel.U prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Guebie.Vowel.U")).group prec✝

@[implicit_reducible]

instance Guebie.instReprVowel : Repr Vowel

Equations

• Guebie.instReprVowel = { reprPrec := Guebie.instReprVowel.repr }

def Guebie.Vowel.atr : Vowel → Phonology.TongueRoot.ATR

The ±ATR split ([SCD26] (1)).

Equations

• Guebie.Vowel.i.atr = Phonology.TongueRoot.ATR.plus
• Guebie.Vowel.e.atr = Phonology.TongueRoot.ATR.plus
• Guebie.Vowel.schwa.atr = Phonology.TongueRoot.ATR.plus
• Guebie.Vowel.o.atr = Phonology.TongueRoot.ATR.plus
• Guebie.Vowel.u.atr = Phonology.TongueRoot.ATR.plus
• Guebie.Vowel.I.atr = Phonology.TongueRoot.ATR.minus
• Guebie.Vowel.E.atr = Phonology.TongueRoot.ATR.minus
• Guebie.Vowel.a.atr = Phonology.TongueRoot.ATR.minus
• Guebie.Vowel.O.atr = Phonology.TongueRoot.ATR.minus
• Guebie.Vowel.U.atr = Phonology.TongueRoot.ATR.minus

structure Guebie.Morpheme : Type

A Guébie morpheme: transcription, vowel skeleton, optional gloss.

• form : String
• vowels : List Vowel
• gloss : Option String

@[implicit_reducible]

instance Guebie.instDecidableEqMorpheme : DecidableEq Morpheme

Equations

• Guebie.instDecidableEqMorpheme = Guebie.instDecidableEqMorpheme.decEq

def Guebie.instDecidableEqMorpheme.decEq (x✝ x✝¹ : Morpheme) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Guebie.instReprMorpheme : Repr Morpheme

Equations

• Guebie.instReprMorpheme = { reprPrec := Guebie.instReprMorpheme.repr }

def Guebie.instReprMorpheme.repr : Morpheme → ℕ → Std.Format

Equations

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

def Guebie.Morpheme.atr (m : Morpheme) : Phonology.TongueRoot.ATR

The lexical ATR value: the value of the morpheme's (agreeing) vowels. The rare vowelless morphemes are treated as [−ATR]; they neither trigger nor block (kɔ-ɲ 'give' surfaces −ATR, (10)).

Equations

• m.atr = (Option.map Guebie.Vowel.atr m.vowels.head?).getD Phonology.TongueRoot.ATR.minus

def Guebie.Morpheme.ATRUniform (m : Morpheme) : Prop

Morpheme-internal vowels agree in ATR ([SCD26] §2.1).

Equations

• m.ATRUniform = ∀ (v : Guebie.Vowel), v ∈ m.vowels → v.atr = m.atr

@[implicit_reducible]

instance Guebie.instDecidableATRUniform (m : Morpheme) : Decidable m.ATRUniform

Equations

• Guebie.instDecidableATRUniform m = id inferInstance

Particles ([SCD26] (10)–(12))

Underlying forms; surface ATR alternates under harmony (e.g. /mɛ/ → [me] before a +ATR root, /jɔkʊ/ → [joku]). dakɔ and jɔkʊ have no independent gloss.

def Guebie.mE : Morpheme

Equations

• Guebie.mE = { form := "mɛ", vowels := [Guebie.Vowel.E], gloss := some "in" }

def Guebie.kO : Morpheme

Equations

• Guebie.kO = { form := "kɔ", vowels := [Guebie.Vowel.O], gloss := some "at/to" }

def Guebie.dakO : Morpheme

Equations

• Guebie.dakO = { form := "dakɔ", vowels := [Guebie.Vowel.a, Guebie.Vowel.O] }

def Guebie.jOkU : Morpheme

Equations

• Guebie.jOkU = { form := "jɔkʊ", vowels := [Guebie.Vowel.O, Guebie.Vowel.U] }

Verbs appearing in the particle-verb inventory

def Guebie.tE : Morpheme

Equations

• Guebie.tE = { form := "tɛ", vowels := [Guebie.Vowel.E], gloss := some "be strong" }

def Guebie.trO : Morpheme

Equations

• Guebie.trO = { form := "trɔ", vowels := [Guebie.Vowel.O], gloss := some "be long/tall" }

def Guebie.para : Morpheme

Equations

• Guebie.para = { form := "para", vowels := [Guebie.Vowel.a, Guebie.Vowel.a] }

def Guebie.salI : Morpheme

Equations

• Guebie.salI = { form := "salɪ", vowels := [Guebie.Vowel.a, Guebie.Vowel.I] }

def Guebie.nu : Morpheme

Equations

• Guebie.nu = { form := "nu", vowels := [Guebie.Vowel.u], gloss := some "hear" }

def Guebie.silije : Morpheme

Equations

• Guebie.silije = { form := "silije", vowels := [Guebie.Vowel.i, Guebie.Vowel.i, Guebie.Vowel.e] }

def Guebie.djE : Morpheme

Equations

• Guebie.djE = { form := "ɟɛ", vowels := [Guebie.Vowel.E] }

def Guebie.pulo : Morpheme

Equations

• Guebie.pulo = { form := "pulo", vowels := [Guebie.Vowel.u, Guebie.Vowel.o], gloss := some "be fast" }

def Guebie.ny : Morpheme

Equations

• Guebie.ny = { form := "ɲ", vowels := [] }

def Guebie.ggO : Morpheme

Equations

• Guebie.ggO = { form := "ggɔ", vowels := [Guebie.Vowel.O] }

def Guebie.wa : Morpheme

Equations

• Guebie.wa = { form := "wa", vowels := [Guebie.Vowel.a] }

def Guebie.ni : Morpheme

Equations

• Guebie.ni = { form := "ni", vowels := [Guebie.Vowel.i], gloss := some "see" }

Particle verbs

structure Guebie.ParticleVerb : Type

A particle-verb pair: a phrasal idiom with noncompositional meaning ([SCD26] (10)).

• particle : Morpheme
• verb : Morpheme
• gloss : String

def Guebie.instDecidableEqParticleVerb.decEq (x✝ x✝¹ : ParticleVerb) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Guebie.instDecidableEqParticleVerb : DecidableEq ParticleVerb

Equations

• Guebie.instDecidableEqParticleVerb = Guebie.instDecidableEqParticleVerb.decEq

def Guebie.instReprParticleVerb.repr : ParticleVerb → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Guebie.instReprParticleVerb : Repr ParticleVerb

Equations

• Guebie.instReprParticleVerb = { reprPrec := Guebie.instReprParticleVerb.repr }

def Guebie.ParticleVerb.harmonizedParticleATR (pv : ParticleVerb) : Phonology.TongueRoot.ATR

The particle's surface ATR in SAuxOV contexts: the verb root's value ([SCD26] (12)).

Equations

• pv.harmonizedParticleATR = pv.verb.atr

def Guebie.particleVerbs : List ParticleVerb

The (10) inventory, plus the (11)–(12) /jɔkʊ/+/ni/ pair.

Equations

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

theorem Guebie.particleVerbs_ATRUniform (pv : ParticleVerb) : pv ∈ particleVerbs → pv.particle.ATRUniform ∧ pv.verb.ATRUniform

Every morpheme in the lexicon is ATR-uniform.

theorem Guebie.joku_alternation : jOkU.atr = Phonology.TongueRoot.ATR.minus ∧ { particle := jOkU, verb := ni, gloss := "see" }.harmonizedParticleATR = Phonology.TongueRoot.ATR.plus

The (11)–(12) alternation: −ATR /jɔkʊ/ surfaces +ATR ([joku]) under harmony with the +ATR root /ni/ 'see'.

def Guebie.tongueRoot : Phonology.TongueRoot.TongueRootProfile

Guébie's tongue-root row: a ten-vowel /2IU/ system with root-controlled harmony ([SCD26] §2.1; [Cas24] (1)). No dominance pattern is reported.

Equations

• Guebie.tongueRoot = { inventoryClass := Phonology.TongueRoot.InventoryClass.twoIU, control := Phonology.Harmony.ControlType.rootControlled, dominant := none }