McCollum, Baković, Mai & Meinhardt (2020): Tutrugbu ATR harmony is circumambient

[McCBMM20] (Phonology 37:215-255) show that Tutrugbu (Kwa, Ghana) regressive ATR harmony is an unbounded circumambient segmental pattern (their def. 13): the surface ATR of a prefix vowel depends on information arbitrarily far away on both sides — the [ATR] value of the root (to the right) and the [high] value of the initial-syllable vowel (to the left). Circumambient patterns require non-deterministic regular power (above the weakly-deterministic upper bound of [HL13]); Tutrugbu is, in the authors' words, "a variation on the sour grapes pattern" — i.e. a non-myopic harmony ([Wil03b], [Wil06]). It is thus a robustly attested counterexample to the claim that unbounded spreading is always myopic: [Wal10] argued (from Romance metaphony) that nonmyopic harmony exists; [Kim12] and [Mas19] replied that harmony is myopic; Tutrugbu is the segmental case the myopic-side replies do not dissolve.

The pattern (paper §2.1)

[+ATR] is dominant; affixes are underlyingly [−ATR]; harmony is regressive (root → prefix). The conditional-blocking generalisation (paper §2.1, exx. (6)-(8)):

• a [−high] prefix vowel blocks harmony iff the initial-syllable vowel is [+high] (exx. (6)); two [+high] prefixes (3) or two [−high] prefixes (4)-(5) never block; harmony spreads as far as the blocking [−high] vowel and stops (7);
• the [+high] initial and the [−high] blocker may be separated by an unbounded number of syllables (ex. (8), 0–4-syllable gaps shown). So a medial vowel's ATR depends on the root (right) and the initial-σ height (left), both unbounded.

What this file does

Seg is a toy alphabet (prefix vowels ±high × ±ATR-surface; root ±ATR). tutrugbuATR implements the conditional-blocking rule faithfully; the paper's exx. (3)-(8) are decide-checked as stimulus contrasts. tutrugbu_isUnboundedCircumambient and tutrugbu_nonmyopic connect it to the substrate predicates in SideDeterminacy.lean.

The machine-level classification (circumambient ⟹ non-deterministic, not weakly deterministic) needs bimachine substrate and is deferred; the co-located circumambience proved here is exactly what that argument consumes.

Alphabet and the conditional-blocking rule

inductive McCollumEtAl2020.Seg : Type

Toy Tutrugbu segment alphabet. Prefix vowels carry [±high] and a surface [±ATR]; the root carries [±ATR] (the harmony trigger). Underlying prefixes are [−ATR] (vHi/vLo); harmony raises them to the [+ATR] surface forms (vHiA/vLoA).

• vHi : Seg
• vLo : Seg
• vHiA : Seg
• vLoA : Seg
• rP : Seg
• rM : Seg

@[implicit_reducible]

instance McCollumEtAl2020.instDecidableEqSeg : DecidableEq Seg

Equations

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

@[implicit_reducible]

instance McCollumEtAl2020.instReprSeg : Repr Seg

Equations

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

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

Equations

• McCollumEtAl2020.instReprSeg.repr McCollumEtAl2020.Seg.vHi prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "McCollumEtAl2020.Seg.vHi")).group prec✝
• McCollumEtAl2020.instReprSeg.repr McCollumEtAl2020.Seg.vLo prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "McCollumEtAl2020.Seg.vLo")).group prec✝
• McCollumEtAl2020.instReprSeg.repr McCollumEtAl2020.Seg.vHiA prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "McCollumEtAl2020.Seg.vHiA")).group prec✝
• McCollumEtAl2020.instReprSeg.repr McCollumEtAl2020.Seg.vLoA prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "McCollumEtAl2020.Seg.vLoA")).group prec✝
• McCollumEtAl2020.instReprSeg.repr McCollumEtAl2020.Seg.rP prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "McCollumEtAl2020.Seg.rP")).group prec✝
• McCollumEtAl2020.instReprSeg.repr McCollumEtAl2020.Seg.rM prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "McCollumEtAl2020.Seg.rM")).group prec✝

def McCollumEtAl2020.Seg.isHiPfx : Seg → Bool

A [+high] prefix vowel.

Equations

• McCollumEtAl2020.Seg.vHi.isHiPfx = true
• McCollumEtAl2020.Seg.vHiA.isHiPfx = true
• x✝.isHiPfx = false

def McCollumEtAl2020.Seg.raisePfx : Seg → Seg

Raise a prefix vowel to its [+ATR] surface form (root vowels unchanged).

Equations

• McCollumEtAl2020.Seg.vHi.raisePfx = McCollumEtAl2020.Seg.vHiA
• McCollumEtAl2020.Seg.vLo.raisePfx = McCollumEtAl2020.Seg.vLoA
• x✝.raisePfx = x✝

def McCollumEtAl2020.spreadRTL (initialHi : Bool) : Bool → List Seg → List Seg

Regressive spread over the prefixes, scanned root-side first (the list is the reversed prefix sequence). spreading tracks whether [+ATR] still propagates; initialHi is whether the initial-syllable vowel is [+high] (the blocking condition). A [−high] vowel is a conditional blocker: it halts spread only when initialHi.

Equations

• One or more equations did not get rendered due to their size.
• McCollumEtAl2020.spreadRTL initialHi x✝ [] = []

@[simp]

theorem McCollumEtAl2020.spreadRTL_nil (ih sp : Bool) : spreadRTL ih sp [] = []

theorem McCollumEtAl2020.spreadRTL_cons (ih sp : Bool) (v : Seg) (rest : List Seg) : spreadRTL ih sp (v :: rest) = if sp = true then if v.isHiPfx = true then v.raisePfx :: spreadRTL ih true rest else if ih = true then v :: spreadRTL ih false rest else v.raisePfx :: spreadRTL ih true rest else v :: spreadRTL ih false rest

theorem McCollumEtAl2020.spreadRTL_stopped (ih : Bool) (L : List Seg) : spreadRTL ih false L = L

Once spreading has stopped, the scan leaves the list unchanged.

theorem McCollumEtAl2020.spreadRTL_false_true (L : List Seg) : spreadRTL false true L = List.map Seg.raisePfx L

With an initial [−high] vowel (ih = false), nothing blocks: every prefix raises.

theorem McCollumEtAl2020.spreadRTL_replicate_vHi (ih : Bool) (rest : List Seg) (n : ℕ) : spreadRTL ih true (List.replicate n Seg.vHi ++ rest) = List.replicate n Seg.vHiA ++ spreadRTL ih true rest

A replicate-block of [+high] fillers raises and keeps spreading.

def McCollumEtAl2020.tutrugbuATR (xs : List Seg) : List Seg

Tutrugbu ATR harmony on [prefix vowels…] ++ [root]. Harmony applies only with a [+ATR] root; the initial-syllable height gates conditional blocking.

Equations

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

Stimulus contrasts (paper §2.1, exx. (3)-(8))

Subregular classification

def McCollumEtAl2020.pre (init : Seg) (d : ℕ) : List Seg

The prefix sequence of the witness: a [−high]/[+high] initial, then d [+high] fillers, the [−high] target, and d more [+high] fillers.

Equations

• McCollumEtAl2020.pre init d = init :: List.replicate d McCollumEtAl2020.Seg.vHi ++ McCollumEtAl2020.Seg.vLo :: List.replicate d McCollumEtAl2020.Seg.vHi

def McCollumEtAl2020.base (d : ℕ) : List Seg

The unbounded-circumambience witness at distance d: a [−high] target flanked by d [+high] fillers on each side, a [−high] initial, and a [+ATR] root.

Equations

• McCollumEtAl2020.base d = McCollumEtAl2020.pre McCollumEtAl2020.Seg.vLo d ++ [McCollumEtAl2020.Seg.rP]

def McCollumEtAl2020.baseL (d : ℕ) : List Seg

Far-LEFT perturbation: flip the initial to [+high] (blocks the target).

Equations

• McCollumEtAl2020.baseL d = McCollumEtAl2020.pre McCollumEtAl2020.Seg.vHi d ++ [McCollumEtAl2020.Seg.rP]

def McCollumEtAl2020.baseR (d : ℕ) : List Seg

Far-RIGHT perturbation: flip the root to [−ATR] (removes the trigger).

Equations

• McCollumEtAl2020.baseR d = McCollumEtAl2020.pre McCollumEtAl2020.Seg.vLo d ++ [McCollumEtAl2020.Seg.rM]

theorem McCollumEtAl2020.tutrugbuATR_base (d : ℕ) : tutrugbuATR (base d) = Seg.vLoA :: List.replicate d Seg.vHiA ++ Seg.vLoA :: List.replicate d Seg.vHiA ++ [Seg.rP]

tutrugbuATR on base d: with a [−high] initial nothing blocks, so every prefix raises; the target at index d+1 surfaces [+ATR] (.vLoA).

theorem McCollumEtAl2020.tutrugbuATR_baseL (d : ℕ) : tutrugbuATR (baseL d) = List.replicate (d + 1) Seg.vHi ++ Seg.vLo :: List.replicate d Seg.vHiA ++ [Seg.rP]

tutrugbuATR on baseL d: a [+high] initial makes the [−high] target a blocker, so [+ATR] reaches only the root-side fillers; the target at index d+1 stays [−ATR].

theorem McCollumEtAl2020.tutrugbuATR_baseR (d : ℕ) : tutrugbuATR (baseR d) = baseR d

tutrugbuATR on baseR d: a [−ATR] root provides no trigger, so the map is the identity; the target at index d+1 stays [−ATR].

theorem McCollumEtAl2020.base_get_target (d : ℕ) : (tutrugbuATR (base d))[d + 1]? = some Seg.vLoA

The base output at the target index is [+ATR].

theorem McCollumEtAl2020.baseL_get_target (d : ℕ) : (tutrugbuATR (baseL d))[d + 1]? = some Seg.vLo

The baseL output at the target index is [−ATR] (blocked).

theorem McCollumEtAl2020.baseR_get_target (d : ℕ) : (tutrugbuATR (baseR d))[d + 1]? = some Seg.vLo

The baseR output at the target index is [−ATR] (no trigger).

theorem McCollumEtAl2020.tutrugbu_isUnboundedCircumambient : Subregular.IsUnboundedCircumambient tutrugbuATR

Tutrugbu ATR harmony is unbounded circumambient ([McCBMM20] §3, def. 13). At the medial target (index d+1): the base harmonises it ([+ATR]); flipping the initial-σ height d syllables to the left blocks it; flipping the root d syllables to the right removes the trigger — both from the one base word.

theorem McCollumEtAl2020.tutrugbu_nonmyopic (s : Subregular.Direction) : ¬Subregular.IsMyopicTowards tutrugbuATR s

Tutrugbu ATR harmony is non-myopic — the attested "variation on sour grapes" ([McCBMM20]; [Wil06]). A segmental counterexample to the myopia generalisation defended by [Kim12] and [Mas19], on the nonmyopic side argued by [Wal10].

theorem McCollumEtAl2020.pre_get_target (init : Seg) (d : ℕ) : (pre init d)[d + 1]? = some Seg.vLo

The input symbol at the target index is the recessive .vLo (for any initial and root): the prefix sequence places a [−high] vowel there.

theorem McCollumEtAl2020.tutrugbu_requiresBothSides : Subregular.RequiresBothSides tutrugbuATR

Tutrugbu ATR harmony requires both sides ([MMBMcC24] Def. 2): at the medial target the base spreads ([+ATR]), but flipping the initial height to the far left or the root ATR to the far right reverts it to its [−ATR] input — the suppression structure no union of one-sided rules can produce.

theorem McCollumEtAl2020.tutrugbu_not_weaklyDeterministic : ¬Subregular.IsBimachineWeaklyDeterministic tutrugbuATR

Tutrugbu ATR harmony is not weakly deterministic — it needs the full non-deterministic regular power, above the weakly-deterministic upper bound of [HL13]. The capstone: the conjunctive blocking (tutrugbu_requiresBothSides) cannot be a union of one-sided rules, so no non-interacting bimachine computes it.