Aksënova, Rawski, Graf & Heinz (2024): The computational power of harmonic forms

Vowel-harmony phonotactics are tier-based strictly 2-local: project the harmonizing segments on a tier and ban the disagreeing bigrams. Lokaa ATR harmony is strictly local at no width, since no window bounds the transparent material between two agreeing vowels, but it is strictly 2-piecewise as well. Kirghiz, Buryat, and Yakut double harmonies each fit on a single tier, where Buryat's blocking high vowels and Yakut's harmonizing blockers are bigram bans, and blocking puts both beyond every strictly piecewise grammar. Kikongo's vowel and nasal harmonies need two tiers: together they are tier-based strictly local at no width.

Each printed grammar is a TierStrictlyLocalGrammar.ofForbiddenPairs whose tier is the paper's tier alphabet, checked against the forms of the examples and figures and their starred counterparts. In the undergoer, blocker, and transparent vocabulary of the double harmonies, which Phonology.Harmony.Pattern encodes, Kirghiz's and Buryat's grammars are each two patterns sharing a tier, the chapter's condition for one tier to suffice. Yakut's harmonizing blockers are no segment-level participation, so its rounding is no pattern beside its fronting harmony.

Main statements

• lokaa_not_isStrictlyLocal, lokaa_language_eq_sp: Lokaa is SL at no width, and its TSL₂ grammar and SP₂ grammar generate one language.
• buryat_language, buryat_not_isStrictlyPiecewise: Buryat's grammar is ATR harmony and blocked rounding harmony on one tier, and SP at no width.
• yakut_rounding_not_pattern: no segment-level pattern beside fronting harmony gives Yakut.
• kikongo_not_isTierStrictlyLocal: no single tier carries Kikongo's two harmonies.

Implementation notes

• A single-tier grammar's surface alphabet is Option V for its tier alphabet V, with none for everything off the tier: consonants, transparent vowels, length and tone marks. Kikongo's forms are read onto its two tier alphabets alone, since a segment on neither is invisible to both grammars, and a prenasalized stop is read as one onset off the nasal tier: with m projected, Table 34.7 would ban the paper's own -somp-el-, -tomb-ol-, and -lemb-ol-.
• The starred counterparts the paper prints are rows of their own, marked ungrammatical, so each harmony theorem accepts the forms of Forms.all and rejects those of Forms.marked.
• Table 34.5's H_r2 prints *üö twice and omits *üo, which H_front bans anyway.

References

• [ARGH24]
• [Hei10]
• [RP11]
• [Lam23]

Grammars on a tier

def AksenovaEtAl2024.read {V : Type} (ofChar : Char → Option V) (cs : List Char) : List (Option V)

A printed form read into the surface alphabet Option V, each character as its tier symbol or as none.

Equations

• AksenovaEtAl2024.read ofChar cs = List.map ofChar cs

def AksenovaEtAl2024.TierRel {V : Type} (R : V → V → Prop) (x y : Option V) : Prop

R between two tier symbols of the surface alphabet Option V.

Equations

• AksenovaEtAl2024.TierRel R x y = ∃ a ∈ x, ∃ b ∈ y, R a b

@[instance_reducible]

instance AksenovaEtAl2024.instDecidableRelOptionTierRel {V : Type} (R : V → V → Prop) [DecidableRel R] : DecidableRel (TierRel R)

Equations

• AksenovaEtAl2024.instDecidableRelOptionTierRel R x✝¹ x✝ = AksenovaEtAl2024.instDecidableRelOptionTierRel._aux_1 R x✝¹ x✝

@[reducible, inline]

abbrev AksenovaEtAl2024.tierGrammar {V : Type} (R : V → V → Prop) : Subregular.TierStrictlyLocalGrammar 2 (Option V)

The TSL₂ grammar of a printed table has the tier V and bans tier-adjacent R-related symbols.

Equations

• AksenovaEtAl2024.tierGrammar R = Subregular.TierStrictlyLocalGrammar.ofForbiddenPairs (AksenovaEtAl2024.TierRel R) fun (x : Option V) => x.isSome = true

Two harmonies on one tier

theorem AksenovaEtAl2024.harmonic_and_iff_mem_tsl {α : Type u_1} {W : Type u_2} {W' : Type u_3} (p : Phonology.Harmony.Pattern α W) (q : Phonology.Harmony.Pattern α W') (h : ∀ (s : α), p.OnTier s ↔ q.OnTier s) (w : List α) : p.Harmonic w ∧ q.Harmonic w ↔ w ∈ (Subregular.TierStrictlyLocalGrammar.ofForbiddenPairs (fun (a b : α) => ¬p.Compatible a b ∨ ¬q.Compatible a b) p.OnTier).language

Two harmonies with the same transparent items fit on one tier (§34.3.1). The words harmonic for both form the language of one TSL₂ grammar, which bans what either harmony bans.

def AksenovaEtAl2024.allParticipate {V : Type} (x : Option V) : Phonology.Harmony.Participation

Every tier symbol participates; everything off the tier is transparent.

Equations

• AksenovaEtAl2024.allParticipate x = if x.isSome = true then Phonology.Harmony.Participation.participating else Phonology.Harmony.Participation.transparent

Lokaa (Table 34.2): ATR agreement on the tier of non-high vowels

inductive AksenovaEtAl2024.LokaaV : Type

The Lokaa tier T = {ɛ, e, o, ə, ɔ, a}; eh = ɛ, oh = ɔ.

• eh : LokaaV
• e : LokaaV
• o : LokaaV
• schwa : LokaaV
• oh : LokaaV
• a : LokaaV

@[instance_reducible]

instance AksenovaEtAl2024.instDecidableEqLokaaV : DecidableEq LokaaV

Equations

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

@[instance_reducible]

instance AksenovaEtAl2024.instFintypeLokaaV : Fintype LokaaV

Equations

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

def AksenovaEtAl2024.instReprLokaaV.repr : LokaaV → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance AksenovaEtAl2024.instReprLokaaV : Repr LokaaV

Equations

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

def AksenovaEtAl2024.LokaaV.tense : LokaaV → Bool

Equations

• AksenovaEtAl2024.LokaaV.e.tense = true
• AksenovaEtAl2024.LokaaV.o.tense = true
• AksenovaEtAl2024.LokaaV.schwa.tense = true
• AksenovaEtAl2024.LokaaV.eh.tense = false
• AksenovaEtAl2024.LokaaV.oh.tense = false
• AksenovaEtAl2024.LokaaV.a.tense = false

def AksenovaEtAl2024.LokaaV.ofChar : Char → Option LokaaV

Akinlabi's transcription carries tone as a precomposed accent on e, o, a and as a combining mark after ɛ, ɔ, ə. High vowels are off the tier.

Equations

• AksenovaEtAl2024.LokaaV.ofChar 'ɛ' = some AksenovaEtAl2024.LokaaV.eh
• AksenovaEtAl2024.LokaaV.ofChar 'ɔ' = some AksenovaEtAl2024.LokaaV.oh
• AksenovaEtAl2024.LokaaV.ofChar 'ə' = some AksenovaEtAl2024.LokaaV.schwa
• AksenovaEtAl2024.LokaaV.ofChar 'e' = some AksenovaEtAl2024.LokaaV.e
• AksenovaEtAl2024.LokaaV.ofChar 'è' = some AksenovaEtAl2024.LokaaV.e
• AksenovaEtAl2024.LokaaV.ofChar 'é' = some AksenovaEtAl2024.LokaaV.e
• AksenovaEtAl2024.LokaaV.ofChar 'o' = some AksenovaEtAl2024.LokaaV.o
• AksenovaEtAl2024.LokaaV.ofChar 'ò' = some AksenovaEtAl2024.LokaaV.o
• AksenovaEtAl2024.LokaaV.ofChar 'ó' = some AksenovaEtAl2024.LokaaV.o
• AksenovaEtAl2024.LokaaV.ofChar 'a' = some AksenovaEtAl2024.LokaaV.a
• AksenovaEtAl2024.LokaaV.ofChar 'à' = some AksenovaEtAl2024.LokaaV.a
• AksenovaEtAl2024.LokaaV.ofChar 'á' = some AksenovaEtAl2024.LokaaV.a
• AksenovaEtAl2024.LokaaV.ofChar x✝ = none

def AksenovaEtAl2024.lokaaBanned (x y : LokaaV) : Prop

H_ATR bans tier-adjacent vowels disagreeing in tenseness.

Equations

• AksenovaEtAl2024.lokaaBanned x y = (x.tense ≠ y.tense)

@[instance_reducible]

instance AksenovaEtAl2024.instDecidableRelLokaaVLokaaBanned : DecidableRel lokaaBanned

Equations

• AksenovaEtAl2024.instDecidableRelLokaaVLokaaBanned x✝¹ x✝ = id inferInstance

@[reducible, inline]

abbrev AksenovaEtAl2024.lokaa : Subregular.TierStrictlyLocalGrammar 2 (Option LokaaV)

Equations

• AksenovaEtAl2024.lokaa = AksenovaEtAl2024.tierGrammar AksenovaEtAl2024.lokaaBanned

theorem AksenovaEtAl2024.lokaa_rows : (∀ f ∈ Forms.all, f.languageId = "loka1252" → read LokaaV.ofChar f.form.toList ∈ lokaa.language) ∧ ∀ f ∈ Forms.marked, f.languageId = "loka1252" → read LokaaV.ofChar f.form.toList ∉ lokaa.language

The (3) forms are accepted and their starred counterparts rejected.

theorem AksenovaEtAl2024.lokaa_not_isStrictlyLocal (k : ℕ) : ¬lokaa.language.IsStrictlyLocal k

No strictly local grammar captures Lokaa harmony (§34.2.1). The vowels e and o agree across any stretch of transparent material, as do ɛ and ɔ, but e and ɔ do not.

def AksenovaEtAl2024.lokaaSP : StrictlyPiecewiseGrammar (Option LokaaV)

The SP₂ grammar of Table 34.1 bans two non-high vowels disagreeing in tenseness, however far apart.

Equations

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

theorem AksenovaEtAl2024.lokaa_language_eq_sp : lokaa.language = StrictlyPiecewiseGrammar.language 2 lokaaSP

The TSL₂ grammar of Table 34.2 and the SP₂ grammar of Table 34.1 generate one language.

Kirghiz ((5), Table 34.3): fronting and rounding on one tier

inductive AksenovaEtAl2024.TurkicV : Type

The tier T = {a, ɨ, e, i, o, ö, u, ü} of Kirghiz and Yakut; ih = ɨ, oe = ö, ue = ü.

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

@[instance_reducible]

instance AksenovaEtAl2024.instDecidableEqTurkicV : DecidableEq TurkicV

Equations

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

@[instance_reducible]

instance AksenovaEtAl2024.instFintypeTurkicV : Fintype TurkicV

Equations

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

def AksenovaEtAl2024.instReprTurkicV.repr : TurkicV → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance AksenovaEtAl2024.instReprTurkicV : Repr TurkicV

Equations

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

def AksenovaEtAl2024.TurkicV.front : TurkicV → Bool

Equations

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

def AksenovaEtAl2024.TurkicV.round : TurkicV → Bool

Equations

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

def AksenovaEtAl2024.TurkicV.high : TurkicV → Bool

Equations

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

def AksenovaEtAl2024.TurkicV.ofChar : Char → Option TurkicV

Equations

• AksenovaEtAl2024.TurkicV.ofChar 'a' = some AksenovaEtAl2024.TurkicV.a
• AksenovaEtAl2024.TurkicV.ofChar 'ɨ' = some AksenovaEtAl2024.TurkicV.ih
• AksenovaEtAl2024.TurkicV.ofChar 'e' = some AksenovaEtAl2024.TurkicV.e
• AksenovaEtAl2024.TurkicV.ofChar 'i' = some AksenovaEtAl2024.TurkicV.i
• AksenovaEtAl2024.TurkicV.ofChar 'o' = some AksenovaEtAl2024.TurkicV.o
• AksenovaEtAl2024.TurkicV.ofChar 'ö' = some AksenovaEtAl2024.TurkicV.oe
• AksenovaEtAl2024.TurkicV.ofChar 'u' = some AksenovaEtAl2024.TurkicV.u
• AksenovaEtAl2024.TurkicV.ofChar 'ü' = some AksenovaEtAl2024.TurkicV.ue
• AksenovaEtAl2024.TurkicV.ofChar x✝ = none

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

H_front ∪ H_round bans a bigram disagreeing in fronting or in rounding.

Equations

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

@[instance_reducible]

instance AksenovaEtAl2024.instDecidableRelTurkicVKirghizBanned : DecidableRel kirghizBanned

Equations

• AksenovaEtAl2024.instDecidableRelTurkicVKirghizBanned x✝¹ x✝ = id inferInstance

@[reducible, inline]

abbrev AksenovaEtAl2024.kirghiz : Subregular.TierStrictlyLocalGrammar 2 (Option TurkicV)

Equations

• AksenovaEtAl2024.kirghiz = AksenovaEtAl2024.tierGrammar AksenovaEtAl2024.kirghizBanned

theorem AksenovaEtAl2024.kirghiz_rows : (∀ f ∈ Forms.all, f.languageId = "kirg1245" → read TurkicV.ofChar f.form.toList ∈ kirghiz.language) ∧ ∀ f ∈ Forms.marked, f.languageId = "kirg1245" → read TurkicV.ofChar f.form.toList ∉ kirghiz.language

The (5) forms are accepted and the starred forms of Figure 34.3 rejected.

def AksenovaEtAl2024.kirghizFront : Phonology.Harmony.Pattern (Option TurkicV) Bool

In Kirghiz frontness harmony every vowel participates.

Equations

• AksenovaEtAl2024.kirghizFront = { value := Option.map AksenovaEtAl2024.TurkicV.front, participation := AksenovaEtAl2024.allParticipate }

def AksenovaEtAl2024.kirghizRound : Phonology.Harmony.Pattern (Option TurkicV) Bool

Kirghiz rounding harmony, with the same undergoers.

Equations

• AksenovaEtAl2024.kirghizRound = { value := Option.map AksenovaEtAl2024.TurkicV.round, participation := AksenovaEtAl2024.allParticipate }

theorem AksenovaEtAl2024.kirghiz_language : kirghiz.language = {w : List (Option TurkicV) | kirghizFront.Harmonic w ∧ kirghizRound.Harmonic w}

The printed grammar is fronting harmony and rounding harmony on one tier.

theorem AksenovaEtAl2024.kirghiz_isStrictlyPiecewise : kirghiz.language.IsStrictlyPiecewise 2

Without blocking, Kirghiz harmony is strictly 2-piecewise as well.

Buryat ((9), Table 34.4): high vowels block rounding

inductive AksenovaEtAl2024.BuryatV : Type

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

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

@[instance_reducible]

instance AksenovaEtAl2024.instDecidableEqBuryatV : DecidableEq BuryatV

Equations

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

@[instance_reducible]

instance AksenovaEtAl2024.instFintypeBuryatV : Fintype BuryatV

Equations

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

@[instance_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.BuryatV.ofChar : Char → Option BuryatV

Equations

• AksenovaEtAl2024.BuryatV.ofChar 'a' = some AksenovaEtAl2024.BuryatV.a
• AksenovaEtAl2024.BuryatV.ofChar 'e' = some AksenovaEtAl2024.BuryatV.e
• AksenovaEtAl2024.BuryatV.ofChar 'ɔ' = some AksenovaEtAl2024.BuryatV.oh
• AksenovaEtAl2024.BuryatV.ofChar 'o' = some AksenovaEtAl2024.BuryatV.o
• AksenovaEtAl2024.BuryatV.ofChar 'ʊ' = some AksenovaEtAl2024.BuryatV.uh
• AksenovaEtAl2024.BuryatV.ofChar 'u' = some AksenovaEtAl2024.BuryatV.u
• AksenovaEtAl2024.BuryatV.ofChar x✝ = none

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

H_ATR ∪ H_r1 ∪ H_r2 bans a bigram disagreeing in ATR, two non-high vowels disagreeing in rounding, and a rounded non-high vowel after a high one.

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)

@[instance_reducible]

instance AksenovaEtAl2024.instDecidableRelBuryatVBuryatBanned : DecidableRel buryatBanned

Equations

• AksenovaEtAl2024.instDecidableRelBuryatVBuryatBanned x✝¹ x✝ = id inferInstance

@[reducible, inline]

abbrev AksenovaEtAl2024.buryat : Subregular.TierStrictlyLocalGrammar 2 (Option BuryatV)

Equations

• AksenovaEtAl2024.buryat = AksenovaEtAl2024.tierGrammar AksenovaEtAl2024.buryatBanned

theorem AksenovaEtAl2024.buryat_rows : (∀ f ∈ Forms.all, f.languageId = "russ1264" → read BuryatV.ofChar f.form.toList ∈ buryat.language) ∧ ∀ f ∈ Forms.marked, f.languageId = "russ1264" → read BuryatV.ofChar f.form.toList ∉ buryat.language

The (9) forms are accepted, ɔr-ʊːl-aːd because the high causative blocks rounding, and their starred counterparts rejected.

def AksenovaEtAl2024.buryatATR : Phonology.Harmony.Pattern (Option BuryatV) Bool

In Buryat ATR harmony every tier vowel participates.

Equations

• AksenovaEtAl2024.buryatATR = { value := Option.map AksenovaEtAl2024.BuryatV.tense, participation := AksenovaEtAl2024.allParticipate }

def AksenovaEtAl2024.buryatRound : Phonology.Harmony.Pattern (Option BuryatV) Bool

In Buryat rounding harmony high vowels are opaque, imposing unroundedness on what follows.

Equations

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

theorem AksenovaEtAl2024.buryat_language : buryat.language = {w : List (Option BuryatV) | buryatATR.Harmonic w ∧ buryatRound.Harmonic w}

The printed grammar is ATR harmony and rounding harmony with opaque high vowels, on one tier.

theorem AksenovaEtAl2024.buryat_not_isStrictlyPiecewise (k : ℕ) : ¬buryat.language.IsStrictlyPiecewise k

Blocking is strictly piecewise at no width (§34.2.2). Deleting the blocking causative vowel of ɔr-ʊːl-aːd (9b) leaves the starred *ɔr-aːd of (9a).

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

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

H_front ∪ H_r1 ∪ H_r2 ∪ H_r3 bans a bigram disagreeing in fronting, two high vowels disagreeing in rounding, a rounded non-high vowel after a high one, and a non-high vowel followed by one disagreeing in rounding.

Equations

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

@[instance_reducible]

instance AksenovaEtAl2024.instDecidableRelTurkicVYakutBanned : DecidableRel yakutBanned

Equations

• AksenovaEtAl2024.instDecidableRelTurkicVYakutBanned x✝¹ x✝ = id inferInstance

@[reducible, inline]

abbrev AksenovaEtAl2024.yakut : Subregular.TierStrictlyLocalGrammar 2 (Option TurkicV)

Equations

• AksenovaEtAl2024.yakut = AksenovaEtAl2024.tierGrammar AksenovaEtAl2024.yakutBanned

theorem AksenovaEtAl2024.yakut_rows : (∀ f ∈ Forms.all, f.languageId = "yaku1245" → read TurkicV.ofChar f.form.toList ∈ yakut.language) ∧ ∀ f ∈ Forms.marked, f.languageId = "yaku1245" → read TurkicV.ofChar f.form.toList ∉ yakut.language

theorem AksenovaEtAl2024.yakut_not_isStrictlyPiecewise (k : ℕ) : ¬yakut.language.IsStrictlyPiecewise k

Harmonizing blockers block (§34.2.2). Deleting the high vowel of ojum-lar (14g) leaves its low vowels disagreeing in rounding, *oa.

def AksenovaEtAl2024.yakutFront : Phonology.Harmony.Pattern (Option TurkicV) Bool

In Yakut fronting harmony every vowel participates.

Equations

• AksenovaEtAl2024.yakutFront = { value := Option.map AksenovaEtAl2024.TurkicV.front, participation := AksenovaEtAl2024.allParticipate }

theorem AksenovaEtAl2024.yakut_rounding_not_pattern {W : Type u_1} (q : Phonology.Harmony.Pattern (Option TurkicV) W) : yakut.language ≠ {w : List (Option TurkicV) | yakutFront.Harmonic w ∧ q.Harmonic w}

Yakut's rounding is no segment-level pattern beside its fronting harmony, whatever its values, tier, blockers, and icy targets. The tier bigram u a is licit and a u is not, so a would have to be opaque or u an icy target, and either would license *oa or *uo.

Kikongo ((16), (18), Tables 34.6–34.7): two disjoint tiers

inductive AksenovaEtAl2024.KikongoSeg : Type

The Kikongo tier symbols are the vowels T_v = {e, o, i, u} and T_n = {n, m, d, l}.

• e : KikongoSeg
• o : KikongoSeg
• i : KikongoSeg
• u : KikongoSeg
• n : KikongoSeg
• m : KikongoSeg
• d : KikongoSeg
• l : KikongoSeg

@[instance_reducible]

instance AksenovaEtAl2024.instDecidableEqKikongoSeg : DecidableEq KikongoSeg

Equations

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

@[instance_reducible]

instance AksenovaEtAl2024.instFintypeKikongoSeg : Fintype KikongoSeg

Equations

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

def AksenovaEtAl2024.instReprKikongoSeg.repr : KikongoSeg → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance AksenovaEtAl2024.instReprKikongoSeg : Repr KikongoSeg

Equations

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

def AksenovaEtAl2024.KikongoSeg.isVowel : KikongoSeg → Bool

Equations

• AksenovaEtAl2024.KikongoSeg.e.isVowel = true
• AksenovaEtAl2024.KikongoSeg.o.isVowel = true
• AksenovaEtAl2024.KikongoSeg.i.isVowel = true
• AksenovaEtAl2024.KikongoSeg.u.isVowel = true
• x✝.isVowel = false

def AksenovaEtAl2024.KikongoSeg.high : KikongoSeg → Bool

Equations

• AksenovaEtAl2024.KikongoSeg.i.high = true
• AksenovaEtAl2024.KikongoSeg.u.high = true
• x✝.high = false

def AksenovaEtAl2024.KikongoSeg.isNasal : KikongoSeg → Bool

Equations

• AksenovaEtAl2024.KikongoSeg.n.isNasal = true
• AksenovaEtAl2024.KikongoSeg.m.isNasal = true
• x✝.isNasal = false

def AksenovaEtAl2024.KikongoSeg.ofChar : Char → Option KikongoSeg

Equations

• AksenovaEtAl2024.KikongoSeg.ofChar 'e' = some AksenovaEtAl2024.KikongoSeg.e
• AksenovaEtAl2024.KikongoSeg.ofChar 'o' = some AksenovaEtAl2024.KikongoSeg.o
• AksenovaEtAl2024.KikongoSeg.ofChar 'i' = some AksenovaEtAl2024.KikongoSeg.i
• AksenovaEtAl2024.KikongoSeg.ofChar 'u' = some AksenovaEtAl2024.KikongoSeg.u
• AksenovaEtAl2024.KikongoSeg.ofChar 'n' = some AksenovaEtAl2024.KikongoSeg.n
• AksenovaEtAl2024.KikongoSeg.ofChar 'm' = some AksenovaEtAl2024.KikongoSeg.m
• AksenovaEtAl2024.KikongoSeg.ofChar 'd' = some AksenovaEtAl2024.KikongoSeg.d
• AksenovaEtAl2024.KikongoSeg.ofChar 'l' = some AksenovaEtAl2024.KikongoSeg.l
• AksenovaEtAl2024.KikongoSeg.ofChar x✝ = none

def AksenovaEtAl2024.KikongoSeg.parse : List Char → List KikongoSeg

A printed form read onto the two tiers, a nasal before a stop read as that stop's prenasalized onset.

Equations

• AksenovaEtAl2024.KikongoSeg.parse ('m' :: 'p' :: rest) = AksenovaEtAl2024.KikongoSeg.parse rest
• AksenovaEtAl2024.KikongoSeg.parse ('m' :: 'b' :: rest) = AksenovaEtAl2024.KikongoSeg.parse rest
• AksenovaEtAl2024.KikongoSeg.parse ('n' :: 'g' :: rest) = AksenovaEtAl2024.KikongoSeg.parse rest
• AksenovaEtAl2024.KikongoSeg.parse (c :: rest) = (AksenovaEtAl2024.KikongoSeg.ofChar c).toList ++ AksenovaEtAl2024.KikongoSeg.parse rest
• AksenovaEtAl2024.KikongoSeg.parse [] = []

@[reducible, inline]

abbrev AksenovaEtAl2024.kikongoVowelTier (s : KikongoSeg) : Prop

The vowel tier T_v and the nasal tier T_n, which partition the symbols.

Equations

• AksenovaEtAl2024.kikongoVowelTier s = (s.isVowel = true)

@[reducible, inline]

abbrev AksenovaEtAl2024.kikongoNasalTier (s : KikongoSeg) : Prop

Equations

• AksenovaEtAl2024.kikongoNasalTier s = (s.isVowel = false)

@[reducible, inline]

abbrev AksenovaEtAl2024.kikongoVowel : Subregular.TierStrictlyLocalGrammar 2 KikongoSeg

H_v bans tier-adjacent vowels disagreeing in height.

Equations

• AksenovaEtAl2024.kikongoVowel = Subregular.TierStrictlyLocalGrammar.ofForbiddenPairs (fun (x y : AksenovaEtAl2024.KikongoSeg) => x.high ≠ y.high) AksenovaEtAl2024.kikongoVowelTier

@[reducible, inline]

abbrev AksenovaEtAl2024.kikongoNasal : Subregular.TierStrictlyLocalGrammar 2 KikongoSeg

H_n bans d or l after a nasal.

Equations

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

def AksenovaEtAl2024.kikongo : Language KikongoSeg

Kikongo phonotactics conjoins the two harmonies, each on its own tier.

Equations

• AksenovaEtAl2024.kikongo = AksenovaEtAl2024.kikongoVowel.language ⊓ AksenovaEtAl2024.kikongoNasal.language

@[instance_reducible]

instance AksenovaEtAl2024.instDecidablePredListKikongoSegMemLanguageKikongo : DecidablePred fun (x : List KikongoSeg) => x ∈ kikongo

Equations

• AksenovaEtAl2024.instDecidablePredListKikongoSegMemLanguageKikongo w = instDecidableAnd

theorem AksenovaEtAl2024.kikongo_rows : (∀ f ∈ Forms.all, f.languageId = "koon1247" → KikongoSeg.parse f.form.toList ∈ kikongo) ∧ ∀ f ∈ Forms.marked, f.languageId = "koon1247" → KikongoSeg.parse f.form.toList ∉ kikongo

The (16) and (18) forms are accepted and the starred forms of Figure 34.6 rejected.

theorem AksenovaEtAl2024.kikongo_not_isTierStrictlyLocal (k : ℕ) : ¬Language.IsTierStrictlyLocal k kikongo

No single tier carries Kikongo's two harmonies (§34.3.3), by [Lam23]'s method. Deleting e from ie changes membership, so a tier must hold e, and then suffix substitution across a stretch of es carries n … n and l … l to the ill-formed n … l.