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 needs the tier because no strictly local window bounds the transparent material; Kirghiz, Buryat, and Yakut double harmonies each fit on a single tier, with blocking (Buryat's high vowels) and configuration-dependent blocking (Yakut's low vowels) both mere bigram bans; Kikongo's vowel and nasal harmonies need two tiers, which are disjoint. Of the four relations two tier alphabets can stand in, only same, embedded, and disjoint are attested.

This file states each printed grammar (Tables 34.2–34.7) as a TierStrictlyLocalGrammar.ofForbiddenPairs over the paper's tier alphabet, reads the paper's forms into that alphabet, and checks the forms and their starred counterparts against it (lokaa_rows, kirghiz_rows, buryat_rows, yakut_rows, kikongo_rows). The Pattern theorems say which grammars segment-level participation reproduces: Kirghiz and Buryat are conjunctions of two patterns (kirghiz_two_patterns, buryat_expressible), Buryat's blocking is asymmetric (buryat_not_symmetric), and Yakut's is left open. tierRelation computes the §34.3.4 typology (kikongo_disjoint_tiers).

References

• [aksenova-rawski-graf-heinz-2024]

def AksenovaEtAl2024.tierOf {V : Type} (ofChar : Char → Option V) (s : String) : List V

The tier of a printed form: its symbols read into the tier alphabet, everything else — consonants, transparent vowels, length and tone marks — dropped.

Equations

• AksenovaEtAl2024.tierOf ofChar s = List.filterMap ofChar s.toList

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: tone is a precomposed accent on e, o, a and 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: 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 y = id inferInstance

def AksenovaEtAl2024.lokaa : Subregular.TierStrictlyLocalGrammar 2 LokaaV

Equations

• AksenovaEtAl2024.lokaa = Subregular.TierStrictlyLocalGrammar.ofForbiddenPairs AksenovaEtAl2024.lokaaBanned fun (x : AksenovaEtAl2024.LokaaV) => True

theorem AksenovaEtAl2024.lokaa_rows (row : Data.Examples.LinguisticExample) : row ∈ Examples.all → row.language = "loka1252" → tierOf LokaaV.ofChar row.primaryText ∈ lokaa.language ∧ ∀ alt ∈ row.alternatives, tierOf LokaaV.ofChar alt.1 ∉ lokaa.language

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

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

inductive AksenovaEtAl2024.KirghizV : Type

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

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

@[instance_reducible]

instance AksenovaEtAl2024.instDecidableEqKirghizV : DecidableEq KirghizV

Equations

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

@[instance_reducible]

instance AksenovaEtAl2024.instFintypeKirghizV : Fintype KirghizV

Equations

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

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

Equations

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

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

H_front ∪ H_round: the bigram disagrees in fronting or in rounding.

Equations

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

@[instance_reducible]

instance AksenovaEtAl2024.instDecidableRelKirghizVKirghizBanned : DecidableRel kirghizBanned

Equations

• AksenovaEtAl2024.instDecidableRelKirghizVKirghizBanned x y = id inferInstance

def AksenovaEtAl2024.kirghiz : Subregular.TierStrictlyLocalGrammar 2 KirghizV

Equations

• AksenovaEtAl2024.kirghiz = Subregular.TierStrictlyLocalGrammar.ofForbiddenPairs AksenovaEtAl2024.kirghizBanned fun (x : AksenovaEtAl2024.KirghizV) => True

theorem AksenovaEtAl2024.kirghiz_rows (row : Data.Examples.LinguisticExample) : row ∈ Examples.all → row.language = "kirg1245" → tierOf KirghizV.ofChar row.primaryText ∈ kirghiz.language ∧ ∀ alt ∈ row.alternatives, tierOf KirghizV.ofChar alt.1 ∉ kirghiz.language

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

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

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)

The printed grammar is the conjunction of the two patterns' compatibilities.

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: the bigram disagrees in ATR; or its non-high vowels disagree in rounding; or a rounded non-high vowel follows a high vowel.

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 y = id inferInstance

def AksenovaEtAl2024.buryat : Subregular.TierStrictlyLocalGrammar 2 BuryatV

Equations

• AksenovaEtAl2024.buryat = Subregular.TierStrictlyLocalGrammar.ofForbiddenPairs AksenovaEtAl2024.buryatBanned fun (x : AksenovaEtAl2024.BuryatV) => True

theorem AksenovaEtAl2024.buryat_rows (row : Data.Examples.LinguisticExample) : row ∈ Examples.all → row.language = "russ1264" → tierOf BuryatV.ofChar row.primaryText ∈ buryat.language ∧ ∀ alt ∈ row.alternatives, tierOf BuryatV.ofChar alt.1 ∉ buryat.language

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

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

Blocking is directional: *ʊɔ is banned but ɔʊ licensed.

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

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

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_expressible (x y : BuryatV) : buryatBanned x y ↔ ¬(buryatATR.Compatible x y ∧ buryatRound.Compatible x y)

With opaque blockers the printed grammar is the conjunction of the two patterns.

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

inductive AksenovaEtAl2024.YakutV : Type

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

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

@[instance_reducible]

instance AksenovaEtAl2024.instDecidableEqYakutV : DecidableEq YakutV

Equations

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

@[instance_reducible]

instance AksenovaEtAl2024.instFintypeYakutV : Fintype YakutV

Equations

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

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

Equations

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

@[instance_reducible]

instance AksenovaEtAl2024.instReprYakutV : Repr YakutV

Equations

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

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.YakutV.ofChar : Char → Option YakutV

Equations

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

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

H_front ∪ H_r1 ∪ H_r2 ∪ H_r3: the bigram disagrees in fronting; or its high vowels disagree in rounding; or a rounded non-high vowel follows a high vowel; or a non-high vowel is followed by a vowel disagreeing in rounding. (The printed H_r2 lists *üö twice and omits *üo, which H_front bans anyway.)

Equations

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

@[instance_reducible]

instance AksenovaEtAl2024.instDecidableRelYakutVYakutBanned : DecidableRel yakutBanned

Equations

• AksenovaEtAl2024.instDecidableRelYakutVYakutBanned x y = id inferInstance

def AksenovaEtAl2024.yakut : Subregular.TierStrictlyLocalGrammar 2 YakutV

Equations

• AksenovaEtAl2024.yakut = Subregular.TierStrictlyLocalGrammar.ofForbiddenPairs AksenovaEtAl2024.yakutBanned fun (x : AksenovaEtAl2024.YakutV) => True

theorem AksenovaEtAl2024.yakut_rows (row : Data.Examples.LinguisticExample) : row ∈ Examples.all → row.language = "yaku1245" → tierOf YakutV.ofChar row.primaryText ∈ yakut.language ∧ ∀ alt ∈ row.alternatives, tierOf YakutV.ofChar alt.1 ∉ yakut.language

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

Low vowels harmonize but block: rounding passes from o to u, not from u to o.

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

inductive AksenovaEtAl2024.KikongoSeg : Type

The Kikongo tier symbols: 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.

@[instance_reducible]

instance AksenovaEtAl2024.instReprKikongoSeg : Repr KikongoSeg

Equations

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

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

Equations

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

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 into the tier symbols. A nasal before a stop is the prenasalized onset of that stop, not a tier nasal: read with m projected, Table 34.7 would ban the paper's own -somp-el-, -tomb-ol-, and -lemb-ol- (*ml).

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.

Equations

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

@[reducible, inline]

abbrev AksenovaEtAl2024.kikongoNasalTier (s : KikongoSeg) : Prop

Equations

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

def AksenovaEtAl2024.kikongoVowel : Subregular.TierStrictlyLocalGrammar 2 KikongoSeg

H_v: tier-adjacent vowels disagreeing in height.

Equations

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

def AksenovaEtAl2024.kikongoNasal : Subregular.TierStrictlyLocalGrammar 2 KikongoSeg

H_n: d or l after a nasal.

Equations

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

theorem AksenovaEtAl2024.kikongo_rows (row : Data.Examples.LinguisticExample) : row ∈ Examples.all → row.language = "koon1247" → KikongoSeg.parse row.primaryText.toList ∈ kikongoVowel.language ∧ KikongoSeg.parse row.primaryText.toList ∈ kikongoNasal.language

Every (16) and (18) form passes both grammars on its own tier.

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

Two tier alphabets are the same, embedded, disjoint, or partially overlapping; the last is unattested, a tendency the chapter reports would exclude 95% of the possible tier organizations of a ten-element alphabet.

inductive AksenovaEtAl2024.TierRelation : Type

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

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

@[instance_reducible]

instance AksenovaEtAl2024.instDecidableEqTierRelation : DecidableEq TierRelation

Equations

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

@[instance_reducible]

instance AksenovaEtAl2024.instReprTierRelation : Repr TierRelation

Equations

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

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

Equations

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

def AksenovaEtAl2024.tierRelation {α : Type} [Fintype α] [DecidableEq α] (p q : α → Prop) [DecidablePred p] [DecidablePred q] : TierRelation

The relation between two tiers over a finite alphabet.

Equations

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

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

Kirghiz and Buryat double harmonies are single-tier — Table 34.8's S rows.

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

theorem AksenovaEtAl2024.kikongo_disjoint_tiers : tierRelation kikongoVowelTier kikongoNasalTier = TierRelation.disjoint

Kikongo's vowel and nasal tiers are disjoint — Table 34.8's D row.