Meinhardt, Mai, Baković and McCollum (2024): Weak Determinism and ATR Harmony

This file formalizes the Maasai case of Meinhardt, Mai, Baković and McCollum, who tighten the weakly deterministic function class of Heinz and Lai by an explicit interaction condition. Bidirectional iterative ATR harmony in Maasai is attested and weakly deterministic, an unbounded semiambient pattern in which every target depends on one side at a time, so its two contradirectional subsequential passes do not interact; Turkana, identical but for exceptionally dominant retracted suffix vowels, is attested and non-deterministic, an unbounded circumambient pattern in which some targets depend on both sides at once. Dominance is an underlying specification of the spreading value on vowels, carried by roots and suffixes alike. The rightward spreading pass is output-strictly-local after Chandlee, Eyraud and Heinz, the bidirectional dominant–recessive map is weakly deterministic through a non-interacting bimachine (maasai_isNonInteractingBimachineComputable) with two-sided unbounded dependence (maasai_twoSidedUnboundedDependence) but without requiring both sides at once (maasai_not_requiresBothSides), the boundary the paper draws. Tutrugbu's conditional blocking, the paper's (3), and unbounded tonal plateauing, its (2), lie on the other side: each requires both sides, so neither is semiambient (tutrugbu_not_semiambient) or computed by a non-interacting bimachine. Plateauing is nonetheless weakly deterministic in Heinz and Lai's sense, by the phonotactic code of §5.2, so their class is not contained in the paper's (exists_isWeaklyDeterministic_not_isNonInteractingBimachineComputable).

Implementation notes

The alphabet has four symbols carrying the dominant–recessive distinction; the bidirectional map is modelled directly, raising a recessive vowel when a dominant one occurs anywhere, rather than as a two-pass composition, and the opaque low vowel, the re-paired low vowel, glide effects, and the Turkana half of the paper are not represented.

Weak determinism is rendered by the change-based reading of Def. 5: a non-interacting bimachine licenses every change by one side alone (IsNonInteractingBimachineComputable). Def. 6 read literally asks the same of unchanged cells, and the Maasai bimachine of Fig. 8 fails it: at a recessive vowel with q1 on both sides the output is the vowel itself, and moving either state alone to q2 changes it.

References

• [MMBMcC24]
• [HL13]
• [CEH15]
• [Wil06]
• [McCBMM20]
• [LOHS19]

inductive MeinhardtEtAl2024.Seg : Type

A minimal alphabet captures the dominance-vs-recessive distinction that drives Maasai ATR harmony (p. 1203). Four symbols stand in for the relevant phonological contrasts.

• recL — a recessive [-ATR] vowel (e.g., /ɪ/, /ʊ/), surfacing as [-ATR] absent harmony and raising to [+ATR] under spread.
• recH — a recessive vowel surfacing [+ATR] (e.g., /i/, /u/), the raised form of recL, and transparent to further spread.
• dom — a dominant vowel, underlyingly specified [+ATR] and the trigger of spreading (the paper's load-bearing distinction).
• a — the opaque /a/. Blocks spread.

Consonants are omitted as they are transparent to the harmony.

• recL : Seg
• recH : Seg
• dom : Seg
• a : Seg

@[instance_reducible]

instance MeinhardtEtAl2024.instDecidableEqSeg : DecidableEq Seg

Equations

• MeinhardtEtAl2024.instDecidableEqSeg x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def MeinhardtEtAl2024.instReprSeg.repr : Seg → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• MeinhardtEtAl2024.instReprSeg.repr MeinhardtEtAl2024.Seg.dom prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "MeinhardtEtAl2024.Seg.dom")).group prec✝
• MeinhardtEtAl2024.instReprSeg.repr MeinhardtEtAl2024.Seg.a prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "MeinhardtEtAl2024.Seg.a")).group prec✝

@[instance_reducible]

instance MeinhardtEtAl2024.instReprSeg : Repr Seg

Equations

• MeinhardtEtAl2024.instReprSeg = { reprPrec := MeinhardtEtAl2024.instReprSeg.repr }

@[instance_reducible]

instance MeinhardtEtAl2024.instFintypeSeg : Fintype Seg

Equations

• MeinhardtEtAl2024.instFintypeSeg = { elems := {MeinhardtEtAl2024.Seg.recL, MeinhardtEtAl2024.Seg.recH, MeinhardtEtAl2024.Seg.dom, MeinhardtEtAl2024.Seg.a}, complete := ⋯ }

def MeinhardtEtAl2024.Seg.isPlusATR : Seg → Bool

Whether the segment is a [+ATR] vowel after surface realisation, which holds of dom and recH and fails of recL (until raised by spread) and of a.

Equations

• MeinhardtEtAl2024.Seg.recH.isPlusATR = true
• MeinhardtEtAl2024.Seg.dom.isPlusATR = true
• x✝.isPlusATR = false

def MeinhardtEtAl2024.Seg.raise : Seg → Seg

The surface form of a segment under spreading [+ATR], which raises recessive [-ATR] vowels and passes everything else through unchanged, including the opaque /a/.

Equations

• MeinhardtEtAl2024.Seg.recL.raise = MeinhardtEtAl2024.Seg.recH
• x✝.raise = x✝

def MeinhardtEtAl2024.rightwardATR_osl : Subregular.OSLRule 2 Seg Seg

OSL rule encoding rightward [+ATR] spreading from a dominant root.

With k = 2 the output decision at each position depends on the single immediately preceding output symbol, as in the canonical OSL fragment of phonological maps of Chandlee, Eyraud and Heinz. The rule emits as follows.

• Current input is dom → emit recH (dominant always surfaces as [+ATR]).
• Current input is a → emit a (opaque, blocks spread; the next position's output context will be a, not a +ATR vowel).
• Current input is recH → emit recH (already +ATR, passes through).
• Current input is recL and previous output was recH → emit recH (spread continues).
• Current input is recL otherwise → emit recL (no spread to here).

Single-direction iterative spreading patterns are OSL but not ISL, after Chandlee, Eyraud and Heinz, because the output decision depends on the output history (how far spread has propagated) rather than the input history alone (rightwardATR_osl_not_isLeftInputStrictlyLocal).

Equations

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

theorem MeinhardtEtAl2024.rightwardATR_osl_isLeftOutputStrictlyLocal : Subregular.IsLeftOutputStrictlyLocal 2 rightwardATR_osl.apply

Rightward [+ATR] spreading is Left-Output-Strictly-Local, witnessed by rightwardATR_osl.

theorem MeinhardtEtAl2024.rightwardATR_osl_not_isLeftInputStrictlyLocal (k : ℕ) : ¬Subregular.IsLeftInputStrictlyLocal k rightwardATR_osl.apply

Rightward [+ATR] spreading is not Input-Strictly-Local for any window, since a dominant vowel followed by k - 1 recessive ones and k recessive vowels end in the same k - 1 input segments while a further recessive vowel raises only after the first.

theorem MeinhardtEtAl2024.rightwardATR_osl_isLeftSubsequential : IsLeftSubsequential rightwardATR_osl.apply

Rightward [+ATR] spreading is also Left-Subsequential, through OSL ⊆ Left-Subsequential (IsLeftOutputStrictlyLocal.isLeftSubsequential).

Bidirectional Maasai harmony — weakly deterministic (faithful)

Maasai dominant-recessive ATR harmony spreads [+ATR] from a dominant root to recessive vowels on both sides. Modelled here in its non-opaque core: a recessive recL raises to recH iff the word contains a dominant vowel anywhere (maasai). This is a union of two independent spreading passes, so it is weakly deterministic (the paper's unbounded semiambient): the bimachine maasaiBM tracks a dominant seen on each side and its output is literally a unite of one-sided rules. A recessive's surface ATR still co-varies with information unboundedly far on either side, so maasai satisfies TwoSidedUnboundedDependence — as does Tutrugbu. The contrast is exactly the WD/ND boundary the paper draws: only Tutrugbu is circumambient, needing both sides at once (RequiresBothSides), which Maasai never does.

def MeinhardtEtAl2024.hasDom (xs : List Seg) : Bool

The word contains a dominant trigger.

Equations

• MeinhardtEtAl2024.hasDom xs = xs.any fun (x : MeinhardtEtAl2024.Seg) => x == MeinhardtEtAl2024.Seg.dom

def MeinhardtEtAl2024.maasai (xs : List Seg) : List Seg

Bidirectional dominant-recessive harmony in its non-opaque core, under which a recessive raises iff the word has a dominant trigger anywhere.

Equations

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

def MeinhardtEtAl2024.maasaiBM : Bimachine Bool Bool Seg Seg

The non-interacting bimachine, whose state on each side tracks a dominant seen on that side, raising a recessive if either side has one as a union of one-sided rules.

Equations

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

theorem MeinhardtEtAl2024.maasaiBM_isNonInteracting : maasaiBM.IsNonInteracting

maasaiBM's cell output is a unite of one-sided raise-rules.

theorem MeinhardtEtAl2024.maasaiBM_run : maasaiBM.run = maasai

The bimachine computes maasai.

theorem MeinhardtEtAl2024.maasai_isNonInteractingBimachineComputable : IsNonInteractingBimachineComputable maasai

Maasai ATR harmony is weakly deterministic in the paper's sense, the bidirectional dominant-recessive spread being a non-interacting bimachine.

theorem MeinhardtEtAl2024.maasai_twoSidedUnboundedDependence : TwoSidedUnboundedDependence maasai

Maasai has two-sided unbounded dependence — at every distance, a medial recessive's ATR flips under a dominant placed far to the left or far to the right, each side alone sufficing. Tutrugbu satisfies this too (McCollumEtAl2020.tutrugbu_twoSidedUnboundedDependence), but Maasai does not RequiresBothSides, so it stays weakly deterministic. The paper's positive classification of Maasai as unbounded semiambient, with every target fixed by information from at most one side, is the stronger claim maasai_semiambient.

theorem MeinhardtEtAl2024.maasai_semiambient : OneSidedChanges maasai

Maasai is semiambient, the paper's positive classification, with every harmonised cell licensed by one side alone, the far dominant that triggers it.

theorem MeinhardtEtAl2024.maasai_not_requiresBothSides : ¬RequiresBothSides maasai

Hence Maasai does not require both sides — it escapes the teeth, unlike Tutrugbu. Covariation (both languages) and interaction (Tutrugbu only) come apart.

theorem MeinhardtEtAl2024.maasai_not_mealyComputable : ¬IsMealyComputable maasai

Maasai ATR harmony is not Mealy-computable, since a Mealy-computable map depends boundedly on the right (IsMealyComputable.boundedDependence_right) and Maasai's bidirectional spread does not (maasai_twoSidedUnboundedDependence).

theorem MeinhardtEtAl2024.maasai_not_leftSubsequential : ¬IsLeftSubsequential maasai

Maasai is not left-subsequential, excluding the block class too, since maasai is length-preserving, so a left-subsequential computer's delay bound would cap its right dependence (IsLeftSubsequential.boundedDependence_right), but the spread's right dependence is unbounded.

Tutrugbu

Tutrugbu's conditional blocking, the paper's (3), is unbounded circumambient (Def. 2). It requires both sides, so some change it makes is licensed by neither side alone and no non-interacting bimachine computes it.

theorem MeinhardtEtAl2024.tutrugbu_not_semiambient : ¬OneSidedChanges McCollumEtAl2020.tutrugbu.map

Tutrugbu ATR harmony is not semiambient (Def. 3), since some change it makes is licensed by neither side alone.

theorem MeinhardtEtAl2024.tutrugbu_not_isNonInteractingBimachineComputable : ¬IsNonInteractingBimachineComputable McCollumEtAl2020.tutrugbu.map

Tutrugbu ATR harmony is computed by no non-interacting bimachine.

Unbounded tonal plateauing

Plateauing, the paper's (2), is unbounded circumambient (Def. 2): it requires both sides, so no non-interacting bimachine computes it. Yet it is weakly deterministic in Heinz and Lai's sense, by the phonotactic code of Lamont, O'Hara and Smith that §5.2 and Fig. 12 take up: their first pass is length- and alphabet-preserving and still tells the second pass what lies beyond its reach.

theorem MeinhardtEtAl2024.utp_not_isNonInteractingBimachineComputable : ¬IsNonInteractingBimachineComputable Tone.utp.map

Unbounded tonal plateauing is not computed by any non-interacting bimachine.

theorem MeinhardtEtAl2024.exists_isWeaklyDeterministic_not_isNonInteractingBimachineComputable : ∃ (f : List Tone.TBU → List Tone.TBU), IsWeaklyDeterministic f ∧ ¬IsNonInteractingBimachineComputable f

Heinz and Lai's weakly deterministic functions are not all computed by non-interacting bimachines.