Yolyan 2025: Weak Determinism as Simultaneous Application

[Yol25]: weakly deterministic functions are those expressible as the simultaneous application P^L ⊙ P^R of a backward and a forward BMRS program (Def. 5.1) — a definition inside the program formalism, which for the first time makes non-membership provable. The ambient formalism is the Boolean monadic recursive schemes of [BCJO20] (Subregular.BMRS), whose one-sided fragments BMRSᵖ/BMRSˢ characterize the left- and right-subsequential functions; [BCJ23] extends the characterization and [CJ21] applies it to phonological modelling. IsBmrsWeaklyDeterministic renders Def. 5.1 via the value-level ⊙ below: SimulModels asks each output symbol to be the ⊙-combination of the two programs' output predicates against the input (Defs. 4.1/4.3), sparing the combined-head-space construction.

The engine is not_isBmrsWeaklyDeterministic_of_requiresBothSides: the paper's §5.3 template (Thms. 5.2–5.5), consuming the same Subregular.RequiresBothSides witness that excludes the bimachine rendering of weak determinism (RequiresBothSides.not_isNonInteractingBimachineComputable). Whether the two definitions coincide is the paper's own open question (§6.1, on the μ-conserving proposal of [MMBMcC24]); feeding both exclusions one witness object states it structurally without resolving it. The proof here streamlines the paper's: on either perturbation the input value is unchanged, so ⊙ collapses to conjunction and both one-sided outputs are forced true; each transports to the base word by one-sided locality (Eval.congr_eqOn_Iic/congr_eqOn_Ici), and recombining forces the base unchanged — no case-split through Prop. 4.2 needed. Only the d = 0 instance of the witness is used: one-sidedness is global, not window-bounded.

Instances: Sour Grapes harmony (Thm. 5.2 — the first proof of the [HL13] conjecture under the paper's Def. 5.1; under the original definition the conjecture is false, [LOHS19] Thm. 3.1 — via [Pad95]/[Wil03b]'s pathology), and — through the shared witnesses already in the library — Tutrugbu ATR harmony (Prop. 5.5, [McCBMM20]), Luganda unbounded tonal plateauing ([Jar16a]), and Copperbelt Bemba high-tone spreading (Prop. 5.4), the latter formalized here as a second Tone.Surfacing instance. The positive side: with no underlying stress the input predicate is constantly ⊥ and ⊙ collapses to disjunction — (5.15), recovering [KJ20]'s LHOL program as the simultaneous application of its two one-sided halves. §6.3's conjunctive dual ⊘ is exact on Sour Grapes: sourGrapes_conjunctive shows the map is the ⊘ of its one-sided licensing conditions.

Simultaneous application, at the value level

[Yol25] Def. 4.1 (⊙) and Def. 6.5 (⊘) act per input position on the input value and the two programs' output values; the program-level operators lift these pointwise. Stating the algebra (Prop. 4.4) on values keeps it a finite Bool computation and spares the combined-head-space transport.

def Yolyan2025.combine (pin a b : Bool) : Bool

Simultaneous application ⊙ on values (Def. 4.1): a change survives iff either program makes it.

Equations

• Yolyan2025.combine pin a b = if pin = true then a && b else a || b

def Yolyan2025.combineC (pin a b : Bool) : Bool

Conjunctive simultaneous application ⊘ on values (Def. 6.5): a change survives iff both programs make it.

Equations

• Yolyan2025.combineC pin a b = if pin = true then a || b else a && b

@[simp]

theorem Yolyan2025.combine_true (a b : Bool) : combine true a b = (a && b)

On a true input, ⊙ is conjunction.

@[simp]

theorem Yolyan2025.combine_false (a b : Bool) : combine false a b = (a || b)

On a false input, ⊙ is disjunction — the collapse behind (5.15): with no underlying stress the ⊙ of the two stress programs is their disjunction.

@[simp]

theorem Yolyan2025.combineC_true (a b : Bool) : combineC true a b = (a || b)

On a true input, ⊘ is disjunction.

@[simp]

theorem Yolyan2025.combineC_false (a b : Bool) : combineC false a b = (a && b)

On a false input, ⊘ is conjunction — the conjunctive licensing of §6.3.

theorem Yolyan2025.combine_ne_iff (pin a b : Bool) : combine pin a b ≠ pin ↔ a ≠ pin ∨ b ≠ pin

A ⊙-value differs from the input iff one of the components does (Prop. 4.2): the changes of the simultaneous application are the union of the changes.

theorem Yolyan2025.combine_comm (pin a b : Bool) : combine pin a b = combine pin b a

theorem Yolyan2025.combine_assoc (pin a b c : Bool) : combine pin (combine pin a b) c = combine pin a (combine pin b c)

theorem Yolyan2025.combine_id (pin a : Bool) : combine pin a pin = a

The input itself is a ⊙-identity (Prop. 4.4(iii)).

theorem Yolyan2025.combineC_eq_not_combine (pin a b : Bool) : combineC pin a b = !combine pin (!a) !b

⊘ is the De Morgan dual of ⊙: negate the two output values, not the input.

theorem Yolyan2025.combineC_comm (pin a b : Bool) : combineC pin a b = combineC pin b a

theorem Yolyan2025.combineC_assoc (pin a b c : Bool) : combineC pin (combineC pin a b) c = combineC pin a (combineC pin b c)

Weak determinism as simultaneous application (Defs. 4.1, 4.3, 5.1)

def Yolyan2025.SimulEval {α : Type u_1} [DecidableEq α] {L R : Type} (PL : Subregular.BMRS.Program α L) (PR : Subregular.BMRS.Program α R) (hL : L) (hR : R) (w : List α) (i : ℕ) (σ : α) (b : Bool) : Prop

The value of the ⊙-combined output predicate for σ at i ([Yol25] Def. 4.1): the two programs' output values combined against the input value.

Equations

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

def Yolyan2025.SimulModels {α : Type u_1} [DecidableEq α] {L R : Type} (PL : Subregular.BMRS.Program α L) (PR : Subregular.BMRS.Program α R) (outL : α → L) (outR : α → R) (f : List α → List α) : Prop

The simultaneous application P^L ⊙ P^R models f (Def. 4.3, restricted to the length-preserving maps of §5): each output symbol is the one whose ⊙-combined output predicate holds.

Equations

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

def Yolyan2025.IsBmrsWeaklyDeterministic {α : Type u_1} [DecidableEq α] (f : List α → List α) : Prop

Def. 5.1: f is weakly deterministic when it is the simultaneous application of a backward (BMRSᵖ) and a forward (BMRSˢ) program. Head types are unconstrained (the paper's are finite), which only strengthens the negative results below.

Equations

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

The exclusion template (§5.3)

theorem Yolyan2025.not_isBmrsWeaklyDeterministic_of_requiresBothSides {α : Type u_1} [DecidableEq α] {f : List α → List α} (hf : RequiresBothSides f) : ¬IsBmrsWeaklyDeterministic f

The §5.3 template, proven once: a map that requires both sides is not weakly deterministic. On the far-left perturbation the target is unchanged, so ⊙ is conjunction and both one-sided outputs are true; the forward one transports to the base by locality. Symmetrically the far-right perturbation delivers the backward one. Recombining in the base forces the target unchanged — contradiction. Thms. 5.2, 5.3 and Props. 5.4, 5.5 are instances.

Sour Grapes harmony is not weakly deterministic (Thm. 5.2)

The pathology of [Pad95]/[Wil03b]: − becomes + iff a + lies anywhere to its left and no blocker ⊟ anywhere to its right — spreading happens only when it can reach the end of the word.

inductive Yolyan2025.SG : Type

The schematic Sour Grapes alphabet: trigger +, target −, blocker ⊟.

• plus : SG
• minus : SG
• blk : SG

@[instance_reducible]

instance Yolyan2025.instDecidableEqSG : DecidableEq SG

Equations

• Yolyan2025.instDecidableEqSG x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Yolyan2025.instReprSG.repr : SG → ℕ → Std.Format

Equations

• Yolyan2025.instReprSG.repr Yolyan2025.SG.plus prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Yolyan2025.SG.plus")).group prec✝
• Yolyan2025.instReprSG.repr Yolyan2025.SG.minus prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Yolyan2025.SG.minus")).group prec✝
• Yolyan2025.instReprSG.repr Yolyan2025.SG.blk prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Yolyan2025.SG.blk")).group prec✝

@[instance_reducible]

instance Yolyan2025.instReprSG : Repr SG

Equations

• Yolyan2025.instReprSG = { reprPrec := Yolyan2025.instReprSG.repr }

def Yolyan2025.sourGrapes (w : List SG) : List SG

Sour Grapes harmony, by the paper's own characterization: a − surfaces + iff a trigger precedes it and no blocker follows it.

Equations

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

theorem Yolyan2025.sourGrapes_requiresBothSides : RequiresBothSides sourGrapes

Sour Grapes requires both sides: the middle of + −…− − spreads, but neither the triggerless − −…− − (far-left perturbation) nor the blocked + −…− ⊟ (far-right) changes it.

theorem Yolyan2025.sourGrapes_not_bmrsWeaklyDeterministic : ¬IsBmrsWeaklyDeterministic sourGrapes

Thm. 5.2 — the first proof of the [HL13] conjecture, under the paper's Def. 5.1 (under the original definition it is false, [LOHS19] Thm. 3.1).

theorem Yolyan2025.sourGrapes_not_bimachineWeaklyDeterministic : ¬IsNonInteractingBimachineComputable sourGrapes

The same witness excludes the bimachine rendering of weak determinism — the two exclusions consume one object, which is the sharpest formal statement available of the paper's §6.1 open question (are the two definitions equivalent?).

The library's unbounded-circumambient maps, through the same template

theorem Yolyan2025.tutrugbu_not_bmrsWeaklyDeterministic : ¬IsBmrsWeaklyDeterministic McCollumEtAl2020.tutrugbuATR

Prop. 5.5 (Tutrugbu ATR harmony is not weakly deterministic), riding the witness already formalized for the bimachine side in Studies/McCollumEtAl2020.

theorem Yolyan2025.utp_not_bmrsWeaklyDeterministic : ¬IsBmrsWeaklyDeterministic Tone.Plateauing.utp.map

Luganda unbounded tonal plateauing is not weakly deterministic: [Jar16a]'s flagship pattern (the class of the paper's Prop. 5.4 Bemba case), through Phonology/Tone/Plateauing's witness.

Bemba high-tone spreading is not weakly deterministic (Prop. 5.4)

Copperbelt Bemba ([Jar16a]; the paper's bounded/unbounded spreading data): a high tone spreads to the end of the word when no high follows it, and only onto the next two TBUs when one does. A second Tone.Surfacing instance — and a cautionary one: unlike plateauing, the surface set is not convex and the map is neither monotone nor idempotent, so only the shared surfacing API transfers.

inductive Yolyan2025.BTone : Type

The Bemba tonal alphabet.

• H : BTone
• L : BTone

@[instance_reducible]

instance Yolyan2025.instDecidableEqBTone : DecidableEq BTone

Equations

• Yolyan2025.instDecidableEqBTone x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Yolyan2025.instReprBTone.repr : BTone → ℕ → Std.Format

Equations

• Yolyan2025.instReprBTone.repr Yolyan2025.BTone.H prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Yolyan2025.BTone.H")).group prec✝
• Yolyan2025.instReprBTone.repr Yolyan2025.BTone.L prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Yolyan2025.BTone.L")).group prec✝

@[instance_reducible]

instance Yolyan2025.instReprBTone : Repr BTone

Equations

• Yolyan2025.instReprBTone = { reprPrec := Yolyan2025.instReprBTone.repr }

def Yolyan2025.bembaSurfaces (w : List BTone) (i : ℕ) : Prop

Position i surfaces H: an underlying H, within the two-TBU bounded spread of a preceding H, or at-or-after the last H (unbounded spread to the word end).

Equations

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

@[instance_reducible]

instance Yolyan2025.instDecidableBembaSurfaces (w : List BTone) (i : ℕ) : Decidable (bembaSurfaces w i)

Equations

• Yolyan2025.instDecidableBembaSurfaces w i = id inferInstance

def Yolyan2025.bemba : Tone.Surfacing BTone

Bemba high-tone spreading as a surfacing process.

Equations

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

theorem Yolyan2025.bemba_requiresBothSides : RequiresBothSides bemba.map

Bemba spreading requires both sides: the middle of H L…L L spreads (unbounded, no blocker), but neither the triggerless far-left flip nor the far-right H (which bounds the spread to two TBUs) changes it — Tone.Surfacing's flank template, from the three surfacing facts alone.

theorem Yolyan2025.bemba_not_bmrsWeaklyDeterministic : ¬IsBmrsWeaklyDeterministic bemba.map

Prop. 5.4: Bemba high-tone spreading is not weakly deterministic.

theorem Yolyan2025.bemba_not_bimachineWeaklyDeterministic : ¬IsNonInteractingBimachineComputable bemba.map

The bimachine twin, off the same witness.

The positive side: LHOL stress as a simultaneous application (§5.2)

Leftmost-heavy-otherwise-leftmost stress ([KJ20]; Lushootseed): stress the leftmost heavy syllable, else the leftmost syllable. The backward program finds a heavy with no heavy to its left; the forward program stresses an initial light with no heavy to its right. No syllable is underlyingly stressed, so the input predicate is constantly ⊥ and ⊙ collapses to disjunction — (5.15), the Koser–Jardine program.

inductive Yolyan2025.Syll : Type

Syllable weight.

• H : Syll
• L : Syll

@[instance_reducible]

instance Yolyan2025.instDecidableEqSyll : DecidableEq Syll

Equations

• Yolyan2025.instDecidableEqSyll x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Yolyan2025.instReprSyll : Repr Syll

Equations

• Yolyan2025.instReprSyll = { reprPrec := Yolyan2025.instReprSyll.repr }

def Yolyan2025.instReprSyll.repr : Syll → ℕ → Std.Format

Equations

• Yolyan2025.instReprSyll.repr Yolyan2025.Syll.H prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Yolyan2025.Syll.H")).group prec✝
• Yolyan2025.instReprSyll.repr Yolyan2025.Syll.L prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Yolyan2025.Syll.L")).group prec✝

inductive Yolyan2025.LHead : Type

Heads of the backward stress program: noHL = no heavy anywhere left (5.8).

• noHL : LHead
• stressL : LHead

@[instance_reducible]

instance Yolyan2025.instDecidableEqLHead : DecidableEq LHead

Equations

• Yolyan2025.instDecidableEqLHead x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Yolyan2025.RHead : Type

Heads of the forward stress program: noHR = no heavy anywhere right (5.9).

• noHR : RHead
• stressR : RHead

@[instance_reducible]

instance Yolyan2025.instDecidableEqRHead : DecidableEq RHead

Equations

• Yolyan2025.instDecidableEqRHead x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Yolyan2025.lholL : Subregular.BMRS.Program Syll LHead

(5.8), (5.12): stress a heavy with no heavy to its left.

Equations

• One or more equations did not get rendered due to their size.
• Yolyan2025.lholL Yolyan2025.LHead.stressL = (Subregular.BMRS.Expr.label {Yolyan2025.Syll.H} Yolyan2025.x✝).and (Subregular.BMRS.Expr.call Yolyan2025.LHead.noHL Yolyan2025.x✝)

def Yolyan2025.lholR : Subregular.BMRS.Program Syll RHead

(5.9), (5.11): stress an initial light with no heavy to its right.

Equations

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

theorem Yolyan2025.lholL_backward : lholL.Backward

theorem Yolyan2025.lholR_forward : lholR.Forward

theorem Yolyan2025.lhol_LHLLH : List.map (fun (i : ℕ) => (Subregular.BMRS.evalFuel lholL [Syll.L, Syll.H, Syll.L, Syll.L, Syll.H] 32 i (Subregular.BMRS.Expr.call LHead.stressL Yolyan2025.x✝)).bind fun (bL : Bool) => Option.map (fun (bR : Bool) => combine false bL bR) (Subregular.BMRS.evalFuel lholR [Syll.L, Syll.H, Syll.L, Syll.L, Syll.H] 32 i (Subregular.BMRS.Expr.call RHead.stressR Yolyan2025.x✝))) (List.range 5) = [some false, some true, some false, some false, some false]

With no underlying stress, ⊙ is the disjunction of the two programs — (5.15). On LHLLH the backward program stresses the leftmost heavy alone.

theorem Yolyan2025.lhol_LLLL : List.map (fun (i : ℕ) => (Subregular.BMRS.evalFuel lholL [Syll.L, Syll.L, Syll.L, Syll.L] 32 i (Subregular.BMRS.Expr.call LHead.stressL Yolyan2025.x✝)).bind fun (bL : Bool) => Option.map (fun (bR : Bool) => combine false bL bR) (Subregular.BMRS.evalFuel lholR [Syll.L, Syll.L, Syll.L, Syll.L] 32 i (Subregular.BMRS.Expr.call RHead.stressR Yolyan2025.x✝))) (List.range 4) = [some true, some false, some false, some false]

On all-light LLLL the forward program stresses the initial syllable alone.

§6.3: Sour Grapes is conjunctively simultaneous

theorem Yolyan2025.sourGrapes_conjunctive {w : List SG} {i : ℕ} (hm : w[i]? = some SG.minus) : (sourGrapes w)[i]? = some (if combineC false (decide (SG.plus ∈ List.take i w)) (decide (SG.blk ∉ List.drop i w)) = true then SG.plus else SG.minus)

Sour Grapes is the conjunctive simultaneous application ⊘ (Def. 6.5) of its two one-sided licensing conditions: at a target, spreading happens iff the backward condition (a trigger left) and the forward condition (no blocker right) both fire. The disjunctive ⊙ cannot express this (Thm. 5.2); ⊘ does so exactly — the paper's §6.3 route toward characterizing unbounded circumambience.