Bimachines and weak determinism

A Bimachine (Schützenberger; [Moh97]) computes a letter-to-letter string function using both directions of context: a left automaton scans → and assigns a left state to each position, a right automaton scans ← and assigns a right state, and the output at position i is out (leftState before i) (input i) (rightState after i).

A bimachine over a single alphabet is non-interacting when its output is a union of one-sided change-rules over the identity: each side may add its own change, but neither can suppress the other's. IsBimachineWeaklyDeterministic is computability by such a bimachine — the weakly-deterministic functions.

Main results

• Bimachine.run_getElem? — output i is out (lState (x.take i)) (x i) (rState (x.drop (i+1))).
• not_isBimachineWeaklyDeterministic_of_requiresBothSides — a map with an unbounded interaction (RequiresBothSides: the target is changed, yet perturbing either far side reverts it) is not weakly deterministic. The far perturbations force both one-sided rules inert at the witness cell while the base needs one to fire — no union of one-sided rules can produce the change. A conjunctive change satisfies it; a two-sided union does not.

structure Subregular.Bimachine (L : Type u_5) (R : Type u_6) (α : Type u_7) (β : Type u_8) : Type (max (max (max u_5 u_6) u_7) u_8)

A bimachine: a left automaton (lInit/lStep, scanning →), a right automaton (rInit/rStep, scanning ← over the suffix), and a cell output out reading both context states and the current symbol.

• lInit : L
• lStep : L → α → L
• rInit : R
• rStep : R → α → R
• out : L → α → R → β

def Subregular.Bimachine.lState {L : Type u_1} {R : Type u_2} {α : Type u_3} {β : Type u_4} (B : Bimachine L R α β) (pre : List α) : L

Left state after scanning a prefix left-to-right.

Equations

• B.lState pre = List.foldl B.lStep B.lInit pre

def Subregular.Bimachine.rState {L : Type u_1} {R : Type u_2} {α : Type u_3} {β : Type u_4} (B : Bimachine L R α β) (suf : List α) : R

Right state after scanning a suffix right-to-left.

Equations

• B.rState suf = List.foldr (fun (a : α) (r : R) => B.rStep r a) B.rInit suf

theorem Subregular.Bimachine.lState_nil {L : Type u_1} {R : Type u_2} {α : Type u_3} {β : Type u_4} (B : Bimachine L R α β) : B.lState [] = B.lInit

theorem Subregular.Bimachine.rState_nil {L : Type u_1} {R : Type u_2} {α : Type u_3} {β : Type u_4} (B : Bimachine L R α β) : B.rState [] = B.rInit

def Subregular.Bimachine.runAux {L : Type u_1} {R : Type u_2} {α : Type u_3} {β : Type u_4} (B : Bimachine L R α β) : L → List α → List β

Run threading the left state; each tail's right state is read on the spot.

Equations

• B.runAux x✝ [] = []
• B.runAux x✝ (x_2 :: xs) = B.out x✝ x_2 (B.rState xs) :: B.runAux (B.lStep x✝ x_2) xs

def Subregular.Bimachine.run {L : Type u_1} {R : Type u_2} {α : Type u_3} {β : Type u_4} (B : Bimachine L R α β) (x : List α) : List β

The computed function.

Equations

• B.run x = B.runAux B.lInit x

@[simp]

theorem Subregular.Bimachine.runAux_nil {L : Type u_1} {R : Type u_2} {α : Type u_3} {β : Type u_4} (B : Bimachine L R α β) (l : L) : B.runAux l [] = []

@[simp]

theorem Subregular.Bimachine.runAux_cons {L : Type u_1} {R : Type u_2} {α : Type u_3} {β : Type u_4} (B : Bimachine L R α β) (l : L) (x : α) (xs : List α) : B.runAux l (x :: xs) = B.out l x (B.rState xs) :: B.runAux (B.lStep l x) xs

theorem Subregular.Bimachine.runAux_length {L : Type u_1} {R : Type u_2} {α : Type u_3} {β : Type u_4} (B : Bimachine L R α β) (l : L) (xs : List α) : (B.runAux l xs).length = xs.length

theorem Subregular.Bimachine.run_length {L : Type u_1} {R : Type u_2} {α : Type u_3} {β : Type u_4} (B : Bimachine L R α β) (x : List α) : (B.run x).length = x.length

theorem Subregular.Bimachine.runAux_getElem? {L : Type u_1} {R : Type u_2} {α : Type u_3} {β : Type u_4} (B : Bimachine L R α β) (l : L) (xs : List α) (i : ℕ) : (B.runAux l xs)[i]? = Option.map (fun (a : α) => B.out (List.foldl B.lStep l (List.take i xs)) a (B.rState (List.drop (i + 1) xs))) xs[i]?

Coordinate characterization (threaded form).

theorem Subregular.Bimachine.run_getElem? {L : Type u_1} {R : Type u_2} {α : Type u_3} {β : Type u_4} (B : Bimachine L R α β) (x : List α) (i : ℕ) : (B.run x)[i]? = Option.map (fun (a : α) => B.out (B.lState (List.take i x)) a (B.rState (List.drop (i + 1) x))) x[i]?

Coordinate characterization: output i is out (lState (x.take i)) (x i) (rState (x.drop (i+1))).

def Subregular.Bimachine.transferEquiv {L : Type u_1} {R : Type u_2} {α : Type u_3} {β : Type u_4} (B : Bimachine L R α β) {L' : Type u_5} {R' : Type u_6} (eL : L ≃ L') (eR : R ≃ R') : Bimachine L' R' α β

Transfer a bimachine along state-space equivalences L ≃ L' and R ≃ R', preserving run. Mirrors SFST.transferEquiv/Mealy.transferEquiv; the use case is bringing Type* finite states down to Fin (Fintype.card ·) : Type 0 so a universe-polymorphic machine can witness the Type 0-state existentials of IsBimachineComputable/IsBimachineWeaklyDeterministic.

Equations

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

theorem Subregular.Bimachine.transferEquiv_lState_from {L : Type u_1} {R : Type u_2} {α : Type u_3} {β : Type u_4} (B : Bimachine L R α β) {L' : Type u_5} {R' : Type u_6} (eL : L ≃ L') (eR : R ≃ R') (l : L) (pre : List α) : List.foldl (B.transferEquiv eL eR).lStep (eL l) pre = eL (List.foldl B.lStep l pre)

theorem Subregular.Bimachine.transferEquiv_rState_from {L : Type u_1} {R : Type u_2} {α : Type u_3} {β : Type u_4} (B : Bimachine L R α β) {L' : Type u_5} {R' : Type u_6} (eL : L ≃ L') (eR : R ≃ R') (r : R) (suf : List α) : List.foldr (fun (a : α) (r : R') => (B.transferEquiv eL eR).rStep r a) (eR r) suf = eR (List.foldr (fun (a : α) (r : R) => B.rStep r a) r suf)

theorem Subregular.Bimachine.transferEquiv_lState {L : Type u_1} {R : Type u_2} {α : Type u_3} {β : Type u_4} (B : Bimachine L R α β) {L' : Type u_5} {R' : Type u_6} (eL : L ≃ L') (eR : R ≃ R') (pre : List α) : (B.transferEquiv eL eR).lState pre = eL (B.lState pre)

theorem Subregular.Bimachine.transferEquiv_rState {L : Type u_1} {R : Type u_2} {α : Type u_3} {β : Type u_4} (B : Bimachine L R α β) {L' : Type u_5} {R' : Type u_6} (eL : L ≃ L') (eR : R ≃ R') (suf : List α) : (B.transferEquiv eL eR).rState suf = eR (B.rState suf)

theorem Subregular.Bimachine.transferEquiv_runAux {L : Type u_1} {R : Type u_2} {α : Type u_3} {β : Type u_4} (B : Bimachine L R α β) {L' : Type u_5} {R' : Type u_6} (eL : L ≃ L') (eR : R ≃ R') (l : L) (xs : List α) : (B.transferEquiv eL eR).runAux (eL l) xs = B.runAux l xs

@[simp]

theorem Subregular.Bimachine.transferEquiv_run {L : Type u_1} {R : Type u_2} {α : Type u_3} {β : Type u_4} (B : Bimachine L R α β) {L' : Type u_5} {R' : Type u_6} (eL : L ≃ L') (eR : R ≃ R') : (B.transferEquiv eL eR).run = B.run

The transferred bimachine computes the same string function.

Flag bimachines

The recurring two-sided-trigger shape: each side's automaton is the one-bit "some symbol on my side satisfies p" flag, so lState/rState compute List.any and the cell sees exactly the two flags. Conjunctive spreads (conjBM in Hierarchy.lean) and unbounded tonal plateauing ([Jar16]) are instances.

def Subregular.Bimachine.ofFlags {α : Type u_3} {β : Type u_4} (pL pR : α → Bool) (out : Bool → α → Bool → β) : Bimachine Bool Bool α β

The bimachine whose side states are "a symbol satisfying pL/pR occurred on my side" flags.

Equations

• Subregular.Bimachine.ofFlags pL pR out = { lInit := false, lStep := fun (l : Bool) (a : α) => l || pL a, rInit := false, rStep := fun (r : Bool) (a : α) => r || pR a, out := out }

@[simp]

theorem Subregular.Bimachine.ofFlags_lState {α : Type u_3} {β : Type u_4} (pL pR : α → Bool) (out : Bool → α → Bool → β) (xs : List α) : (ofFlags pL pR out).lState xs = xs.any pL

@[simp]

theorem Subregular.Bimachine.ofFlags_rState {α : Type u_3} {β : Type u_4} (pL pR : α → Bool) (out : Bool → α → Bool → β) (xs : List α) : (ofFlags pL pR out).rState xs = xs.any pR

theorem Subregular.Bimachine.ofFlags_run_getElem? {α : Type u_3} {β : Type u_4} (pL pR : α → Bool) (out : Bool → α → Bool → β) (x : List α) (i : ℕ) : ((ofFlags pL pR out).run x)[i]? = Option.map (fun (a : α) => out ((List.take i x).any pL) a ((List.drop (i + 1) x).any pR)) x[i]?

Coordinate characterization of a flag bimachine: output i sees the input symbol and the two window-any flags.

Weak determinism

def Subregular.IsBimachineComputable {α : Type u_3} {β : Type u_4} (f : List α → List β) : Prop

Computability by a finite bimachine (the length-preserving regular functions).

Equations

• Subregular.IsBimachineComputable f = ∃ (L : Type) (R : Type) (x : Fintype L) (x : Fintype R) (B : Subregular.Bimachine L R α β), B.run = f

theorem Subregular.isBimachineComputable {L : Type u_5} {R : Type u_6} [Fintype L] [Fintype R] {α : Type u_7} {β : Type u_8} (B : Bimachine L R α β) : IsBimachineComputable B.run

Constructor lemma: every finite-state bimachine witnesses IsBimachineComputable for its run. States are accepted at arbitrary Type* and brought down to Fin (Fintype.card ·) : Type 0 via transferEquiv + Fintype.equivFin, so consumers stop spelling the ∃ (L R : Type) quadruple. Mirrors SFST.isLeftSubsequential.

The flank-witness template

The recurring witness family for two-sided unboundedness: a target buried in a filler run, with independently editable flanks. RequiresBothSides.of_flanks packages the whole assembly — a map is excluded by exhibiting only the images of the base and the two single-flank perturbations at the target. This is the three-map method of [Yol25] §5.3, as an object.

def Subregular.flankWord {α : Type u_5} (x fill y : α) (n : ℕ) : List α

A flank-controlled word: x, then n copies of fill, then y.

Equations

• Subregular.flankWord x fill y n = x :: (List.replicate n fill ++ [y])

@[simp]

theorem Subregular.flankWord_length {α : Type u_5} {x fill y : α} {n : ℕ} : (flankWord x fill y n).length = n + 2

theorem Subregular.flankWord_getElem? {α : Type u_5} {x fill y : α} {n k : ℕ} : (flankWord x fill y n)[k]? = if k = 0 then some x else if k = n + 1 then some y else if k < n + 2 then some fill else none

@[simp]

theorem Subregular.flankWord_getElem?_zero {α : Type u_5} {x fill y : α} {n : ℕ} : (flankWord x fill y n)[0]? = some x

@[simp]

theorem Subregular.flankWord_getElem?_last {α : Type u_5} {x fill y : α} {n : ℕ} : (flankWord x fill y n)[n + 1]? = some y

theorem Subregular.flankWord_getElem?_mid {α : Type u_5} {x fill y : α} {n k : ℕ} (h₁ : 0 < k) (h₂ : k ≤ n) : (flankWord x fill y n)[k]? = some fill

theorem Subregular.flankWord_getElem?_eq_some_iff {α : Type u_5} {x fill y a : α} {n j : ℕ} (hfill : fill ≠ a) : (flankWord x fill y n)[j]? = some a ↔ j = 0 ∧ x = a ∨ j = n + 1 ∧ y = a

A non-filler value sits only on a flank.

theorem Subregular.exists_le_flankWord_eq_some_iff {α : Type u_5} {x fill y a : α} {n k : ℕ} (hfill : fill ≠ a) (hk : k ≤ n) : (∃ j ≤ k, (flankWord x fill y n)[j]? = some a) ↔ x = a

A window reaching at most the filler run hits a iff the left flank is a.

theorem Subregular.exists_ge_flankWord_eq_some_iff {α : Type u_5} {x fill y a : α} {n k : ℕ} (hfill : fill ≠ a) (h0 : 0 < k) (hk : k ≤ n + 1) : (∃ j ≥ k, (flankWord x fill y n)[j]? = some a) ↔ y = a

A window past the left flank hits a iff the right flank is a.

theorem Subregular.flankWord_congr_left {α : Type u_5} {x fill y : α} {n k : ℕ} {x' : α} (h : k ≠ 0) : (flankWord x fill y n)[k]? = (flankWord x' fill y n)[k]?

Flank words differing only on the left agree off position 0.

theorem Subregular.flankWord_congr_right {α : Type u_5} {x fill y : α} {n k : ℕ} {y' : α} (h : k ≠ n + 1) : (flankWord x fill y n)[k]? = (flankWord x fill y' n)[k]?

Flank words differing only on the right agree off the last position.

def Subregular.RequiresBothSides {α : Type u_5} (f : List α → List α) : Prop

f requires both sides: some target changes under f, yet perturbing either far side reverts it to the identity. Unlike IsUnboundedCircumambient, a two-sided union never satisfies this — removing one trigger leaves the other, so the output stays changed.

Equations

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

theorem Subregular.RequiresBothSides.of_flanks {α : Type u_5} {f : List α → List α} {fill on xOn yOn xOff yOff : α} {n t : ℕ → ℕ} (hne : on ≠ fill) (hmargin : ∀ (d : ℕ), d < t d ∧ t d + d < n d + 1) (hchange : ∀ (d : ℕ), (f (flankWord xOn fill yOn (n d)))[t d]? = some on) (hrevL : ∀ (d : ℕ), (f (flankWord xOff fill yOn (n d)))[t d]? = some fill) (hrevR : ∀ (d : ℕ), (f (flankWord xOn fill yOff (n d)))[t d]? = some fill) : RequiresBothSides f

The three-map template: a d-indexed family of flank words whose target sits d-far from both flanks, changed to on in the base and reverted by flipping either flank alone, requires both sides.

theorem Subregular.RequiresBothSides.isUnboundedCircumambient {α : Type u_5} {f : List α → List α} (hf : RequiresBothSides f) : IsUnboundedCircumambient f

Requiring both sides strengthens unbounded circumambience: a reverted target is in particular a flipped one. The converse fails (a two-sided union is circumambient but reverts under neither side alone).

def Subregular.unite {α : Type u_7} [DecidableEq α] (cL cR a : α) : α

Combine two one-sided change proposals over the identity default a: take the left rule's change if it fires (≠ a), else the right rule's, else leave the symbol.

Equations

• Subregular.unite cL cR a = if cL = a then if cR = a then a else cR else cL

@[simp]

theorem Subregular.unite_self {α : Type u_7} [DecidableEq α] (a : α) : unite a a a = a

theorem Subregular.unite_eq_default {α : Type u_7} [DecidableEq α] {cL cR a : α} (h : unite cL cR a = a) : cL = a ∧ cR = a

A combined value equal to the default forces both one-sided proposals to be inert.

def Subregular.Bimachine.IsNonInteracting {L : Type u_5} {R : Type u_6} {α : Type u_7} [DecidableEq α] (B : Bimachine L R α α) : Prop

Non-interaction: the cell output is a union of one-sided change-rules over the identity default — ωL/ωR each propose a change for their side, and the output takes whichever fires, else leaves the symbol unchanged. Neither side can suppress the other's change; that asymmetry is exactly what interaction would require.

Equations

• B.IsNonInteracting = ∃ (ωL : L → α → α) (ωR : R → α → α), ∀ (l : L) (a : α) (r : R), B.out l a r = Subregular.unite (ωL l a) (ωR r a) a

def Subregular.IsBimachineWeaklyDeterministic {α : Type u_7} [DecidableEq α] (f : List α → List α) : Prop

Weak determinism: computability by a non-interacting finite bimachine.

Equations

• Subregular.IsBimachineWeaklyDeterministic f = ∃ (L : Type) (R : Type) (x : Fintype L) (x : Fintype R) (B : Subregular.Bimachine L R α α), B.run = f ∧ B.IsNonInteracting

theorem Subregular.isBimachineWeaklyDeterministic {α : Type u_7} [DecidableEq α] {L : Type u_8} {R : Type u_9} [Fintype L] [Fintype R] (B : Bimachine L R α α) (h : B.IsNonInteracting) : IsBimachineWeaklyDeterministic B.run

Constructor lemma: a non-interacting finite-state bimachine witnesses IsBimachineWeaklyDeterministic for its run. The one-sided rules survive the state-space transfer by composing with e.symm.

theorem Subregular.inert_of_reverting {L : Type u_5} {R : Type u_6} {α : Type u_7} [DecidableEq α] {B : Bimachine L R α α} {ωL : L → α → α} {ωR : R → α → α} (hω : ∀ (l : L) (a : α) (r : R), B.out l a r = unite (ωL l a) (ωR r a) a) {u : List α} {i : ℕ} {a : α} (hsym : u[i]? = some a) (hrev : (B.run u)[i]? = u[i]?) : ωL (B.lState (List.take i u)) a = a ∧ ωR (B.rState (List.drop (i + 1) u)) a = a

Under a non-interacting cell decomposition, a word whose run leaves target i unchanged has both of its change-proposals inert there.

theorem Subregular.not_isBimachineWeaklyDeterministic_of_requiresBothSides {α : Type u_7} [DecidableEq α] {f : List α → List α} (hf : RequiresBothSides f) : ¬IsBimachineWeaklyDeterministic f

Unbounded interaction ⟹ not weakly deterministic. At the witness, the base changes but each far perturbation reverts: the right perturbation keeps the left state, forcing ωL inert at this cell; the left perturbation keeps the right state, forcing ωR inert; yet the base needs one of them to fire — no union of one-sided rules can produce the change.