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

Worked example using the function-level subregular substrate (Core/Computability/Subregular/Function/) to classify a fragment of Eastern Nilotic ATR harmony per @cite{meinhardt-mai-bakovic-mccollum-2024}.

The paper

@cite{meinhardt-mai-bakovic-mccollum-2024} (NLLT 42:1191-1232) propose a tightening of the @cite{heinz-lai-2013} Weakly Deterministic (WD) function class. Their thesis:

• Bidirectional iterative ATR harmony in Maasai and Turkana (Eastern Nilotic) is attested and WD — a composition of two subsequential FSTs reading from opposite directions, where the two passes do not interact in the technical sense the paper formalises (§5).
• Hypothetical unbounded-circumambient "sour grapes" patterns (@cite{wilson-2003}; @cite{wilson-2006}) are unattested and non-deterministic — the inner and outer passes interact, placing the function strictly above WD in the hierarchy (Fig. 1).
• 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 (§§5–6).

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 a lexical property of the root, independent of the surface ATR value of any individual segment. A dominant root triggers spreading regardless of its constituent vowels' phonetic ATR; a recessive root does not.

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

• (i) Full bidirectional spreading from a dominant root: /kɪ-√noŋ-ʊ/ → [ki-√noŋ-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-ɪʃɔ-rɛ/ → [ɪ-√as-iʃo-re] '2sg-do-intr-appl' — the spreading [+ATR] reaches the rightward vowels but is blocked leftward by the opaque /a/, 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 SFST and an OSLRule. Per paper §5.4 (p. 45), single- direction iterative spreading is Output-Strictly-Local — 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. Documents the bidirectional upgrade and its WD classification. Formal proof deferred to Function/WeaklyDeterministic.lean (in this PR), which lands both Heinz-Lai 2013 and Meinhardt et al. 2024 definitions side-by-side per linglib's "make incompatibilities visible" thesis.

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 contains far richer data including back-rounding harmony interactions and exceptional roots.
• Does not prove sour-grapes patterns are non-deterministic (impossibility argument requires a sophisticated pumping-style reasoning, deferred to a follow-up dedicated to negative results).
• Does not encode the leftward pass or the bidirectional composition (substrate ready: SFST.compose from Function/Subsequential.lean and IsLeftSubsequential.comp from Function/Subsequential.lean would be the building blocks; the WD predicate then certifies non- interaction of the two passes).

Scope note: cross-construction extrapolation

The OSL framing here characterises ATR harmony within a single spell-out domain (root + affixes). @cite{sande-clem-dabkowski-2026} 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 Phenomena/Phonology/Studies/SandeClemDabkowski2026.lean for the discontinuous case.

inductive Phenomena.Phonology.Studies.MeinhardtEtAl2024.Seg : Type

Minimal alphabet capturing the dominance-vs-recessive distinction that drives Maasai ATR harmony per @cite{meinhardt-mai-bakovic-mccollum-2024} 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 [+ATR] vowel (e.g., /i/, /u/). Already [+ATR]; passes spread through.
• dom — a dominant vowel. Triggers [+ATR] spread regardless of its own surface quality (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

@[implicit_reducible]

instance Phenomena.Phonology.Studies.MeinhardtEtAl2024.instDecidableEqSeg : DecidableEq Seg

Equations

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

@[implicit_reducible]

instance Phenomena.Phonology.Studies.MeinhardtEtAl2024.instReprSeg : Repr Seg

Equations

• Phenomena.Phonology.Studies.MeinhardtEtAl2024.instReprSeg = { reprPrec := Phenomena.Phonology.Studies.MeinhardtEtAl2024.instReprSeg.repr }

def Phenomena.Phonology.Studies.MeinhardtEtAl2024.instReprSeg.repr : Seg → ℕ → Std.Format

Equations

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

def Phenomena.Phonology.Studies.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

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

def Phenomena.Phonology.Studies.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

• Phenomena.Phonology.Studies.MeinhardtEtAl2024.Seg.recL.raise = Phenomena.Phonology.Studies.MeinhardtEtAl2024.Seg.recH
• x✝.raise = x✝

def Phenomena.Phonology.Studies.MeinhardtEtAl2024.rightwardATR_osl : Core.Computability.Subregular.Function.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 @cite{chandlee-eyraud-heinz-2015} 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).

Per paper §5.4 (p. 45): single-direction iterative spreading patterns are OSL but not ISL, 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.

def Phenomena.Phonology.Studies.MeinhardtEtAl2024.rightwardATR : Core.Computability.Subregular.Function.SFST Bool Seg Seg

Equivalent SFST for the same map: state tracks whether spread is active. Demonstrates that the rule has both an OSL representation (above) and a Subsequential representation (here) — the latter being the umbrella class.

Equations

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

theorem Phenomena.Phonology.Studies.MeinhardtEtAl2024.rightwardATR_osl_isLeftOutputStrictlyLocal : Core.Computability.Subregular.Function.IsLeftOutputStrictlyLocal 2 rightwardATR_osl.apply

Rightward [+ATR] spreading is Left-Output-Strictly-Local (@cite{chandlee-eyraud-heinz-2015}; @cite{meinhardt-mai-bakovic-mccollum-2024} §5.4). 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 Phenomena.Phonology.Studies.MeinhardtEtAl2024.rightwardATR_isLeftSubsequential : Core.Computability.Subregular.Function.IsLeftSubsequential rightwardATR.run

Rightward [+ATR] spreading is also Left-Subsequential (a weaker claim than OSL but the umbrella class). Witness: the SFST.

theorem Phenomena.Phonology.Studies.MeinhardtEtAl2024.rightwardATR_osl_isLeftSubsequential : Core.Computability.Subregular.Function.IsLeftSubsequential rightwardATR_osl.apply

Since OSL ⊆ Left-Subsequential (Function/Hierarchy.lean), the OSL classification automatically lifts.

Bidirectional Maasai harmony — WD classification

The full Maasai/Turkana pattern in (1a) is bidirectional: [+ATR] spreads from a dominant root vowel both leftward and rightward, with spread blocked by the opaque /a/ in either direction (per ex 1a-ii). The bidirectional function is the composition of rightwardATR (left-subsequential) with a leftwardATR (right-subsequential — mirror image via SFST.runRight):

maasai := leftwardATR.runRight ∘ rightwardATR.run     -- (or vice versa)

@cite{meinhardt-mai-bakovic-mccollum-2024} call such non-interacting two-pass compositions Weakly Deterministic. The non-interaction condition is what their paper formalises and tightens compared to @cite{heinz-lai-2013}'s original definition.

Both definitions land in Function/WeaklyDeterministic.lean (this PR) per linglib's "make incompatibilities visible" thesis: the IsWeaklyDeterministic_HL2013 and IsWeaklyDeterministic_MMBM2024 predicates state the contested pair side-by-side. The Maasai bidirectional function is claimed WD by both definitions; the divergence point — sour-grapes-style functions admitted by HL2013 but rejected by MMBM2024 — is where the patch matters.

Sour grapes harmony (@cite{wilson-2003}; @cite{wilson-2006}) — where leftward spread fails entirely if blocked at any position — is the canonical example of a function above WD: the inner (rightward) and outer (leftward) passes interact, so no non-interacting two-pass composition can compute it. The paper argues sour grapes is unattested cross-linguistically; formalising the impossibility-of-WD claim is deferred to a follow-up.