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 [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 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 ([Wil03b]; [Wil06]) 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. Proves the bidirectional dominant-recessive map maasai is weakly deterministic (maasai_weaklyDeterministic) via a non-interacting bimachine, yet unbounded-circumambient as covariation (maasai_isUnboundedCircumambient) — the same predicate Tutrugbu 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 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).
• Models the bidirectional map directly (maasai: raise a recessive iff a dominant occurs anywhere) rather than as an explicit two-pass composition leftwardATR.runRight ∘ rightwardATR.run, 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 [+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 MeinhardtEtAl2024.instDecidableEqSeg : DecidableEq Seg

Equations

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

@[implicit_reducible]

instance MeinhardtEtAl2024.instReprSeg : Repr Seg

Equations

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

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✝

@[implicit_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).

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 MeinhardtEtAl2024.rightwardATR : Subregular.SFST Seg Seg Bool

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 MeinhardtEtAl2024.rightwardATR_osl_isLeftOutputStrictlyLocal : Subregular.IsLeftOutputStrictlyLocal 2 rightwardATR_osl.apply

Rightward [+ATR] spreading is Left-Output-Strictly-Local ([CEH15]; [MMBMcC24] §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 MeinhardtEtAl2024.rightwardATR_isLeftSubsequential : Subregular.IsLeftSubsequential rightwardATR.run

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

theorem MeinhardtEtAl2024.rightwardATR_osl_isLeftSubsequential : Subregular.IsLeftSubsequential rightwardATR_osl.apply

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

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. Yet — like Tutrugbu — a recessive's surface ATR co-varies with information unboundedly far on either side, so maasai also satisfies IsUnboundedCircumambient. The contrast is exactly the WD/ND boundary the paper draws: both maps are circumambient as covariation, but only Tutrugbu RequiresBothSides (suppression/conjunction).

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 : Subregular.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_lState (xs : List Seg) : maasaiBM.lState xs = xs.any fun (x : Seg) => x == Seg.dom

The left state after a prefix is exactly "a dominant occurs in it".

theorem MeinhardtEtAl2024.maasaiBM_rState (xs : List Seg) : maasaiBM.rState xs = xs.any fun (x : Seg) => x == Seg.dom

The right state after a suffix is exactly "a dominant occurs in it".

theorem MeinhardtEtAl2024.maasaiBM_run : maasaiBM.run = maasai

The bimachine computes maasai.

theorem MeinhardtEtAl2024.maasai_weaklyDeterministic : Subregular.IsBimachineWeaklyDeterministic maasai

Maasai ATR harmony is weakly deterministic ([MMBMcC24]): the bidirectional dominant-recessive spread is a non-interacting bimachine.

theorem MeinhardtEtAl2024.maasai_isUnboundedCircumambient : Subregular.IsUnboundedCircumambient maasai

Maasai is unbounded-circumambient as covariation — at every distance, a medial recessive's ATR flips under a dominant placed far to the left or far to the right. The same predicate Tutrugbu satisfies (tutrugbu_isUnboundedCircumambient); the difference is that Maasai does not RequiresBothSides.

theorem MeinhardtEtAl2024.maasai_not_requiresBothSides : ¬Subregular.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_letterLeftSubsequential : ¬Subregular.IsLetterLeftSubsequential maasai

Strictness witness subsequential ⊊ WD: Maasai is weakly deterministic yet not left-subsequential. A synchronous left-subsequential map is right-myopic (IsLetterLeftSubsequential.isRightMyopic), but Maasai's bidirectional spread is not (maasai_isUnboundedCircumambient).