Casali (2003): [ATR] value asymmetries and underlying vowel inventory structure

This file formalizes the paper's inventory typology and its account of System-Dependent [ATR] Dominance. An underlying inventory with a tongue-root contrast is a 5Ht, 4Ht(H) or 4Ht(M) system according to which heights carry the contrast, its footnote 2 (InventoryType, inventoryType?, read off a finite set of segments; the schematic inventories (1) are the witnesses nineVowel, sevenVowelHigh, sevenVowelMid, and the five-vowel system falls outside). Its survey of 110 Niger-Congo and Nilo-Saharan languages finds [+ATR] dominant where high vowels contrast and [−ATR] dominant where only mid vowels do, against the System Independence Hypothesis shared by the Universal [+ATR] Dominance and Variable [ATR] Dominance theories; the correlation is its hypothesis (20) (InventoryType.specifiedValue, SystemDependent), with Kimatuumbi and Legbo the two survey languages it leaves unexplained. Its two poles are Akan, the nine-vowel 5Ht system whose [+ATR] spreads across word boundaries and in compounds and lends /a/ a [+ATR] allophone (Table 2), and Standard Yoruba, the seven-vowel 4Ht(M) system with [−ATR] spreading in compounds (Table 4); both types derive from the fragments' inventories and both languages conform, while a [+ATR]-dominant Yoruba, its Yoruba⁺, would not (akan_conforms, yoruba_conforms, yoruba_plus_violates). Section 7 derives the correlation from lexical specification: only the specified value is present underlyingly, MAX([ATR]) preserves it and *[ATR] penalizes it. Ranked HARMONY, MAX([ATR])root ≫ *[ATR] ≫ MAX([ATR]), affixes take the root's value whatever the inputs, its tableaux (21) and (22) (rootControl_optimal); promoting MAX([ATR]) above *[ATR] lets the specified value win from either position, the classic dominant pattern (dominant_optimal); outside a harmonic context the root-control ranking strips an affix of its specification, so harmonizing affixes surface with the value opposite to the dominant one, weak assimilatory dominance, where the dominant ranking keeps the affix faithful (isolated_optimal, isolatedDominant_optimal); and a ban on [+ATR] low vowels outranking MAX([ATR]) gives indirect [−ATR] dominance before a low-vowel suffix, its tableau (23) (reversal_optimal).

Implementation notes

The [ATR] value is Phonology.Feature.atr read as Bool, true for [+ATR]. The paper's underspecified representations are rendered by constraints that see only the specified value: a candidate is a fully valued form, and a value is specified when it is the inventory type's specifiedValue. A contrast at a height is a [+ATR] vowel of that height whose [−ATR] twin is also in the inventory. The survey rows and their counts (Tables 2–7), section 3's criteria for telling 4Ht(H) from 4Ht(M) systems, and section 6's genetic discussion are not formalized.

References

• [Cas03]
• [Hay09]

Inventory types (1)

inductive Casali2003.InventoryType : Type

The three underlying inventory types with an [ATR] contrast, by the heights that carry it (footnote 2): both high and mid vowels, high vowels only, or mid vowels only.

• fiveHeight : InventoryType
• fourHeightHigh : InventoryType
• fourHeightMid : InventoryType

@[instance_reducible]

instance Casali2003.instDecidableEqInventoryType : DecidableEq InventoryType

Equations

• Casali2003.instDecidableEqInventoryType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Casali2003.instReprInventoryType : Repr InventoryType

Equations

• Casali2003.instReprInventoryType = { reprPrec := Casali2003.instReprInventoryType.repr }

def Casali2003.instReprInventoryType.repr : InventoryType → ℕ → Std.Format

Equations

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

def Casali2003.HasContrastAmong (I : Finset Phonology.Segment) (P : Phonology.Segment → Prop) [DecidablePred P] : Prop

An [ATR] contrast among the vowels of I satisfying P is a [+ATR] member whose [−ATR] twin is also a member.

Equations

• Casali2003.HasContrastAmong I P = ∃ v ∈ I, P v ∧ v.HasValue Phonology.Feature.atr true ∧ v.setFeature Phonology.Feature.atr false ∈ I

@[instance_reducible]

instance Casali2003.instDecidableHasContrastAmong (I : Finset Phonology.Segment) (P : Phonology.Segment → Prop) [DecidablePred P] : Decidable (HasContrastAmong I P)

Equations

• Casali2003.instDecidableHasContrastAmong I P = id inferInstance

def Casali2003.IsHigh (v : Phonology.Segment) : Prop

The high vowels.

Equations

• Casali2003.IsHigh v = v.HasValue Phonology.Feature.high true

@[instance_reducible]

instance Casali2003.instDecidablePredSegmentIsHigh : DecidablePred IsHigh

Equations

• Casali2003.instDecidablePredSegmentIsHigh v = Casali2003.instDecidablePredSegmentIsHigh._aux_1 v

def Casali2003.IsMid (v : Phonology.Segment) : Prop

The mid vowels.

Equations

• Casali2003.IsMid v = (v.HasValue Phonology.Feature.high false ∧ v.HasValue Phonology.Feature.low false)

@[instance_reducible]

instance Casali2003.instDecidablePredSegmentIsMid : DecidablePred IsMid

Equations

• Casali2003.instDecidablePredSegmentIsMid x✝ = { decide := decide (x✝.HasValue Phonology.Feature.high false) && decide (x✝.HasValue Phonology.Feature.low false), reflects_decide := ⋯ }

def Casali2003.inventoryType? (I : Finset Phonology.Segment) : Option InventoryType

The inventory type of I, when it has a tongue-root contrast at all: five-vowel systems fall outside the typology.

Equations

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

def Casali2003.vowel (m : Data.PHOIBLE.FeatureMatrix) : Phonology.Segment

A vowel of a schematic inventory is the segment of its chart entry's tongue-root reading, as in the fragments.

Equations

• Casali2003.vowel m = Phonology.Segment.ofChart m.tenseAsATR

def Casali2003.nineVowel : Finset Phonology.Segment

The nine-vowel 5Ht system /i ɪ e ɛ a ɔ o ʊ u/ of (1a), Akan's.

Equations

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

def Casali2003.sevenVowelMid : Finset Phonology.Segment

The seven-vowel 4Ht(M) system /i e ɛ a ɔ o u/ of (1b), Yoruba's.

Equations

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

def Casali2003.sevenVowelHigh : Finset Phonology.Segment

The seven-vowel 4Ht(H) system /i ɪ ɛ a ɔ ʊ u/ of (1c).

Equations

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

def Casali2003.fiveVowel : Finset Phonology.Segment

The five-vowel system /i e a o u/, outside the typology.

Equations

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

theorem Casali2003.nineVowel_eq : nineVowel = Akan.vowels

The 5Ht system (1a) is Akan's vowel inventory.

theorem Casali2003.sevenVowelMid_eq : sevenVowelMid = Yoruba.vowels

The 4Ht(M) system (1b) is Yoruba's vowel inventory.

theorem Casali2003.inventoryType?_schematic : inventoryType? nineVowel = some InventoryType.fiveHeight ∧ inventoryType? sevenVowelHigh = some InventoryType.fourHeightHigh ∧ inventoryType? sevenVowelMid = some InventoryType.fourHeightMid ∧ inventoryType? fiveVowel = none

The schematic inventories of (1) receive their types, and the five-vowel system none.

System-Dependent [ATR] Dominance (20)

def Casali2003.InventoryType.specifiedValue : InventoryType → Bool

The lexically specified, hence systematically dominant, [ATR] value is [+ATR] where high vowels contrast and [−ATR] where only mid vowels do.

Equations

• Casali2003.InventoryType.fiveHeight.specifiedValue = true
• Casali2003.InventoryType.fourHeightHigh.specifiedValue = true
• Casali2003.InventoryType.fourHeightMid.specifiedValue = false

def Casali2003.SystemDependent (I : Finset Phonology.Segment) (dominant : Bool) : Prop

System-Dependent [ATR] Dominance (20): a language the typology classifies has its inventory type's specified value as its systematically dominant value.

Equations

• Casali2003.SystemDependent I dominant = ∀ T ∈ Casali2003.inventoryType? I, dominant = T.specifiedValue

@[instance_reducible]

instance Casali2003.instDecidableSystemDependent (I : Finset Phonology.Segment) (dominant : Bool) : Decidable (SystemDependent I dominant)

Equations

• Casali2003.instDecidableSystemDependent I dominant = id inferInstance

Two survey languages

theorem Casali2003.akan_conforms : inventoryType? Akan.vowels = some InventoryType.fiveHeight ∧ SystemDependent Akan.vowels true

Akan's nine vowels form a 5Ht system, and its [+ATR] dominance (Table 2) conforms to (20); the [−ATR] spreading from a dominant affix it also shows (Table 5) is the indirect kind.

theorem Casali2003.yoruba_conforms : inventoryType? Yoruba.vowels = some InventoryType.fourHeightMid ∧ SystemDependent Yoruba.vowels false

Standard Yoruba's seven vowels form a 4Ht(M) system, and its [−ATR] dominance (Table 4) conforms to (20).

theorem Casali2003.yoruba_plus_violates : ¬SystemDependent Yoruba.vowels true

Yoruba⁺, a 4Ht(M) language with [+ATR] dominance, would violate (20), the typological gap the survey finds nearly empty.

Section 7: dominance from inventory-dependent specification

Only the specified value s is present underlyingly. MAX([ATR]) and its root-specific version demand that specified input values survive; *[ATR] penalizes each specified value on the surface; HARMONY demands agreement.

structure Casali2003.Word : Type

The [ATR] values of a root and an affix.

• root : Bool
• affix : Bool

@[instance_reducible]

instance Casali2003.instDecidableEqWord : DecidableEq Word

Equations

• Casali2003.instDecidableEqWord = Casali2003.instDecidableEqWord.decEq

def Casali2003.instDecidableEqWord.decEq (x✝ x✝¹ : Word) : Decidable (x✝ = x✝¹)

Equations

• Casali2003.instDecidableEqWord.decEq { root := a, affix := a_1 } { root := b, affix := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

def Casali2003.instReprWord.repr : Word → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Casali2003.instReprWord : Repr Word

Equations

• Casali2003.instReprWord = { reprPrec := Casali2003.instReprWord.repr }

def Casali2003.harmony : OptimalityTheory.Constraint Word

HARMONY requires root and affix to agree.

Equations

• Casali2003.harmony = OptimalityTheory.Constraint.binary fun (o : Casali2003.Word) => o.root ≠ o.affix

def Casali2003.maxRoot (s : Bool) (w : Word) : OptimalityTheory.Constraint Word

MAX([ATR])root requires a specified root value to survive.

Equations

• Casali2003.maxRoot s w = OptimalityTheory.Constraint.binary fun (o : Casali2003.Word) => w.root = s ∧ o.root ≠ s

def Casali2003.maxAtr (s : Bool) (w : Word) : OptimalityTheory.Constraint Word

MAX([ATR]) requires every specified input value to survive, with one violation per loss.

Equations

• Casali2003.maxAtr s w o = (if w.root = s ∧ o.root ≠ s then 1 else 0) + if w.affix = s ∧ o.affix ≠ s then 1 else 0

def Casali2003.starAtr (s : Bool) : OptimalityTheory.Constraint Word

*[ATR] assigns one violation per specified value on the surface.

Equations

• Casali2003.starAtr s o = (if o.root = s then 1 else 0) + if o.affix = s then 1 else 0

def Casali2003.outputs : List Word

The four outputs for a root–affix input.

Equations

• Casali2003.outputs = [{ root := true, affix := true }, { root := true, affix := false }, { root := false, affix := true }, { root := false, affix := false }]

def Casali2003.rootControl (s : Bool) (w : Word) : OptimalityTheory.Tableau Word 4

The root-control ranking HARMONY, MAX([ATR])root ≫ *[ATR] ≫ MAX([ATR]) over the outputs for input w: the tableaux (21) and (22).

Equations

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

theorem Casali2003.rootControl_optimal (s : Bool) (w : Word) : (rootControl s w).optimal = {{ root := w.root, affix := w.root }}

Under root control the affix takes the root's value, whatever the inputs and whichever value is specified: (21) and (22).

def Casali2003.dominant (s : Bool) (w : Word) : OptimalityTheory.Tableau Word 4

The dominant ranking promotes MAX([ATR]) above *[ATR].

Equations

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

def Casali2003.Word.dominantValue (s : Bool) (w : Word) : Bool

A dominant system assigns the specified value when either input carries it.

Equations

• Casali2003.Word.dominantValue s w = if w.root = s ∨ w.affix = s then s else !s

theorem Casali2003.dominant_optimal (s : Bool) (w : Word) : (dominant s w).optimal = {{ root := Word.dominantValue s w, affix := Word.dominantValue s w }}

Under the dominant ranking the specified value spreads from root or affix alike, the classic dominant–recessive pattern.

def Casali2003.isolated (s a : Bool) : OptimalityTheory.Tableau Bool 2

An affix outside any harmonic context under the root-control order *[ATR] ≫ MAX([ATR]), over its two surface values.

Equations

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

def Casali2003.isolatedDominant (s a : Bool) : OptimalityTheory.Tableau Bool 2

The same affix under the dominant order MAX([ATR]) ≫ *[ATR].

Equations

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

theorem Casali2003.isolated_optimal (s a : Bool) : (isolated s a).optimal = {!s}

Outside harmony a root-control system strips an affix of its specification, so harmonizing affixes surface with the value opposite to the dominant one: weak assimilatory dominance of s.

theorem Casali2003.isolatedDominant_optimal (s a : Bool) : (isolatedDominant s a).optimal = {a}

Under the dominant order an isolated affix keeps its value.

Dominance reversal (23)

structure Casali2003.LowSuffixCand : Type

An output for the input /tol-a/ of (23), a [+ATR] root with a [−ATR] low suffix in a 5Ht language, records the root's value and the suffix's [ATR] and [low] values.

• root : Bool
• suffixAtr : Bool
• suffixLow : Bool

def Casali2003.instDecidableEqLowSuffixCand.decEq (x✝ x✝¹ : LowSuffixCand) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Casali2003.instDecidableEqLowSuffixCand : DecidableEq LowSuffixCand

Equations

• Casali2003.instDecidableEqLowSuffixCand = Casali2003.instDecidableEqLowSuffixCand.decEq

@[instance_reducible]

instance Casali2003.instReprLowSuffixCand : Repr LowSuffixCand

Equations

• Casali2003.instReprLowSuffixCand = { reprPrec := Casali2003.instReprLowSuffixCand.repr }

def Casali2003.instReprLowSuffixCand.repr : LowSuffixCand → ℕ → Std.Format

Equations

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

def Casali2003.reversal : OptimalityTheory.Tableau LowSuffixCand 4

Tableau (23) ranks *[+ATR, +low] and the preservation of [+low] above HARMONY above MAX([ATR]), over [tola], [tɔla], [tolæ] and [tole].

Equations

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

theorem Casali2003.reversal_optimal : reversal.optimal = {{ root := false, suffixAtr := false, suffixLow := true }}

The root loses its [+ATR] to the low suffix, [tɔla], which is indirect [−ATR] dominance in a language whose specified value is [+ATR].