Aksënova, Rawski, Graf & Heinz 2024: the computational power of harmonic forms

[ARGH24] §34.3.1 works out three double vowel harmonies with their TSL grammars printed (Tables 34.3–34.5); a single tier always suffices. This study transcribes the grammars featurally and stress-tests Phonology.Harmony.Pattern: Kirghiz is the conjunction of two patterns on one tier (kirghiz_two_patterns); Buryat's asymmetric blocking defeats every symmetric relation (buryat_not_symmetric) — the finding that forced blocker imposition into Pattern.Compatible — and with imposition is expressible (buryat_expressible, certified on the (9) forms); Yakut's harmonizing blockers show the same asymmetry (yakut_asymmetric); whether its configuration-dependent grammar is a conjunction of patterns is left open.

Constructor names ASCII-ize the IPA: ih = ɨ, oe = ö, ue = ü, oh = ɔ, uh = ʊ. The §34.3.4 tier-relation typology is formalized as a classifier computed from patterns' tiers (tierRelation); the vowel-language rows of Table 34.8 check out as single-tier (kirghiz_same_tier, buryat_same_tier). TODO: the embedded/disjoint rows (Imdlawn Tashlhiyt sibilants, Kikongo) need their consonant alphabets.

Kirghiz ((5), Table 34.3): double harmony, one tier, two patterns

inductive AksenovaEtAl2024.KirghizV : Type

The Kirghiz vowel tier T = {a, ɨ, e, i, o, ö, u, ü}.

• a : KirghizV
• ih : KirghizV
• e : KirghizV
• i : KirghizV
• o : KirghizV
• oe : KirghizV
• u : KirghizV
• ue : KirghizV

@[implicit_reducible]

instance AksenovaEtAl2024.instDecidableEqKirghizV : DecidableEq KirghizV

Equations

• AksenovaEtAl2024.instDecidableEqKirghizV x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance AksenovaEtAl2024.instFintypeKirghizV : Fintype KirghizV

Equations

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

@[implicit_reducible]

instance AksenovaEtAl2024.instReprKirghizV : Repr KirghizV

Equations

• AksenovaEtAl2024.instReprKirghizV = { reprPrec := AksenovaEtAl2024.instReprKirghizV.repr }

def AksenovaEtAl2024.instReprKirghizV.repr : KirghizV → ℕ → Std.Format

Equations

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

def AksenovaEtAl2024.KirghizV.front : KirghizV → Bool

Equations

• AksenovaEtAl2024.KirghizV.e.front = true
• AksenovaEtAl2024.KirghizV.i.front = true
• AksenovaEtAl2024.KirghizV.oe.front = true
• AksenovaEtAl2024.KirghizV.ue.front = true
• AksenovaEtAl2024.KirghizV.a.front = false
• AksenovaEtAl2024.KirghizV.ih.front = false
• AksenovaEtAl2024.KirghizV.o.front = false
• AksenovaEtAl2024.KirghizV.u.front = false

def AksenovaEtAl2024.KirghizV.round : KirghizV → Bool

Equations

• AksenovaEtAl2024.KirghizV.o.round = true
• AksenovaEtAl2024.KirghizV.oe.round = true
• AksenovaEtAl2024.KirghizV.u.round = true
• AksenovaEtAl2024.KirghizV.ue.round = true
• AksenovaEtAl2024.KirghizV.a.round = false
• AksenovaEtAl2024.KirghizV.ih.round = false
• AksenovaEtAl2024.KirghizV.e.round = false
• AksenovaEtAl2024.KirghizV.i.round = false

def AksenovaEtAl2024.kirghizBanned (x y : KirghizV) : Prop

kirghizBanned x y: the tier bigram xy disagrees in fronting or in rounding (Table 34.3).

Equations

• AksenovaEtAl2024.kirghizBanned x y = (x.front ≠ y.front ∨ x.round ≠ y.round)

@[implicit_reducible]

instance AksenovaEtAl2024.instDecidableRelKirghizVKirghizBanned : DecidableRel kirghizBanned

Equations

• AksenovaEtAl2024.instDecidableRelKirghizVKirghizBanned x y = id inferInstance

def AksenovaEtAl2024.kirghizFront : Phonology.Harmony.Pattern KirghizV Bool

kirghizFront is Kirghiz frontness harmony: every vowel participates.

Equations

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

def AksenovaEtAl2024.kirghizRound : Phonology.Harmony.Pattern KirghizV Bool

kirghizRound is Kirghiz rounding harmony, on the same tier.

Equations

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

theorem AksenovaEtAl2024.kirghiz_two_patterns (x y : KirghizV) : kirghizBanned x y ↔ ¬(kirghizFront.Compatible x y ∧ kirghizRound.Compatible x y)

Kirghiz double harmony fits a single tier: the printed grammar is the conjunction of the two patterns' compatibilities.

Buryat ((9), Table 34.4): asymmetric blocking defeats symmetry

inductive AksenovaEtAl2024.BuryatV : Type

The Buryat vowel tier T = {a, e, ɔ, o, ʊ, u} (transparent /i/ excluded).

• a : BuryatV
• e : BuryatV
• oh : BuryatV
• o : BuryatV
• uh : BuryatV
• u : BuryatV

@[implicit_reducible]

instance AksenovaEtAl2024.instDecidableEqBuryatV : DecidableEq BuryatV

Equations

• AksenovaEtAl2024.instDecidableEqBuryatV x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance AksenovaEtAl2024.instFintypeBuryatV : Fintype BuryatV

Equations

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

@[implicit_reducible]

instance AksenovaEtAl2024.instReprBuryatV : Repr BuryatV

Equations

• AksenovaEtAl2024.instReprBuryatV = { reprPrec := AksenovaEtAl2024.instReprBuryatV.repr }

def AksenovaEtAl2024.instReprBuryatV.repr : BuryatV → ℕ → Std.Format

Equations

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

def AksenovaEtAl2024.BuryatV.tense : BuryatV → Bool

Equations

• AksenovaEtAl2024.BuryatV.e.tense = true
• AksenovaEtAl2024.BuryatV.o.tense = true
• AksenovaEtAl2024.BuryatV.u.tense = true
• AksenovaEtAl2024.BuryatV.a.tense = false
• AksenovaEtAl2024.BuryatV.oh.tense = false
• AksenovaEtAl2024.BuryatV.uh.tense = false

def AksenovaEtAl2024.BuryatV.high : BuryatV → Bool

Equations

• AksenovaEtAl2024.BuryatV.uh.high = true
• AksenovaEtAl2024.BuryatV.u.high = true
• AksenovaEtAl2024.BuryatV.a.high = false
• AksenovaEtAl2024.BuryatV.e.high = false
• AksenovaEtAl2024.BuryatV.oh.high = false
• AksenovaEtAl2024.BuryatV.o.high = false

def AksenovaEtAl2024.BuryatV.round : BuryatV → Bool

Equations

• AksenovaEtAl2024.BuryatV.oh.round = true
• AksenovaEtAl2024.BuryatV.o.round = true
• AksenovaEtAl2024.BuryatV.uh.round = true
• AksenovaEtAl2024.BuryatV.u.round = true
• AksenovaEtAl2024.BuryatV.a.round = false
• AksenovaEtAl2024.BuryatV.e.round = false

def AksenovaEtAl2024.buryatBanned (x y : BuryatV) : Prop

buryatBanned x y: the bigram disagrees in ATR; or disagrees in rounding between non-high vowels; or places a rounded non-high vowel after a high vowel (Table 34.4).

Equations

• AksenovaEtAl2024.buryatBanned x y = (x.tense ≠ y.tense ∨ ¬x.high = true ∧ ¬y.high = true ∧ x.round ≠ y.round ∨ x.high = true ∧ ¬y.high = true ∧ y.round = true)

@[implicit_reducible]

instance AksenovaEtAl2024.instDecidableRelBuryatVBuryatBanned : DecidableRel buryatBanned

Equations

• AksenovaEtAl2024.instDecidableRelBuryatVBuryatBanned x y = id inferInstance

theorem AksenovaEtAl2024.buryat_asymmetric : buryatBanned BuryatV.uh BuryatV.oh ∧ ¬buryatBanned BuryatV.oh BuryatV.uh

Buryat blocking is directional: *ʊɔ is banned but ɔʊ is licensed ((9b)).

theorem AksenovaEtAl2024.buryat_not_symmetric (R : BuryatV → BuryatV → Prop) (hsymm : ∀ (x y : BuryatV), R x y ↔ R y x) : ¬∀ (x y : BuryatV), R x y ↔ buryatBanned x y

No symmetric adjacency relation renders Buryat's grammar.

def AksenovaEtAl2024.buryatATR : Phonology.Harmony.Pattern BuryatV Bool

buryatATR is Buryat ATR harmony: every tier vowel participates.

Equations

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

def AksenovaEtAl2024.buryatRound : Phonology.Harmony.Pattern BuryatV Bool

buryatRound is Buryat rounding harmony: high vowels are opaque blockers transmitting unroundedness to what follows.

Equations

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

theorem AksenovaEtAl2024.buryat_expressible (x y : BuryatV) : buryatBanned x y ↔ ¬(buryatATR.Compatible x y ∧ buryatRound.Compatible x y)

With imposition, Buryat is expressible: the printed grammar is exactly the conjunction of the ATR pattern and the rounding pattern.

def AksenovaEtAl2024.buryatWellFormed (w : List BuryatV) : Prop

buryatWellFormed w says the skeleton w is harmonic for both Buryat patterns.

Equations

• AksenovaEtAl2024.buryatWellFormed w = (AksenovaEtAl2024.buryatATR.Harmonic w ∧ AksenovaEtAl2024.buryatRound.Harmonic w)

@[implicit_reducible]

instance AksenovaEtAl2024.instDecidableBuryatWellFormed (w : List BuryatV) : Decidable (buryatWellFormed w)

Equations

• AksenovaEtAl2024.instDecidableBuryatWellFormed w = id inferInstance

Yakut ((14), Table 34.5): harmonizing blockers

inductive AksenovaEtAl2024.YakutV : Type

The Yakut vowel tier T = {a, ɨ, e, i, o, ö, u, ü}.

• a : YakutV
• ih : YakutV
• e : YakutV
• i : YakutV
• o : YakutV
• oe : YakutV
• u : YakutV
• ue : YakutV

@[implicit_reducible]

instance AksenovaEtAl2024.instDecidableEqYakutV : DecidableEq YakutV

Equations

• AksenovaEtAl2024.instDecidableEqYakutV x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance AksenovaEtAl2024.instReprYakutV : Repr YakutV

Equations

• AksenovaEtAl2024.instReprYakutV = { reprPrec := AksenovaEtAl2024.instReprYakutV.repr }

def AksenovaEtAl2024.instReprYakutV.repr : YakutV → ℕ → Std.Format

Equations

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

def AksenovaEtAl2024.YakutV.front : YakutV → Bool

Equations

• AksenovaEtAl2024.YakutV.e.front = true
• AksenovaEtAl2024.YakutV.i.front = true
• AksenovaEtAl2024.YakutV.oe.front = true
• AksenovaEtAl2024.YakutV.ue.front = true
• AksenovaEtAl2024.YakutV.a.front = false
• AksenovaEtAl2024.YakutV.ih.front = false
• AksenovaEtAl2024.YakutV.o.front = false
• AksenovaEtAl2024.YakutV.u.front = false

def AksenovaEtAl2024.YakutV.round : YakutV → Bool

Equations

• AksenovaEtAl2024.YakutV.o.round = true
• AksenovaEtAl2024.YakutV.oe.round = true
• AksenovaEtAl2024.YakutV.u.round = true
• AksenovaEtAl2024.YakutV.ue.round = true
• AksenovaEtAl2024.YakutV.a.round = false
• AksenovaEtAl2024.YakutV.ih.round = false
• AksenovaEtAl2024.YakutV.e.round = false
• AksenovaEtAl2024.YakutV.i.round = false

def AksenovaEtAl2024.YakutV.high : YakutV → Bool

Equations

• AksenovaEtAl2024.YakutV.ih.high = true
• AksenovaEtAl2024.YakutV.i.high = true
• AksenovaEtAl2024.YakutV.u.high = true
• AksenovaEtAl2024.YakutV.ue.high = true
• AksenovaEtAl2024.YakutV.a.high = false
• AksenovaEtAl2024.YakutV.e.high = false
• AksenovaEtAl2024.YakutV.o.high = false
• AksenovaEtAl2024.YakutV.oe.high = false

def AksenovaEtAl2024.yakutBanned (x y : YakutV) : Prop

yakutBanned x y: the bigram disagrees in fronting; or disagrees in rounding between high vowels; or places a rounded non-high vowel after a high vowel; or disagrees in rounding after a non-high vowel (Table 34.5).

Equations

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

@[implicit_reducible]

instance AksenovaEtAl2024.instDecidableRelYakutVYakutBanned : DecidableRel yakutBanned

Equations

• AksenovaEtAl2024.instDecidableRelYakutVYakutBanned x y = id inferInstance

theorem AksenovaEtAl2024.yakut_asymmetric : yakutBanned YakutV.u YakutV.o ∧ ¬yakutBanned YakutV.o YakutV.u

Yakut's low vowels are harmonizing blockers ((14g)): rounding spreads from o to u but not from u to o — the icy-target configuration.

The tier-relation typology (§34.3.4, Table 34.8)

Of the four logical relations between two tier alphabets, only three are attested: same, embedded, and disjoint. Partially overlapping tiers are unattested — a typological tendency (the chapter reports it excludes 95% of the possible tier organizations for a ten-element alphabet), stated per row, never as a theorem.

inductive AksenovaEtAl2024.TierRelation : Type

The four logical relations between two tier alphabets (Figure 34.2).

• same : TierRelation
• embedded : TierRelation
• disjoint : TierRelation
• overlapping : TierRelation

@[implicit_reducible]

instance AksenovaEtAl2024.instDecidableEqTierRelation : DecidableEq TierRelation

Equations

• AksenovaEtAl2024.instDecidableEqTierRelation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def AksenovaEtAl2024.instReprTierRelation.repr : TierRelation → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance AksenovaEtAl2024.instReprTierRelation : Repr TierRelation

Equations

• AksenovaEtAl2024.instReprTierRelation = { reprPrec := AksenovaEtAl2024.instReprTierRelation.repr }

def AksenovaEtAl2024.tierRelation {α V W : Type} [Fintype α] [DecidableEq α] (p : Phonology.Harmony.Pattern α V) (q : Phonology.Harmony.Pattern α W) : TierRelation

tierRelation p q classifies the relation between two patterns' tier alphabets, computed from their participation functions.

Equations

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

theorem AksenovaEtAl2024.kirghiz_same_tier : tierRelation kirghizFront kirghizRound = TierRelation.same

Kirghiz's two harmonies share one tier — Table 34.8's S row.

theorem AksenovaEtAl2024.buryat_same_tier : tierRelation buryatATR buryatRound = TierRelation.same

Buryat's two harmonies share one tier — Table 34.8's S row.