Yolyan & Comer 2026: Phonological Processes as Modal Transductions

[YC26]: total BMRS is expressively equivalent to the modal μ-calculus on words (Thm. 2), giving an alternative proof that order-preserving BMRS captures the rational functions. This file formalizes the constructive core: the translation tr (Def. 6) from vectorial modal formulas to BMRS expressions and its compositionality (eval_tr, Remark 7) — tr φ evaluates to the truth value of φ wherever rule-head calls agree with the recursion variables. Thm. 8 discharges that hypothesis for directed systems by SCC induction (TODO: the directedness machinery); Thm. 2's converse containment runs through MSO (out of scope until an MSO substrate exists).

The paper's two worked examples ground both formalisms: vowel nasalization ((2)–(4), non-recursive) and progressive nasal spreading in Warao ((5)–(7), [osborn-1966]). The modal form N′ = μX.(N ∨ (¬T ∧ ♦X)) recurses under the backward modality ♦ = bdia — a target inherits nasality from its predecessor. Both compute the Fig. 4/5 columns on /naote/ → [nãõte], and the BMRS and modal results agree (warao_agreement); warao_tr_agreement runs Remark 7 end-to-end on the translated program, with the rule-head hypothesis discharged by direct computation — the concrete shape of Thm. 8's induction.

Segments and feature classes

The examples' segments, with the paper's overlapping feature predicates N, V, T as class tests (a nasalized vowel satisfies both V and N — a partition alphabet cannot represent the nasalization output, which is why label atoms are class tests).

inductive YolyanComer2026.Seg : Type

Segments occurring in the paper's examples.

• n : Seg
• a : Seg
• o : Seg
• t : Seg
• e : Seg
• b : Seg

@[implicit_reducible]

instance YolyanComer2026.instDecidableEqSeg : DecidableEq Seg

Equations

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

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

Equations

• YolyanComer2026.instReprSeg.repr YolyanComer2026.Seg.n prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "YolyanComer2026.Seg.n")).group prec✝
• YolyanComer2026.instReprSeg.repr YolyanComer2026.Seg.a prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "YolyanComer2026.Seg.a")).group prec✝
• YolyanComer2026.instReprSeg.repr YolyanComer2026.Seg.o prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "YolyanComer2026.Seg.o")).group prec✝
• YolyanComer2026.instReprSeg.repr YolyanComer2026.Seg.t prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "YolyanComer2026.Seg.t")).group prec✝
• YolyanComer2026.instReprSeg.repr YolyanComer2026.Seg.e prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "YolyanComer2026.Seg.e")).group prec✝
• YolyanComer2026.instReprSeg.repr YolyanComer2026.Seg.b prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "YolyanComer2026.Seg.b")).group prec✝

@[implicit_reducible]

instance YolyanComer2026.instReprSeg : Repr Seg

Equations

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

def YolyanComer2026.nas : Finset Seg

N: nasal sounds.

Equations

• YolyanComer2026.nas = {YolyanComer2026.Seg.n}

def YolyanComer2026.vow : Finset Seg

V: vowels.

Equations

• YolyanComer2026.vow = {YolyanComer2026.Seg.a, YolyanComer2026.Seg.o, YolyanComer2026.Seg.e}

def YolyanComer2026.stop : Finset Seg

T: voiceless stops (the spreading blocker).

Equations

• YolyanComer2026.stop = {YolyanComer2026.Seg.t}

def YolyanComer2026.naote : Subregular.Logic.WordModel Seg

/naote/, the Fig. 4 input.

Equations

• YolyanComer2026.naote = [YolyanComer2026.Seg.n, YolyanComer2026.Seg.a, YolyanComer2026.Seg.o, YolyanComer2026.Seg.t, YolyanComer2026.Seg.e]

def YolyanComer2026.baen : Subregular.Logic.WordModel Seg

/bæn/, the vowel-nasalization input.

Equations

• YolyanComer2026.baen = [YolyanComer2026.Seg.b, YolyanComer2026.Seg.a, YolyanComer2026.Seg.n]

Vowel nasalization ((2)–(4)): a vowel nasalizes before a nasal

inductive YolyanComer2026.NasHead : Type

Output predicates of the nasalization program.

• V' : NasHead
• N' : NasHead

@[implicit_reducible]

instance YolyanComer2026.instDecidableEqNasHead : DecidableEq NasHead

Equations

• YolyanComer2026.instDecidableEqNasHead x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def YolyanComer2026.nasalization : Subregular.Logic.BMRS.Program Seg NasHead

(3): V′(x) = V(x); N′(x) = if V(x) then N(s(x)) else N(x).

Equations

• One or more equations did not get rendered due to their size.
• YolyanComer2026.nasalization YolyanComer2026.NasHead.V' = Subregular.Logic.BMRS.Expr.label YolyanComer2026.vow YolyanComer2026.x✝

theorem YolyanComer2026.nasalization_columns : List.map (fun (i : ℕ) => Subregular.Logic.BMRS.evalFuel nasalization baen 8 i (Subregular.Logic.BMRS.Expr.call NasHead.V' YolyanComer2026.x✝)) (List.range 3) = [some false, some true, some false] ∧ List.map (fun (i : ℕ) => Subregular.Logic.BMRS.evalFuel nasalization baen 8 i (Subregular.Logic.BMRS.Expr.call NasHead.N' YolyanComer2026.x✝)) (List.range 3) = [some false, some true, some true]

Fig. 3: on /bæn/ the output columns are V′ = ⊥⊤⊥ and N′ = ⊥⊤⊤ — [bæ̃n], the æ nasalized by the following n.

def YolyanComer2026.nasalizationChi : Subregular.Logic.ModalMu.System Seg 1

(4): the modal form N′ = (V ∧ ◇N) ∨ N — non-recursive, so no fixed point is involved.

Equations

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

theorem YolyanComer2026.nasalizationChi_sat (i : ℕ) : nasalizationChi.Sat baen i ↔ i = 1 ∨ i = 2

The modal (4) marks exactly positions 1 and 2 of /bæn/ nasal, agreeing with the BMRS N′ column.

Warao nasal spreading ((5)–(7)): nasality spreads rightward until a stop

inductive YolyanComer2026.WHead : Type

The single output predicate of the spreading program.

• N' : WHead

@[implicit_reducible]

instance YolyanComer2026.instDecidableEqWHead : DecidableEq WHead

Equations

• YolyanComer2026.instDecidableEqWHead x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def YolyanComer2026.warao : Subregular.Logic.BMRS.Program Seg WHead

(6): N′(x) = if N(x) then ⊤ else if T(x) then ⊥ else if min(x) then ⊥ else N′(p(x)) — recursive through the predecessor: spreading is progressive.

Equations

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

theorem YolyanComer2026.warao_column : List.map (fun (i : ℕ) => Subregular.Logic.BMRS.evalFuel warao naote 32 i (Subregular.Logic.BMRS.Expr.call WHead.N' YolyanComer2026.x✝)) (List.range 5) = [some true, some true, some true, some false, some false]

Fig. 4: on /naote/ the output column is N′ = ⊤⊤⊤⊥⊥ — [nãõte], spreading blocked by the t.

def YolyanComer2026.waraoChi : Subregular.Logic.ModalMu.System Seg 1

(7): the modal form N′ = μX.(N ∨ (¬T ∧ ♦X)).

Equations

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

@[reducible, inline]

abbrev YolyanComer2026.waraoU : Fin 1 → Set ℕ

The least fixed point on /naote/: nasality holds exactly at positions 0, 1, 2.

Equations

• YolyanComer2026.waraoU x✝ = {i : ℕ | i < 3}

theorem YolyanComer2026.warao_op_le : (waraoChi.op naote) waraoU ≤ waraoU

waraoU is a prefixed point of the system operator.

theorem YolyanComer2026.warao_le_sem : waraoU ≤ waraoChi.sem naote

The three nasal positions are in the least fixed point (unfolding op_sem once per step of the spread).

theorem YolyanComer2026.warao_sem : waraoChi.sem naote = waraoU

The modal semantics on /naote/, exactly.

theorem YolyanComer2026.warao_sat {i : ℕ} : waraoChi.Sat naote i ↔ i < 3

Fig. 5: the modal (7) marks exactly positions 0, 1, 2 of /naote/.

theorem YolyanComer2026.warao_agreement (i : ℕ) (hi : i < 5) : Subregular.Logic.BMRS.evalFuel warao naote 32 i (Subregular.Logic.BMRS.Expr.call WHead.N' YolyanComer2026.x✝) = some true ↔ waraoChi.Sat naote i

Fig. 4/5 agreement: the BMRS program (6) and the modal formula (7) compute the same nasality column on /naote/.

The translation (Def. 6) and its compositionality (Remark 7)

def YolyanComer2026.tr {α : Type u_1} {n : ℕ} : Subregular.Logic.ModalMu.Formula α n → Subregular.Logic.BMRS.Expr α (Fin n)

Def. 6: translate a vectorial modal formula into a BMRS expression whose rule heads are the recursion variables. Modalities substitute a moved term into the translated body; class-negated atoms translate by (3.8)-negation (the evident extension of the paper's clauses, which cover positive atoms).

Equations

• YolyanComer2026.tr Subregular.Logic.ModalMu.Formula.tru = Subregular.Logic.BMRS.Expr.tru
• YolyanComer2026.tr Subregular.Logic.ModalMu.Formula.fls = Subregular.Logic.BMRS.Expr.fls
• YolyanComer2026.tr Subregular.Logic.ModalMu.Formula.initial = Subregular.Logic.BMRS.Expr.initial YolyanComer2026.x✝
• YolyanComer2026.tr Subregular.Logic.ModalMu.Formula.final = Subregular.Logic.BMRS.Expr.final YolyanComer2026.x✝
• YolyanComer2026.tr (Subregular.Logic.ModalMu.Formula.label s) = Subregular.Logic.BMRS.Expr.label s YolyanComer2026.x✝
• YolyanComer2026.tr (Subregular.Logic.ModalMu.Formula.nlabel s) = (Subregular.Logic.BMRS.Expr.label s YolyanComer2026.x✝).ite Subregular.Logic.BMRS.Expr.fls Subregular.Logic.BMRS.Expr.tru
• YolyanComer2026.tr (Subregular.Logic.ModalMu.Formula.var X) = Subregular.Logic.BMRS.Expr.call X YolyanComer2026.x✝
• YolyanComer2026.tr (φ.and ψ) = (YolyanComer2026.tr φ).ite (YolyanComer2026.tr ψ) Subregular.Logic.BMRS.Expr.fls
• YolyanComer2026.tr (φ.or ψ) = (YolyanComer2026.tr φ).ite Subregular.Logic.BMRS.Expr.tru (YolyanComer2026.tr ψ)
• YolyanComer2026.tr φ.dia = (Subregular.Logic.BMRS.Expr.final YolyanComer2026.x✝).ite Subregular.Logic.BMRS.Expr.fls ((YolyanComer2026.tr φ).subst YolyanComer2026.x✝.succ)
• YolyanComer2026.tr φ.bdia = (Subregular.Logic.BMRS.Expr.initial YolyanComer2026.x✝).ite Subregular.Logic.BMRS.Expr.fls ((YolyanComer2026.tr φ).subst YolyanComer2026.x✝.pred)

def Subregular.Logic.ModalMu.System.trProgram {α : Type u_1} {n : ℕ} (χ : System α n) : BMRS.Program α (Fin n)

The translated program of a system: one rule per recursion variable.

Equations

• χ.trProgram X = YolyanComer2026.tr (χ.eqs X)

theorem YolyanComer2026.eval_tr {α : Type u_1} {n : ℕ} [DecidableEq α] {P : Subregular.Logic.BMRS.Program α (Fin n)} {w : Subregular.Logic.WordModel α} {U : Fin n → Set ℕ} [(X : Fin n) → DecidablePred fun (x : ℕ) => x ∈ U X] (hcall : ∀ (X : Fin n), ∀ j < List.length w, Subregular.Logic.BMRS.Eval P w j (Subregular.Logic.BMRS.Expr.call X YolyanComer2026.x✝) (decide (j ∈ U X))) (φ : Subregular.Logic.ModalMu.Formula α n) {i : ℕ} : i < List.length w → Subregular.Logic.BMRS.Eval P w i (tr φ) (decide (Subregular.Logic.ModalMu.Formula.Realize w U i φ))

Remark 7 (compositionality of the translation): wherever rule-head calls agree with the recursion variables, tr φ evaluates to the truth value of φ. Thm. 8's SCC induction discharges the hypothesis for directed systems.

theorem YolyanComer2026.warao_tr_agreement (i : ℕ) (hi : i < 5) : Subregular.Logic.BMRS.Eval waraoChi.trProgram naote i (tr (waraoChi.eqs 0)) (decide (Subregular.Logic.ModalMu.Formula.Realize naote waraoU i (waraoChi.eqs 0)))

Remark 7 run end-to-end on Warao: the translated program agrees with the modal semantics on /naote/ (waraoU = waraoChi.sem naote by warao_sem), the rule-head hypothesis discharged by direct computation — the concrete shape of Thm. 8.