Yolyan and Comer (2026): Phonological Processes as Modal Transductions

Yolyan and Comer translate the modal μ-calculus on words into the Boolean monadic recursive schemes of Bhaskar, Jardine, Chandlee and Oakden (Subregular.BMRS). Their main result (Thm. 2) is that total BMRS programs and Kozen's μ-calculus express the same unary properties of words, which gives an alternative proof that order-preserving BMRS interpretations capture the rational functions. Formula and System are the vectorial presentation of §4: a finite system of equations Xⱼ = θⱼ whose semantics is the least fixed point of the induced monotone operator on valuations. The translation tr (Def. 6) sends a right-hand side to a BMRS expression whose rule heads are the recursion variables, and eval_tr is its compositionality (Remark 7): wherever the rule-head calls agree with the recursion variables, tr φ evaluates to the truth value of φ.

The paper's two worked examples run through both formalisms. Vowel nasalization, (2)–(4), is non-recursive: nasalization is the program (3) and nasalizationChi the modal form (4), and both mark the vowel of /bæn/ before the nasal (Fig. 3). Progressive nasal spreading in Warao, (5)–(7), after Osborn, recurses under the backward modality: warao is the program (6), waraoChi the modal form (7), and the two agree on the Fig. 4 and Fig. 5 columns of /naote/ (warao_agreement). Fig. 4 is the rounds of evaluating (6) (warao_rounds). Footnote 2 notes that (3) ignores the word edge, so (3) has no value at a word-final vowel, while the edge-guarded program is total (not_totalOn_nasalization, nasalizationGuarded_totalOn). warao_tr_agreement runs Remark 7 on the translated Warao program, with the rule-head hypothesis discharged by computation.

Implementation notes

• Formulas are the negation-free fragment μMLf+ of Thm. 8, extended with negated label atoms (nlabel); negation stays off the recursion variables, so monotonicity of the system operator is structural, while the Warao formula N′ = μX.(N ∨ (¬T ∧ ♦X)) is expressible. Negated atoms translate as an if–then–else, the evident extension of the paper's clauses.
• Label atoms test the current symbol against a Finset class, since the paper's feature predicates N, V and T overlap (a nasalized vowel satisfies both V and N).
• The vectorial semantics is the least fixed point of the system operator by Knaster–Tarski, which by Bekić's theorem agrees with nested μ-binders.

TODO

• Thm. 8, the translation of directed systems (Def. 3) by induction on the strongly connected components of the dependency graph, which discharges the hypothesis of eval_tr.
• The converse containment of Thm. 2 runs through monadic second-order logic and needs an MSO substrate.

References

• [YC26]
• [BCJO20]
• [Koz83]
• [Osb66]

The vectorial modal μ-calculus on words (§4)

inductive YolyanComer2026.Formula (α : Type u_2) (n : ℕ) : Type u_2

Quantifier-free modal formulas over labels α and n recursion variables, negation-free apart from the class atoms nlabel, so that recursion variables occur only positively. label and nlabel test the current position's symbol against a Finset class; initial and final are the edge tests min and max; dia (◇) reads the successor position and bdia (♦) the predecessor.

• tru {α : Type u_2} {n : ℕ} : Formula α n
• fls {α : Type u_2} {n : ℕ} : Formula α n
• initial {α : Type u_2} {n : ℕ} : Formula α n
• final {α : Type u_2} {n : ℕ} : Formula α n
• label {α : Type u_2} {n : ℕ} (s : Finset α) : Formula α n
• nlabel {α : Type u_2} {n : ℕ} (s : Finset α) : Formula α n
• var {α : Type u_2} {n : ℕ} (X : Fin n) : Formula α n
• and {α : Type u_2} {n : ℕ} (φ ψ : Formula α n) : Formula α n
• or {α : Type u_2} {n : ℕ} (φ ψ : Formula α n) : Formula α n
• dia {α : Type u_2} {n : ℕ} (φ : Formula α n) : Formula α n
• bdia {α : Type u_2} {n : ℕ} (φ : Formula α n) : Formula α n

def YolyanComer2026.instDecidableEqFormula.decEq {α✝ : Type u_2} {n✝ : ℕ} [DecidableEq α✝] (x✝ x✝¹ : Formula α✝ n✝) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance YolyanComer2026.instDecidableEqFormula {α✝ : Type u_2} {n✝ : ℕ} [DecidableEq α✝] : DecidableEq (Formula α✝ n✝)

Equations

• YolyanComer2026.instDecidableEqFormula = YolyanComer2026.instDecidableEqFormula.decEq

def YolyanComer2026.Formula.Realize {α : Type u_1} {n : ℕ} (w : List α) (U : Fin n → Set ℕ) : ℕ → Formula α n → Prop

Satisfaction at a pointed word (w, i) under a valuation U of the recursion variables.

Equations

• YolyanComer2026.Formula.Realize w U x✝ YolyanComer2026.Formula.tru = True
• YolyanComer2026.Formula.Realize w U x✝ YolyanComer2026.Formula.fls = False
• YolyanComer2026.Formula.Realize w U x✝ YolyanComer2026.Formula.initial = (x✝ = 0)
• YolyanComer2026.Formula.Realize w U x✝ YolyanComer2026.Formula.final = (x✝ + 1 = w.length)
• YolyanComer2026.Formula.Realize w U x✝ (YolyanComer2026.Formula.label s) = ∃ a ∈ s, w[x✝]? = some a
• YolyanComer2026.Formula.Realize w U x✝ (YolyanComer2026.Formula.nlabel s) = ∀ a ∈ s, w[x✝]? ≠ some a
• YolyanComer2026.Formula.Realize w U x✝ (YolyanComer2026.Formula.var X) = (x✝ ∈ U X)
• YolyanComer2026.Formula.Realize w U x✝ (φ.and ψ) = (YolyanComer2026.Formula.Realize w U x✝ φ ∧ YolyanComer2026.Formula.Realize w U x✝ ψ)
• YolyanComer2026.Formula.Realize w U x✝ (φ.or ψ) = (YolyanComer2026.Formula.Realize w U x✝ φ ∨ YolyanComer2026.Formula.Realize w U x✝ ψ)
• YolyanComer2026.Formula.Realize w U x✝ φ.dia = ∃ (j : ℕ), Subregular.succ? w x✝ = some j ∧ YolyanComer2026.Formula.Realize w U j φ
• YolyanComer2026.Formula.Realize w U x✝ φ.bdia = ∃ (j : ℕ), Subregular.pred? w x✝ = some j ∧ YolyanComer2026.Formula.Realize w U j φ

@[simp]

theorem YolyanComer2026.Formula.realize_tru {α : Type u_1} {n : ℕ} {w : List α} {U : Fin n → Set ℕ} {i : ℕ} : Realize w U i tru

@[simp]

theorem YolyanComer2026.Formula.realize_fls {α : Type u_1} {n : ℕ} {w : List α} {U : Fin n → Set ℕ} {i : ℕ} : ¬Realize w U i fls

@[simp]

theorem YolyanComer2026.Formula.realize_initial {α : Type u_1} {n : ℕ} {w : List α} {U : Fin n → Set ℕ} {i : ℕ} : Realize w U i initial ↔ i = 0

@[simp]

theorem YolyanComer2026.Formula.realize_final {α : Type u_1} {n : ℕ} {w : List α} {U : Fin n → Set ℕ} {i : ℕ} : Realize w U i final ↔ i + 1 = w.length

@[simp]

theorem YolyanComer2026.Formula.realize_label {α : Type u_1} {n : ℕ} {w : List α} {U : Fin n → Set ℕ} {i : ℕ} {s : Finset α} : Realize w U i (label s) ↔ ∃ a ∈ s, w[i]? = some a

@[simp]

theorem YolyanComer2026.Formula.realize_nlabel {α : Type u_1} {n : ℕ} {w : List α} {U : Fin n → Set ℕ} {i : ℕ} {s : Finset α} : Realize w U i (nlabel s) ↔ ∀ a ∈ s, w[i]? ≠ some a

@[simp]

theorem YolyanComer2026.Formula.realize_var {α : Type u_1} {n : ℕ} {w : List α} {U : Fin n → Set ℕ} {i : ℕ} {X : Fin n} : Realize w U i (var X) ↔ i ∈ U X

@[simp]

theorem YolyanComer2026.Formula.realize_and {α : Type u_1} {n : ℕ} {w : List α} {U : Fin n → Set ℕ} {i : ℕ} {φ ψ : Formula α n} : Realize w U i (φ.and ψ) ↔ Realize w U i φ ∧ Realize w U i ψ

@[simp]

theorem YolyanComer2026.Formula.realize_or {α : Type u_1} {n : ℕ} {w : List α} {U : Fin n → Set ℕ} {i : ℕ} {φ ψ : Formula α n} : Realize w U i (φ.or ψ) ↔ Realize w U i φ ∨ Realize w U i ψ

@[simp]

theorem YolyanComer2026.Formula.realize_dia {α : Type u_1} {n : ℕ} {w : List α} {U : Fin n → Set ℕ} {i : ℕ} {φ : Formula α n} : Realize w U i φ.dia ↔ ∃ (j : ℕ), Subregular.succ? w i = some j ∧ Realize w U j φ

@[simp]

theorem YolyanComer2026.Formula.realize_bdia {α : Type u_1} {n : ℕ} {w : List α} {U : Fin n → Set ℕ} {i : ℕ} {φ : Formula α n} : Realize w U i φ.bdia ↔ ∃ (j : ℕ), Subregular.pred? w i = some j ∧ Realize w U j φ

@[instance_reducible]

instance YolyanComer2026.Formula.instDecidableRealize {α : Type u_1} {n : ℕ} [DecidableEq α] (w : List α) (U : Fin n → Set ℕ) [(X : Fin n) → DecidablePred fun (x : ℕ) => x ∈ U X] (i : ℕ) (φ : Formula α n) : Decidable (Realize w U i φ)

Equations

• One or more equations did not get rendered due to their size.
• YolyanComer2026.Formula.instDecidableRealize w U x✝ YolyanComer2026.Formula.tru = isTrue trivial
• YolyanComer2026.Formula.instDecidableRealize w U x✝ YolyanComer2026.Formula.fls = isFalse not_false
• YolyanComer2026.Formula.instDecidableRealize w U x✝ YolyanComer2026.Formula.initial = { decide := x✝.beq 0, reflects_decide := ⋯ }
• YolyanComer2026.Formula.instDecidableRealize w U x✝ YolyanComer2026.Formula.final = { decide := (x✝ + 1).beq w.length, reflects_decide := ⋯ }
• YolyanComer2026.Formula.instDecidableRealize w U x✝ (YolyanComer2026.Formula.label s) = { decide := decide (∃ (a : α) (_ : a ∈ s), (fun (a : α) => w[x✝]? = some a) a), reflects_decide := ⋯ }
• YolyanComer2026.Formula.instDecidableRealize w U x✝ (YolyanComer2026.Formula.var X) = YolyanComer2026.Formula.instDecidableRealize._aux_5 w U x✝ X
• YolyanComer2026.Formula.instDecidableRealize w U x✝ (φ.and ψ) = instDecidableAnd
• YolyanComer2026.Formula.instDecidableRealize w U x✝ (φ.or ψ) = instDecidableOr
• YolyanComer2026.Formula.instDecidableRealize w U x✝ φ.dia = match h : Subregular.succ? w x✝ with | none => isFalse ⋯ | some j => decidable_of_iff (YolyanComer2026.Formula.Realize w U j φ) ⋯
• YolyanComer2026.Formula.instDecidableRealize w U x✝ φ.bdia = match h : Subregular.pred? w x✝ with | none => isFalse ⋯ | some j => decidable_of_iff (YolyanComer2026.Formula.Realize w U j φ) ⋯

theorem YolyanComer2026.Formula.Realize.mono {α : Type u_1} {n : ℕ} {w : List α} {U V : Fin n → Set ℕ} (hUV : U ≤ V) {φ : Formula α n} {i : ℕ} : Realize w U i φ → Realize w V i φ

Satisfaction is monotone in the valuation, since recursion variables occur only positively.

structure YolyanComer2026.System (α : Type u_2) (n : ℕ) : Type u_2

A vectorial formula is a finite system of equations Xⱼ = θⱼ with a designated variable.

• eqs : Fin n → Formula α n

  The right-hand side of each equation.

• out : Fin n

  The designated variable whose satisfaction is the system's.

def YolyanComer2026.System.op {α : Type u_1} {n : ℕ} (χ : System α n) (w : List α) : (Fin n → Set ℕ) →o Fin n → Set ℕ

The monotone operator a system induces on valuations.

Equations

• χ.op w = { toFun := fun (U : Fin n → Set ℕ) (X : Fin n) => {i : ℕ | YolyanComer2026.Formula.Realize w U i (χ.eqs X)}, monotone' := ⋯ }

@[simp]

theorem YolyanComer2026.System.mem_op {α : Type u_1} {n : ℕ} (χ : System α n) (w : List α) {U : Fin n → Set ℕ} {X : Fin n} {i : ℕ} : i ∈ (χ.op w) U X ↔ Formula.Realize w U i (χ.eqs X)

noncomputable def YolyanComer2026.System.sem {α : Type u_1} {n : ℕ} (χ : System α n) (w : List α) : Fin n → Set ℕ

The least-fixed-point valuation.

Equations

• χ.sem w = OrderHom.lfp (χ.op w)

theorem YolyanComer2026.System.op_sem {α : Type u_1} {n : ℕ} (χ : System α n) (w : List α) : (χ.op w) (χ.sem w) = χ.sem w

sem is a fixed point of the system operator.

theorem YolyanComer2026.System.sem_le {α : Type u_1} {n : ℕ} (χ : System α n) (w : List α) {U : Fin n → Set ℕ} (hU : (χ.op w) U ≤ U) : χ.sem w ≤ U

sem is below every prefixed point.

def YolyanComer2026.System.Sat {α : Type u_1} {n : ℕ} (χ : System α n) (w : List α) (i : ℕ) : Prop

w, i ⊨ χ holds when the designated variable holds at i in the least fixed point.

Equations

• χ.Sat w i = (i ∈ χ.sem w χ.out)

@[reducible, inline]

abbrev YolyanComer2026.x : Subregular.Walk

The single BMRS index variable.

Equations

• YolyanComer2026.x = Subregular.Walk.var

Segments and feature classes

inductive YolyanComer2026.Seg : Type

Segments occurring in the paper's examples.

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

@[instance_reducible]

instance YolyanComer2026.instDecidableEqSeg : DecidableEq Seg

Equations

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

@[instance_reducible]

instance YolyanComer2026.instReprSeg : Repr Seg

Equations

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

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✝

def YolyanComer2026.nas : Finset Seg

The nasals, N.

Equations

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

def YolyanComer2026.vow : Finset Seg

The vowels, V.

Equations

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

def YolyanComer2026.stop : Finset Seg

The voiceless stops, T, which block spreading.

Equations

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

def YolyanComer2026.naote : List 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 : List 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

@[instance_reducible]

instance YolyanComer2026.instDecidableEqNasHead : DecidableEq NasHead

Equations

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

@[instance_reducible]

instance YolyanComer2026.instFintypeNasHead : Fintype NasHead

Equations

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

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

The nasalization program (3), V′(x) = V(x) and 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.BMRS.Expr.label YolyanComer2026.vow YolyanComer2026.x

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

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

theorem YolyanComer2026.not_totalOn_nasalization : ¬nasalization.TotalOn [Seg.b, Seg.a]

Program (3) ignores the word edge (footnote 2), so at a word-final vowel, where s(x) denotes nothing, N′ has no value.

def YolyanComer2026.nasalizationGuarded : Subregular.BMRS.Program Seg NasHead

The edge-guarded program of footnote 2, with N′(x) = if V(x) then (if max(x) then N(x) else N(s(x))) else N(x).

Equations

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

theorem YolyanComer2026.nasalizationGuarded_totalOn (w : List Seg) : nasalizationGuarded.TotalOn w

The edge-guarded program is total on every word, testing max before reading the successor.

def YolyanComer2026.nasalizationChi : System Seg 1

The modal form (4), N′ = (V ∧ ◇N) ∨ N, which is not recursive.

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

@[instance_reducible]

instance YolyanComer2026.instDecidableEqWHead : DecidableEq WHead

Equations

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

@[instance_reducible]

instance YolyanComer2026.instFintypeWHead : Fintype WHead

Equations

• YolyanComer2026.instFintypeWHead = { elems := { val := ↑YolyanComer2026.WHead.enumList, nodup := YolyanComer2026.WHead.enumList_nodup }, complete := YolyanComer2026.instFintypeWHead._proof_1 }

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

The spreading program (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.

Equations

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

theorem YolyanComer2026.warao_rounds : List.map (warao.approx naote 1 WHead.N') (List.range 5) = [some true, none, none, some false, none] ∧ List.map (warao.approx naote 2 WHead.N') (List.range 5) = [some true, some true, none, some false, some false] ∧ List.map (warao.approx naote 3 WHead.N') (List.range 5) = [some true, some true, some true, some false, some false] ∧ List.map (fun (i : ℕ) => warao.eval naote i (Subregular.BMRS.Expr.call WHead.N' x)) (List.range 5) = [some true, some true, some true, some false, some false]

Fig. 4, the rounds of evaluating (6) on /naote/. The first round values N′ at the nasal and at the stop, the second at the positions after them, and the third at position 2, reaching the output column N′ = ⊤⊤⊤⊥⊥, [nãõte], with spreading blocked by the t.

def YolyanComer2026.waraoChi : System Seg 1

The modal form (7), 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/, where 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

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

theorem YolyanComer2026.warao_agreement (i : ℕ) (hi : i < 5) : Subregular.BMRS.Eval warao naote i (Subregular.BMRS.Expr.call WHead.N' x) true ↔ waraoChi.Sat naote i

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

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

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

The translation of Def. 6 sends a vectorial modal formula to a BMRS expression whose rule heads are the recursion variables. Modalities substitute a moved term into the translated body, and the connectives are the if…then…else forms of footnote 3.

Equations

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

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

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

Equations

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

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

The translation is compositional (Remark 7). Wherever rule-head calls agree with the recursion variables, tr φ evaluates to the truth value of φ.

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

On Warao the translated program agrees with the modal semantics on /naote/ (waraoU is waraoChi.sem naote by warao_sem), the rule-head hypothesis discharged by computation.