Meinhardt, Mai, Baković & McCollum (2024): ATR Harmony Subregular Classification

Worked example using the function-level subregular substrate (the subregular function classes) to classify a fragment of Eastern Nilotic ATR harmony per [MMBMcC24].

The paper

[MMBMcC24] (NLLT 42:1191-1232) propose a tightening of the [HL13] Weakly Deterministic (WD) function class. Their thesis:

• Bidirectional iterative ATR harmony in Maasai (Eastern Nilotic) is attested and WD — unbounded semiambient: every target depends on one side at a time (though the side may vary), so its two contradirectional subsequential passes do not interact in the technical sense the paper formalises (§4).
• Turkana, identical to Maasai but for a set of exceptionally dominant [-ATR] suffix vowels, is attested and non-deterministic — unbounded circumambient: some targets depend on both sides at once, so the passes must interact. "The Maasai pattern is weakly deterministic, and the Turkana pattern is not" (end of §2.3): the paper's ND case is attested, not merely the hypothetical sour grapes ([Wil03b]; [Wil06]) it also places above WD.
• The original Heinz-Lai 2013 WD definition was too permissive, admitting some unattested patterns; Meinhardt et al. patch it by formalising the interaction condition explicitly (§4).

Maasai dominant/recessive harmony (paper §3.1, p. 1203)

The empirically critical fact (paper p. 1203): "(non-exceptional) dominant vowels are underlyingly specified for the spreading value of the harmonic feature, [+ATR]" — dominance is an underlying featural specification on vowels, carried by roots and by suffixes alike (the paper shows both root- and suffix-controlled spreading), not a diacritic property of roots. A dominant vowel triggers spreading; recessive vowels harmonise.

The bidirectional Maasai pattern (paper p. 1193, ex 1a):

• (i) Full bidirectional spreading from a dominant root: /kɪ-√ñorr-ʊ/ → [ki-√ñorr-u] '1pl-love-pres' — [+ATR] spreads from the (dominant) root in both directions, raising recessive prefix /ɪ/ to [i] and recessive suffix /ʊ/ to [u].
• (ii) Leftward spread blocked by /a/: /ɪ-√as-ɪʃɔ-re/ → [ɪ-√as-iʃo-re] '2sg-do-intr-appl' — the dominant applied suffix -re triggers leftward [+ATR] spread, raising /ɪʃɔ/ to [iʃo]; the opaque /a/ of the root blocks it, leaving the prefix /ɪ/ unchanged.

What this file does (audit-corrected)

Per CLAUDE.md "stimulus contrasts" discipline for Studies files:

1. Defines a 4-symbol alphabet Seg capturing the dominant/recessive distinction the paper insists is empirically load-bearing — the formaliser-invented alphabet from the previous version of this file (which conflated [+ATR] with the spreading trigger) is replaced.
2. Encodes the rightward [+ATR] spreading half of Maasai harmony as both a SubsequentialTransducer and an OSLRule. Single-direction iterative spreading is Output-Strictly-Local ([CEH15], the result [MMBMcC24] builds on) — the output decision at each position depends on whether the immediately preceding output symbol is +ATR. The OSL classification is tighter than Left-Subsequential and is what the paper actually predicts for the unidirectional pass.
3. Decide-checks input/output examples corresponding to ex 1a-i and ex 1a-ii from the paper (encoded in the toy alphabet).
4. Proves the bidirectional dominant-recessive map maasai is weakly deterministic (maasai_weaklyDeterministic) via a non-interacting bimachine, with two-sided unbounded dependence (maasai_twoSidedUnboundedDependence) — a predicate Tutrugbu also satisfies — while not RequiresBothSides (maasai_not_requiresBothSides). That asymmetry is the WD/ND boundary [MMBMcC24] draws.

What this file does NOT do

• Does not encode the full Maasai/Turkana paradigms — only the minimal pair sufficient to illustrate substrate use. Paper §§3–4 add the re-paired low vowel (raised /A/ surfaces as [o]), opaque /A/ blocking, glides disrupting harmony, and Turkana's exceptionally dominant [-ATR] suffix vowels.
• Does not formalize Turkana — the paper's attested non-deterministic half. Its exceptionally dominant [-ATR] suffixes make the pattern unbounded circumambient, so the RequiresBothSides machinery applies directly; this is the natural next arc.
• Models the bidirectional map directly (maasai: raise a recessive iff a dominant occurs anywhere) rather than as an explicit two-pass composition of a rightward and a leftward transducer, and omits the opaque /a/ blocking — the non-opaque core already exhibits weak determinism and the WD/ND covariation contrast.

Scope note: cross-construction extrapolation

The OSL framing here characterises ATR harmony within a single spell-out domain (root + affixes). [SCD26] argue that ATR harmony in Guébie particle-verb focus-fronting constructions is also local at the moment of spell-out but surface-discontinuous after subsequent A′-movement. Their pattern is not a counterexample to the OSL classification of root-internal ATR harmony — the two analyses describe disjoint construction types — but it does refute the broader extrapolation that "ATR harmony is strictly local on the surface" universally. See Studies/SandeClemDabkowski2026.lean for the discontinuous case.

inductive MeinhardtEtAl2024.Seg : Type

Minimal alphabet capturing the dominance-vs-recessive distinction that drives Maasai ATR harmony per [MMBMcC24] p. 1203. Four symbols stand in for the relevant phonological contrasts:

• recL — a recessive [-ATR] vowel (e.g., /ɪ/, /ʊ/). Surfaces as [-ATR] absent harmony; raises 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], 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

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

def MeinhardtEtAl2024.Seg.isPlusATR : Seg → Bool

Whether the segment is a [+ATR] vowel (after surface realisation). A dom segment surfaces as [+ATR] by definition; recH is underlyingly [+ATR]; recL is [-ATR] (until raised by spread); a is neither.

Equations

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

def MeinhardtEtAl2024.Seg.raise : Seg → Seg

Surface form of a segment under spreading [+ATR]: recessive [-ATR] vowels raise; everything else passes through unchanged (including the opaque /a/, which blocks the spread that would have reached it).

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.

The rule's k = 2: the output decision at each position depends on the single immediately preceding output symbol (per [CEH15] the canonical OSL fragment of phonological maps). Rule logic:

• 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 ([CEH15]), because the output decision genuinely depends on the output history (how spread has propagated) rather than the input history alone.

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 ([CEH15], the result [MMBMcC24] builds on). Witness: the OSL rule rightwardATR_osl defined above.

This is the tighter classification per the paper — single-direction iterative spreading patterns are properly contained in OSL, strictly above the ISL class but strictly below the (Left-)Subsequential class.

theorem MeinhardtEtAl2024.rightwardATR_osl_isLeftSubsequential : IsLeftSubsequential rightwardATR_osl.apply

Rightward [+ATR] spreading is also Left-Subsequential — the umbrella class, lifted from the OSL classification via OSL ⊆ Left-Subsequential (isLeftOutputStrictlyLocal_left_subsequential).

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 ([MMBMcC24], 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 (non-opaque core): 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: each side's state tracks a dominant seen on that side; a recessive raises if either side has one — 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_weaklyDeterministic : IsNonInteractingBimachineComputable maasai

Maasai ATR harmony is weakly deterministic ([MMBMcC24]): the bidirectional dominant-recessive spread is 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 (tutrugbu_twoSidedUnboundedDependence); the difference is that Maasai does not RequiresBothSides, so it stays weakly deterministic. The paper's positive classification of Maasai as unbounded semiambient — 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: every harmonised cell is 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

Strictness witness synchronous ⊊ WD: Maasai is weakly deterministic yet not Mealy-computable — the length-preserving-stratum reading of [HL13]'s LSF, RSF ⊆ WD corollary being strict, with maasai as their own dominant-recessive witness (their Thms. 6 and 7). A Mealy-computable map is right-myopic (IsMealyComputable.boundedDependence_right), but Maasai's bidirectional spread is not (maasai_twoSidedUnboundedDependence); the block-class exclusion is maasai_not_leftSubsequential.

theorem MeinhardtEtAl2024.maasai_not_leftSubsequential : ¬IsLeftSubsequential maasai

Maasai is not left-subsequential — the block class is excluded too: 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.