Yolyan (2025): A Logical Characterization of Weak Determinism as Simultaneous Application

This file formalizes Yolyan's definition of the weakly deterministic string functions as the simultaneous application P^L ⊙ P^R of a backward and a forward Boolean monadic recursive scheme (Def. 5.1), in the BMRS formalism of Bhaskar, Jardine, Chandlee and Oakden (Subregular.BMRS), whose one-sided fragments characterize the left- and right-subsequential functions. The operator ⊙ (Def. 4.1) acts per position on the input value and the two programs' output values, so that a change survives iff either program makes it (Prop. 4.2); SimulModels lifts it to programs (Def. 4.3) for the length-preserving maps of §5, and IsBmrsWeaklyDeterministic is Def. 5.1.

The negative results of §5.3 share one argument. On a far-left and on a far-right perturbation of a witness word the target is unchanged, so ⊙ is conjunction there and both one-sided outputs are forced true; each transports to the base word by one-sided locality, and recombining forces the base target unchanged. not_isBmrsWeaklyDeterministic_of_requiresBothSides proves this once from the substrate's RequiresBothSides witness, and Sour Grapes harmony (Thm. 5.2, the conjecture of Heinz and Lai), Copperbelt Bemba high-tone spreading (Prop. 5.4) and Tutrugbu ATR harmony (Prop. 5.5, through McCollumEtAl2020) are its instances. On the positive side, with no underlying stress the input predicate is constantly false and ⊙ collapses to disjunction, (5.15), which recovers Koser and Jardine's program for leftmost-heavy-otherwise-leftmost stress in Lushootseed as the simultaneous application of its two one-sided halves (§5.2). The conjunctive dual ⊘ of §6.3 (Def. 6.5) expresses Sour Grapes exactly (sourGrapes_conjunctive).

Implementation notes

• ⊙ and ⊘ are stated on values (combine, combineC), where the algebra of Prop. 4.4 is a finite computation; the program-level operators lift them pointwise. Copy sets are omitted, as none of the §5 maps needs them.
• The head types of the two programs are unconstrained, which only strengthens the negative results. The exclusion uses the d = 0 instance of the witness, since one-sidedness is global rather than window-bounded.
• Bemba spreading is a Tone.Surfacing instance built from the paper's characterization: a high spreads to the word end when no high follows it, and onto the next two tone-bearing units when one does. Unlike plateauing, the surface set is not convex and the map is neither monotone nor idempotent. The words of Example 2.11 are in Data/Forms/Yolyan2025.json, their tones read off the accents; the Tutrugbu words of Example 2.12 are McCollum et al.'s, and Data/Forms/McCollumEtAl2020.json cites them.
• Thm. 5.2 settles Heinz and Lai's conjecture under Def. 5.1; under their own definition Lamont, O'Hara and Smith express Sour Grapes as a composition of contradirectional subsequential functions.

TODO

• Thm. 5.3 (Yidiny liquid dissimilation) awaits a map for that pattern.

References

• [Yol25]
• [BCJO20]
• [HL13]
• [KJ20]
• [McCBMM20]
• [Jar16a]
• [Pad95]
• [Wil03b]
• [LOHS19]

@[reducible, inline]

abbrev Yolyan2025.x : Subregular.Walk

x is the single BMRS index variable.

Equations

• Yolyan2025.x = Subregular.Walk.var

Simultaneous application, at the value level

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.

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

Simultaneous application ⊙ on values (Def. 4.1) keeps a change 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) keeps a change 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).

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

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).

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

⊙ is commutative (Prop. 4.4 (i)).

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

⊙ is associative (Prop. 4.4 (ii)).

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 ⊙, negating the two output values but 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

b is the value of the ⊙-combined output predicate for σ at i (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, for the length-preserving maps of §5) when 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

f is weakly deterministic (Def. 5.1) when it is the simultaneous application of a backward (BMRSᵖ) and a forward (BMRSˢ) program.

Equations

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

The exclusion argument of §5.3

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

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. Thm. 5.2 and Props. 5.4 and 5.5 are instances.

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

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

inductive Yolyan2025.SG : Type

The schematic Sour Grapes alphabet has a trigger +, a target − and a 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

In Sour Grapes harmony 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, by the maps (a)–(c) of the proof of Thm. 5.2. The middle of + −…− − spreads, but neither the triggerless − −…− − nor the blocked + −…− ⊟ changes it.

theorem Yolyan2025.sourGrapes_not_bmrsWeaklyDeterministic : ¬IsBmrsWeaklyDeterministic sourGrapes

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

theorem Yolyan2025.tutrugbu_not_bmrsWeaklyDeterministic : ¬IsBmrsWeaklyDeterministic McCollumEtAl2020.tutrugbu.map

Tutrugbu ATR harmony (Example 2.12) is not weakly deterministic (Prop. 5.5), from the witness of McCollumEtAl2020.

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

Copperbelt Bemba, Example 2.11, after Jardine. A high tone spreads to the end of the word when no high follows it, and only onto the next two tone-bearing units when one does.

inductive Yolyan2025.BTone : Type

The Bemba tonal alphabet has a high and a low tone.

• 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 when it is 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 is a surfacing process.

Equations

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

def Yolyan2025.toneOf : Char → Option BTone

toneOf c is the tone of the vowel letter c, high under an acute and low otherwise; any other character is no vowel.

Equations

• Yolyan2025.toneOf 'á' = some Yolyan2025.BTone.H
• Yolyan2025.toneOf 'é' = some Yolyan2025.BTone.H
• Yolyan2025.toneOf 'í' = some Yolyan2025.BTone.H
• Yolyan2025.toneOf 'ó' = some Yolyan2025.BTone.H
• Yolyan2025.toneOf 'ú' = some Yolyan2025.BTone.H
• Yolyan2025.toneOf 'a' = some Yolyan2025.BTone.L
• Yolyan2025.toneOf 'e' = some Yolyan2025.BTone.L
• Yolyan2025.toneOf 'i' = some Yolyan2025.BTone.L
• Yolyan2025.toneOf 'o' = some Yolyan2025.BTone.L
• Yolyan2025.toneOf 'u' = some Yolyan2025.BTone.L
• Yolyan2025.toneOf 'à' = some Yolyan2025.BTone.L
• Yolyan2025.toneOf 'è' = some Yolyan2025.BTone.L
• Yolyan2025.toneOf 'ì' = some Yolyan2025.BTone.L
• Yolyan2025.toneOf 'ò' = some Yolyan2025.BTone.L
• Yolyan2025.toneOf 'ù' = some Yolyan2025.BTone.L
• Yolyan2025.toneOf x✝ = none

def Yolyan2025.ofAnalysis (a : Forms.Analysis) : Option (List BTone × List BTone)

ofAnalysis a is the tones of the underlying and of the surface form of the word a analyses, one per vowel, when the two have as many vowels.

Equations

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

theorem Yolyan2025.bemba_map_forms (a : Forms.Analysis) : a ∈ Forms.analyses → ∀ p ∈ ofAnalysis a, bemba.map p.1 = p.2

Bemba spreading takes the tones of each word of Example 2.11 to its surface tones. In (a) the initial high spreads to the end of the word, and in (b) a following high bounds the spread to the next two tone-bearing units.

theorem Yolyan2025.bemba_requiresBothSides : RequiresBothSides bemba.map

Bemba spreading requires both sides, by the maps (a)–(c) of the proof of Prop. 5.4. The middle of H L…L L spreads, but neither the triggerless far-left flip nor the far-right H, which bounds the spread to two TBUs, changes it.

theorem Yolyan2025.bemba_not_bmrsWeaklyDeterministic : ¬IsBmrsWeaklyDeterministic bemba.map

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

LHOL stress as a simultaneous application (§5.2)

Leftmost-heavy-otherwise-leftmost stress in Lushootseed, Example 2.9: stress the leftmost heavy syllable, else the leftmost syllable. The backward program stresses 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 false and ⊙ collapses to the disjunction (5.15) of the two programs, the program of [KJ20].

inductive Yolyan2025.Syll : Type

A syllable is heavy or light.

• 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

The backward stress program has two heads, noHL being (5.8), no heavy anywhere to the left.

• 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 ⋯

@[instance_reducible]

instance Yolyan2025.instFintypeLHead : Fintype LHead

Equations

• Yolyan2025.instFintypeLHead = { elems := { val := ↑Yolyan2025.LHead.enumList, nodup := Yolyan2025.LHead.enumList_nodup }, complete := Yolyan2025.instFintypeLHead._proof_1 }

inductive Yolyan2025.RHead : Type

The forward stress program has two heads, noHR being (5.9), no heavy anywhere to the right.

• 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 ⋯

@[instance_reducible]

instance Yolyan2025.instFintypeRHead : Fintype RHead

Equations

• Yolyan2025.instFintypeRHead = { elems := { val := ↑Yolyan2025.RHead.enumList, nodup := Yolyan2025.RHead.enumList_nodup }, complete := Yolyan2025.instFintypeRHead._proof_1 }

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

The backward program, (5.8) and (5.12), stresses 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

The forward program, (5.9) and (5.11), stresses 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

def Yolyan2025.lholStress (w : List Syll) : List (Option Bool)

The stress pattern the ⊙ of the two programs assigns to a word, position by position, is the disjunction (5.15), there being no underlying stress.

Equations

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

theorem Yolyan2025.lholStress_LHLHL : lholStress [Syll.L, Syll.H, Syll.L, Syll.H, Syll.L] = [some false, some true, some false, some false, some false]

In Example 2.9 (a), LH́LHL, the backward program alone stresses the leftmost heavy.

theorem Yolyan2025.lholStress_HHHHH : lholStress [Syll.H, Syll.H, Syll.H, Syll.H, Syll.H] = [some true, some false, some false, some false, some false]

In Example 2.9 (a), H́HHHH, the backward program alone stresses an initial heavy.

theorem Yolyan2025.lholStress_LLLLL : lholStress [Syll.L, Syll.L, Syll.L, Syll.L, Syll.L] = [some true, some false, some false, some false, some false]

In Example 2.9 (b), ĹLLLL, with no heavy, the forward program alone stresses the initial syllable.

Sour Grapes as a conjunctive simultaneous application (§6.3)

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, (6.6) and (6.7). At a target, spreading happens iff a trigger lies to the left and no blocker lies to the right.