Guébie vowels

Guébie (Kru; Côte d'Ivoire) has ten vowels, five [+ATR] vowels /i e ə o u/ paired with five [−ATR] vowels /ɪ ɛ a ɔ ʊ/, as Sande describes them. The pairs agree in backness and rounding, and in height except for /ə a/. Vowels within a morpheme agree in [ATR], and affixes harmonize with roots.

The feature values come from the PHOIBLE chart, which codes the tongue-root contrast by [tense], so a vowel is the segment of its chart entry's tongue-root reading. The chart's /ə/ is [−tense], and Guébie's /ə/ departs from it in being [+ATR].

Main definitions

• Guebie.i, Guebie.schwa and the like: the ten vowels, and Guebie.vowels the set of them.
• Guebie.atr: a segment's [ATR] value.
• Guebie.withATR: the member of a vowel's pair with a given [ATR] value.

Main results

• Guebie.withATR_atr: a segment's own [ATR] value leaves it unchanged.
• Guebie.atr_withATR: the member of a vowel's pair with a value has that value.

References

• [San22]
• [MMcC19]

def Guebie.vowel (m : Data.PHOIBLE.FeatureMatrix) (departure : Phonology.Segment := ⊥) : Phonology.Segment

A vowel is the segment of its chart entry's tongue-root reading, with its departure.

Equations

• Guebie.vowel m departure = Phonology.Segment.ofChart m.tenseAsATR departure

def Guebie.i : Phonology.Segment

The advanced high front vowel /i/.

Equations

• Guebie.i = Guebie.vowel Data.PHOIBLE.FeatureMatrix.i

def Guebie.e : Phonology.Segment

The advanced mid front vowel /e/.

Equations

• Guebie.e = Guebie.vowel Data.PHOIBLE.FeatureMatrix.e

def Guebie.schwa : Phonology.Segment

The advanced mid central vowel /ə/.

Equations

• Guebie.schwa = Guebie.vowel Data.PHOIBLE.FeatureMatrix.«ə» (Phonology.Segment.ofSpecs [(Phonology.Feature.atr, true)])

def Guebie.o : Phonology.Segment

The advanced mid back vowel /o/.

Equations

• Guebie.o = Guebie.vowel Data.PHOIBLE.FeatureMatrix.o

def Guebie.u : Phonology.Segment

The advanced high back vowel /u/.

Equations

• Guebie.u = Guebie.vowel Data.PHOIBLE.FeatureMatrix.u

def Guebie.smallCapitalI : Phonology.Segment

The unadvanced high front vowel /ɪ/.

Equations

• Guebie.smallCapitalI = Guebie.vowel Data.PHOIBLE.FeatureMatrix.«ɪ»

def Guebie.epsilon : Phonology.Segment

The unadvanced mid front vowel /ɛ/.

Equations

• Guebie.epsilon = Guebie.vowel Data.PHOIBLE.FeatureMatrix.«ɛ»

def Guebie.a : Phonology.Segment

The unadvanced low vowel /a/.

Equations

• Guebie.a = Guebie.vowel Data.PHOIBLE.FeatureMatrix.a

def Guebie.openO : Phonology.Segment

The unadvanced mid back vowel /ɔ/.

Equations

• Guebie.openO = Guebie.vowel Data.PHOIBLE.FeatureMatrix.«ɔ»

def Guebie.upsilon : Phonology.Segment

The unadvanced high back vowel /ʊ/.

Equations

• Guebie.upsilon = Guebie.vowel Data.PHOIBLE.FeatureMatrix.«ʊ»

def Guebie.vowels : Finset Phonology.Segment

The ten vowels, pairwise distinct.

Equations

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

def Guebie.atr (x : Phonology.Segment) : Bool

A segment's [ATR] value, true for [+ATR].

Equations

• Guebie.atr x = decide (x.HasValue Phonology.Feature.atr true)

theorem Guebie.atr_iff (x : Phonology.Segment) : x ∈ vowels → (atr x = true ↔ x ∈ {i, e, schwa, o, u})

The advanced vowels are /i e ə o u/.

def Guebie.pairs : List (Phonology.Segment × Phonology.Segment)

The ±ATR pairs, the [+ATR] member first, are /i ɪ/, /e ɛ/, /ə a/, /o ɔ/ and /u ʊ/.

Equations

• Guebie.pairs = [(Guebie.i, Guebie.smallCapitalI), (Guebie.e, Guebie.epsilon), (Guebie.schwa, Guebie.a), (Guebie.o, Guebie.openO), (Guebie.u, Guebie.upsilon)]

def Guebie.withATR (x : Phonology.Segment) (b : Bool) : Phonology.Segment

The member of a vowel's pair with the given [ATR] value. The pair /ə a/ differs in height too, so this is not Segment.setFeature .atr. A segment in no pair is left unchanged.

Equations

• Guebie.withATR x b = match List.find? (fun (p : Phonology.Segment × Phonology.Segment) => decide (p.1 = x ∨ p.2 = x)) Guebie.pairs with | some p => if b = true then p.1 else p.2 | none => x

@[simp]

theorem Guebie.withATR_atr (x : Phonology.Segment) : withATR x (atr x) = x

theorem Guebie.atr_withATR (x : Phonology.Segment) : x ∈ vowels → ∀ (b : Bool), atr (withATR x b) = b