Tongue-root systems and the [ATR]-inventory correlation

Casali's typology of tongue-root harmony systems ([Cas24], the inventory-structure chapter of [RvdH24a]; [Cas03], [Cas08]): systems with a tongue-root contrast in high vowels (/2IU/) are characteristically [+ATR]-dominant (69 of 72 surveyed), while systems contrasting tongue root only in non-high vowels (/1IU/) show [+ATR] inertness and [−ATR] dominance indicators. Whether the feature is binary [±ATR] or privative [ATR]/[RTR] is explicitly open in the source; the value type here is neutral between the two readings.

The correlation is a defeasible typological tendency, never a theorem: Casali's own chapter records /1IU/ exceptions (Legbo, Ikoma), a questionable /2IU/ exception (Kimatuumbi), and a dominance-reversal class (Kinande, Komo, Lango, Turkana, …) where [+ATR] dominance is overridden in identifiable contexts. Per-language rows live with fragments and studies, not here.

Main definitions

• ATR: the tongue-root feature value.
• InventoryClass: Casali's /2IU/ vs /1IU/ classification (applies only to systems with a tongue-root contrast at all — five-vowel systems are excluded).
• DominanceIndicator: the five evidence types for a dominant value.
• TongueRootProfile, InventoryClass.predictedDominant: a language's row schema and the correlation as a prediction function; conformance is stated inline at use sites (∀ v ∈ p.dominant, v = p.inventoryClass.predictedDominant).

inductive Phonology.TongueRoot.ATR : Type

The tongue-root feature value: [+ATR] or [−ATR]. Neutral between binary and privative readings ([Cas24]).

• plus : ATR
• minus : ATR

@[implicit_reducible]

instance Phonology.TongueRoot.instDecidableEqATR : DecidableEq ATR

Equations

• Phonology.TongueRoot.instDecidableEqATR x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phonology.TongueRoot.instReprATR.repr : ATR → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phonology.TongueRoot.instReprATR : Repr ATR

Equations

• Phonology.TongueRoot.instReprATR = { reprPrec := Phonology.TongueRoot.instReprATR.repr }

def Phonology.TongueRoot.ATR.opp : ATR → ATR

The opposite value.

Equations

• Phonology.TongueRoot.ATR.plus.opp = Phonology.TongueRoot.ATR.minus
• Phonology.TongueRoot.ATR.minus.opp = Phonology.TongueRoot.ATR.plus

@[simp]

theorem Phonology.TongueRoot.ATR.opp_opp (v : ATR) : v.opp.opp = v

inductive Phonology.TongueRoot.InventoryClass : Type

Casali's inventory classification: where the tongue-root contrast lives. Only systems with a contrast at all are classified (five-vowel /i e a o u/ systems fall outside the typology, [Cas24] fn. 1).

• twoIU : InventoryClass

  Contrast in high vowels (possibly elsewhere too): nine-vowel Akan/Maasai, seven-vowel Kinande, ten-vowel Guébie.

• oneIU : InventoryClass

  Contrast only in non-high vowels: the common seven-vowel /i u e ɛ o ɔ a/ type (Yoruba, Wolof).

@[implicit_reducible]

instance Phonology.TongueRoot.instDecidableEqInventoryClass : DecidableEq InventoryClass

Equations

• Phonology.TongueRoot.instDecidableEqInventoryClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Phonology.TongueRoot.instReprInventoryClass : Repr InventoryClass

Equations

• Phonology.TongueRoot.instReprInventoryClass = { reprPrec := Phonology.TongueRoot.instReprInventoryClass.repr }

def Phonology.TongueRoot.instReprInventoryClass.repr : InventoryClass → ℕ → Std.Format

Equations

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

inductive Phonology.TongueRoot.DominanceIndicator : Type

The five evidence types for a dominant [ATR] value ([Cas24] §15.2.1, following [Cas03]).

• dominantAffix : DominanceIndicator

  Invariant dominant affixes spreading onto roots (Maasai /íé/).

• crossWordSpreading : DominanceIndicator

  Spreading across word boundaries or between compound members.

• coalescencePreservation : DominanceIndicator

  Systematic preservation of one value in vowel coalescence.

• allophonicDominance : DominanceIndicator

  A phonemically unpaired vowel with a predictable harmonized allophone.

• weakAssimilatory : DominanceIndicator

  Harmonizing affixes surfacing with one value where harmony is inapplicable.

@[implicit_reducible]

instance Phonology.TongueRoot.instDecidableEqDominanceIndicator : DecidableEq DominanceIndicator

Equations

• Phonology.TongueRoot.instDecidableEqDominanceIndicator x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Phonology.TongueRoot.instReprDominanceIndicator : Repr DominanceIndicator

Equations

• Phonology.TongueRoot.instReprDominanceIndicator = { reprPrec := Phonology.TongueRoot.instReprDominanceIndicator.repr }

def Phonology.TongueRoot.instReprDominanceIndicator.repr : DominanceIndicator → ℕ → Std.Format

Equations

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

structure Phonology.TongueRoot.TongueRootProfile : Type

A language's tongue-root row: inventory class, control type (Phonology.Harmony.ControlType — cross-cutting the inventory classification: root-controlled Degema and Guébie vs dominant-recessive Maasai), and the observed dominant value with its evidence (none = symmetric/inert patterning).

• inventoryClass : InventoryClass
• control : Harmony.ControlType ATR
• dominant : Option ATR
• evidence : List DominanceIndicator

@[implicit_reducible]

instance Phonology.TongueRoot.instDecidableEqTongueRootProfile : DecidableEq TongueRootProfile

Equations

• Phonology.TongueRoot.instDecidableEqTongueRootProfile = Phonology.TongueRoot.instDecidableEqTongueRootProfile.decEq

def Phonology.TongueRoot.instDecidableEqTongueRootProfile.decEq (x✝ x✝¹ : TongueRootProfile) : Decidable (x✝ = x✝¹)

Equations

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

def Phonology.TongueRoot.instReprTongueRootProfile.repr : TongueRootProfile → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phonology.TongueRoot.instReprTongueRootProfile : Repr TongueRootProfile

Equations

• Phonology.TongueRoot.instReprTongueRootProfile = { reprPrec := Phonology.TongueRoot.instReprTongueRootProfile.repr }

def Phonology.TongueRoot.InventoryClass.predictedDominant : InventoryClass → ATR

The dominant value the [ATR]-inventory correlation predicts from inventory structure ([Cas24]): /2IU/ systems tend to [+ATR] dominance, /1IU/ systems to [−ATR] dominance. A defeasible tendency — the chapter records the exceptions — so studies state per-language conformance inline (∀ v ∈ p.dominant, v = p.inventoryClass.predictedDominant), never as a universal theorem.

Equations

• Phonology.TongueRoot.InventoryClass.twoIU.predictedDominant = Phonology.TongueRoot.ATR.plus
• Phonology.TongueRoot.InventoryClass.oneIU.predictedDominant = Phonology.TongueRoot.ATR.minus