Bimachines

A Bimachine ([Sch61]; [Eil74]) reads its input in both directions: a left automaton scans →, a right automaton scans ←, and output i is output (lState (x.take i)) (x i) (rState (x.drop (i+1))). Word-output bimachines compute exactly the rational functions ([EM65]; they are the transducers of [Sch76]'s semi-monomial representations, see [Sak09]); the letter-to-letter machines here compute the total length-preserving ones.

Main definitions

• Bimachine L R α β: machine with left states L, right states R, alphabets α, β
• Bimachine.run: the computed function
• IsBimachineComputable f: f is computed by some finite bimachine

Main theorems

• Bimachine.getElem?_run: output i is output (lState (x.take i)) (x i) (rState (x.drop (i+1)))

Implementation notes

Only the left state is threaded through the run (Bimachine.runFrom); the recursion reads each tail's right state on the spot. The class existentials pin state types at Type 0; the universe-polymorphic isBimachineComputable_iff recovers generality. The identification of IsBimachineComputable with the total rational functions preserving the empty word is classical and not formalized here; ElgotMezei.lean proves the composition half.

[UPSTREAM] candidate: Mathlib.Computability.Bimachine.

structure 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 is a left automaton scanning left to right, a right automaton scanning right to left, and a cell output reading both context states and the current symbol.

• lInit : L

  Starting state of the left automaton.

• lStep : L → α → L

  Transition of the left automaton, scanning left to right.

• rInit : R

  Starting state of the right automaton.

• rStep : R → α → R

  Transition of the right automaton, scanning right to left.

• output : L → α → R → List β

  The word emitted from the two context states and the current input symbol.

@[instance_reducible]

instance instInhabitedBimachine {L : Type u_1} {R : Type u_2} {α : Type u_3} {β : Type u_4} [Inhabited L] [Inhabited R] : Inhabited (Bimachine L R α β)

Equations

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

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

B.lStateAfter l pre is the left state reached from l after scanning pre.

Equations

• B.lStateAfter l = List.foldl B.lStep l

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

Left state after scanning a prefix left-to-right from the start state.

Equations

• B.lState = B.lStateAfter B.lInit

def 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

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

B.runFrom l x runs B on x threading the left state from l; each tail's right state is read on the spot.

Equations

• B.runFrom x✝ [] = []
• B.runFrom x✝ (x_2 :: xs) = B.output x✝ x_2 (B.rState xs) ++ B.runFrom (B.lStep x✝ x_2) xs

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

The computed function.

Equations

• B.run = B.runFrom B.lInit

@[simp]

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

@[simp]

theorem Bimachine.lStateAfter_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.lStateAfter l (x :: xs) = B.lStateAfter (B.lStep l x) xs

@[simp]

theorem 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

@[simp]

theorem 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

@[simp]

theorem Bimachine.rState_cons {L : Type u_1} {R : Type u_2} {α : Type u_3} {β : Type u_4} (B : Bimachine L R α β) (x : α) (xs : List α) : B.rState (x :: xs) = B.rStep (B.rState xs) x

@[simp]

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

@[simp]

theorem Bimachine.runFrom_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.runFrom l (x :: xs) = B.output l x (B.rState xs) ++ B.runFrom (B.lStep l x) xs

Letter-to-letter bimachines

A cell of a general bimachine emits a word, so the run is a concatenation and output positions need not track input positions. A letter-to-letter bimachine emits exactly one symbol per cell ([Sak09] §IV.6); the function it computes is then length-preserving, and the positional description below holds.

structure Bimachine.LetterToLetter {L : Type u_1} {R : Type u_2} {α : Type u_3} {β : Type u_4} (B : Bimachine L R α β) : Type (max (max (max u_1 u_2) u_3) u_4)

A witness that B is letter-to-letter: every cell emits exactly one symbol, named by cell.

• cell : L → α → R → β

  The single symbol emitted at a cell.

• output_eq (l : L) (a : α) (r : R) : B.output l a r = [self.cell l a r]

  Every cell emits exactly that one symbol.

def Bimachine.IsLetterToLetter {L : Type u_1} {R : Type u_2} {α : Type u_3} {β : Type u_4} (B : Bimachine L R α β) : Prop

B is letter-to-letter when it admits a LetterToLetter witness.

Equations

• B.IsLetterToLetter = Nonempty B.LetterToLetter

@[simp]

theorem Bimachine.LetterToLetter.length_runFrom {L : Type u_1} {R : Type u_2} {α : Type u_3} {β : Type u_4} {B : Bimachine L R α β} (w : B.LetterToLetter) (l : L) (xs : List α) : (B.runFrom l xs).length = xs.length

The run of a letter-to-letter bimachine has the length of its input.

@[simp]

theorem Bimachine.LetterToLetter.length_run {L : Type u_1} {R : Type u_2} {α : Type u_3} {β : Type u_4} {B : Bimachine L R α β} (w : B.LetterToLetter) (xs : List α) : (B.run xs).length = xs.length

theorem Bimachine.LetterToLetter.getElem?_runFrom {L : Type u_1} {R : Type u_2} {α : Type u_3} {β : Type u_4} {B : Bimachine L R α β} (w : B.LetterToLetter) (l : L) (xs : List α) (i : ℕ) : (B.runFrom l xs)[i]? = Option.map (fun (a : α) => w.cell (B.lStateAfter l (List.take i xs)) a (B.rState (List.drop (i + 1) xs))) xs[i]?

Output coordinate i reads the left state after the length-i prefix and the right state of the strict suffix.

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

Output i is cell (lState (x.take i)) (x i) (rState (x.drop (i+1))).

Transport along state equivalences

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

Transport a bimachine along equivalences on the two state spaces.

Equations

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

@[simp]

theorem Bimachine.map_lStep {L : Type u_1} {R : Type u_2} {α : Type u_3} {β : Type u_4} {L' : Type u_5} {R' : Type u_6} (eL : L ≃ L') (eR : R ≃ R') (B : Bimachine L R α β) (l : L') (a : α) : (map eL eR B).lStep l a = eL (B.lStep (eL.symm l) a)

@[simp]

theorem Bimachine.map_output {L : Type u_1} {R : Type u_2} {α : Type u_3} {β : Type u_4} {L' : Type u_5} {R' : Type u_6} (eL : L ≃ L') (eR : R ≃ R') (B : Bimachine L R α β) (l : L') (a : α) (r : R') : (map eL eR B).output l a r = B.output (eL.symm l) a (eR.symm r)

@[simp]

theorem Bimachine.map_lInit {L : Type u_1} {R : Type u_2} {α : Type u_3} {β : Type u_4} {L' : Type u_5} {R' : Type u_6} (eL : L ≃ L') (eR : R ≃ R') (B : Bimachine L R α β) : (map eL eR B).lInit = eL B.lInit

@[simp]

theorem Bimachine.map_rInit {L : Type u_1} {R : Type u_2} {α : Type u_3} {β : Type u_4} {L' : Type u_5} {R' : Type u_6} (eL : L ≃ L') (eR : R ≃ R') (B : Bimachine L R α β) : (map eL eR B).rInit = eR B.rInit

@[simp]

theorem Bimachine.map_rStep {L : Type u_1} {R : Type u_2} {α : Type u_3} {β : Type u_4} {L' : Type u_5} {R' : Type u_6} (eL : L ≃ L') (eR : R ≃ R') (B : Bimachine L R α β) (r : R') (a : α) : (map eL eR B).rStep r a = eR (B.rStep (eR.symm r) a)

@[simp]

theorem Bimachine.map_refl {L : Type u_1} {R : Type u_2} {α : Type u_3} {β : Type u_4} (B : Bimachine L R α β) : map (Equiv.refl L) (Equiv.refl R) B = B

@[simp]

theorem Bimachine.map_map {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} {L'' : Type u_7} {R'' : Type u_8} (eL : L ≃ L') (eR : R ≃ R') (eL' : L' ≃ L'') (eR' : R' ≃ R'') : map eL' eR' (map eL eR B) = map (eL.trans eL') (eR.trans eR') B

@[simp]

theorem Bimachine.lStateAfter_map {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 α) : (map eL eR B).lStateAfter l' pre = eL (B.lStateAfter (eL.symm l') pre)

@[simp]

theorem Bimachine.lState_map {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 α) : (map eL eR B).lState pre = eL (B.lState pre)

@[simp]

theorem Bimachine.rState_map {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 α) : (map eL eR B).rState suf = eR (B.rState suf)

@[simp]

theorem Bimachine.runFrom_map {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 α) : (map eL eR B).runFrom l' xs = B.runFrom (eL.symm l') xs

@[simp]

theorem Bimachine.run_map {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') : (map eL eR B).run = B.run

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

map as an equivalence of bimachines.

Equations

• Bimachine.reindex eL eR = { toFun := Bimachine.map eL eR, invFun := Bimachine.map eL.symm eR.symm, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Bimachine.coe_reindex {L : Type u_1} {R : Type u_2} {α : Type u_3} {β : Type u_4} {L' : Type u_5} {R' : Type u_6} (eL : L ≃ L') (eR : R ≃ R') : ⇑(reindex eL eR) = map eL eR

@[simp]

theorem Bimachine.symm_reindex {L : Type u_1} {R : Type u_2} {α : Type u_3} {β : Type u_4} {L' : Type u_5} {R' : Type u_6} (eL : L ≃ L') (eR : R ≃ R') : (reindex eL eR).symm = reindex eL.symm eR.symm

theorem Bimachine.LetterToLetter.cell_inj {L : Type u_1} {R : Type u_2} {α : Type u_3} {β : Type u_4} {B : Bimachine L R α β} (w : B.LetterToLetter) {l l' : L} {a a' : α} {r r' : R} : w.cell l a r = w.cell l' a' r' ↔ B.output l a r = B.output l' a' r'

Cells agree exactly when the underlying word-valued outputs do.

def Bimachine.LetterToLetter.map {L : Type u_1} {R : Type u_2} {α : Type u_3} {β : Type u_4} {L' : Type u_7} {R' : Type u_8} {B : Bimachine L R α β} (w : B.LetterToLetter) (eL : L ≃ L') (eR : R ≃ R') : (Bimachine.map eL eR B).LetterToLetter

Letter-to-letter-ness transports along state reindexing.

Equations

• w.map eL eR = { cell := fun (l : L') (a : α) (r : R') => w.cell (eL.symm l) a (eR.symm r), output_eq := ⋯ }

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. The conjunctive witness conjBM below is an instance.

def 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

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

@[simp]

theorem Bimachine.ofFlags_lInit {α : Type u_3} {β : Type u_4} (pL pR : α → Bool) (out : Bool → α → Bool → β) : (ofFlags pL pR out).lInit = false

@[simp]

theorem Bimachine.ofFlags_lStep {α : Type u_3} {β : Type u_4} (pL pR : α → Bool) (out : Bool → α → Bool → β) (l : Bool) (a : α) : (ofFlags pL pR out).lStep l a = (l || pL a)

@[simp]

theorem Bimachine.ofFlags_rInit {α : Type u_3} {β : Type u_4} (pL pR : α → Bool) (out : Bool → α → Bool → β) : (ofFlags pL pR out).rInit = false

@[simp]

theorem Bimachine.ofFlags_rStep {α : Type u_3} {β : Type u_4} (pL pR : α → Bool) (out : Bool → α → Bool → β) (r : Bool) (a : α) : (ofFlags pL pR out).rStep r a = (r || pR a)

@[simp]

theorem Bimachine.ofFlags_output {α : Type u_3} {β : Type u_4} (pL pR : α → Bool) (out : Bool → α → Bool → β) (l : Bool) (a : α) (r : Bool) : (ofFlags pL pR out).output l a r = [out l a r]

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

A flag bimachine is letter-to-letter, with out as its cell.

Equations

• Bimachine.ofFlags_letterToLetter pL pR out = { cell := out, output_eq := ⋯ }

@[simp]

theorem Bimachine.ofFlags_lStateAfter {α : Type u_3} {β : Type u_4} (pL pR : α → Bool) (out : Bool → α → Bool → β) (l : Bool) (xs : List α) : (ofFlags pL pR out).lStateAfter l xs = (l || xs.any pL)

@[simp]

theorem 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 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 Bimachine.getElem?_ofFlags_run {α : 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]?

Output i of a flag bimachine sees the input symbol and the two window-any flags.

Sequential machines as bimachines

def Mealy.toBimachine {α : Type u_3} {β : Type u_4} {σ : Type u_5} (T : Mealy σ α β) : Bimachine σ Unit α β

A sequential machine as the bimachine whose left automaton does all the work and whose right automaton is trivial.

Equations

• T.toBimachine = { lInit := T.initial, lStep := T.step, rInit := (), rStep := fun (x : Unit) (x_1 : α) => (), output := fun (l : σ) (a : α) (x : Unit) => [T.output l a] }

@[simp]

theorem Mealy.toBimachine_lInit {α : Type u_3} {β : Type u_4} {σ : Type u_5} (T : Mealy σ α β) : T.toBimachine.lInit = T.initial

@[simp]

theorem Mealy.toBimachine_rStep {α : Type u_3} {β : Type u_4} {σ : Type u_5} (T : Mealy σ α β) (x✝ : Unit) (x✝¹ : α) : T.toBimachine.rStep x✝ x✝¹ = ()

@[simp]

theorem Mealy.toBimachine_rInit {α : Type u_3} {β : Type u_4} {σ : Type u_5} (T : Mealy σ α β) : T.toBimachine.rInit = ()

@[simp]

theorem Mealy.toBimachine_output {α : Type u_3} {β : Type u_4} {σ : Type u_5} (T : Mealy σ α β) (l : σ) (a : α) (x✝ : Unit) : T.toBimachine.output l a x✝ = [T.output l a]

@[simp]

theorem Mealy.toBimachine_lStep {α : Type u_3} {β : Type u_4} {σ : Type u_5} (T : Mealy σ α β) (a✝ : σ) (a✝¹ : α) : T.toBimachine.lStep a✝ a✝¹ = T.step a✝ a✝¹

@[simp]

theorem Mealy.toBimachine_runFrom {α : Type u_3} {β : Type u_4} {σ : Type u_5} (T : Mealy σ α β) (s : σ) (xs : List α) : T.toBimachine.runFrom s xs = T.runFrom s xs

@[simp]

theorem Mealy.toBimachine_run {α : Type u_3} {β : Type u_4} {σ : Type u_5} (T : Mealy σ α β) : T.toBimachine.run = T.run

The bimachine view computes the same string function.

The bimachine-computable class

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

Computability by a finite bimachine — classically, the total rational functions preserving the empty word.

Equations

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

theorem isBimachineComputable_iff {α : Type u_3} {β : Type u_4} {f : List α → List β} : IsBimachineComputable f ↔ ∃ (L : Type v) (x : Fintype L) (R : Type w) (x : Fintype R) (B : Bimachine L R α β), B.run = f

f is bimachine-computable if and only if it is computed by a finite bimachine with state types in any universes.

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

Every finite-state bimachine computes a bimachine-computable function, whatever the universes of its state types.

def IsLengthPreservingBimachineComputable {α : Type u_3} {β : Type u_4} (f : List α → List β) : Prop

Computability by a finite letter-to-letter bimachine: the total length-preserving rational functions.

Equations

• IsLengthPreservingBimachineComputable f = ∃ (L : Type) (x : Fintype L) (R : Type) (x : Fintype R) (B : Bimachine L R α β), B.IsLetterToLetter ∧ B.run = f

theorem isLengthPreservingBimachineComputable_iff {α : Type u_3} {β : Type u_4} {f : List α → List β} : IsLengthPreservingBimachineComputable f ↔ ∃ (L : Type v) (x : Fintype L) (R : Type w) (x : Fintype R) (B : Bimachine L R α β), B.IsLetterToLetter ∧ B.run = f

f is computed by a finite letter-to-letter bimachine iff it is computed by one with state types in any universes.

theorem IsBimachineComputable.of_lengthPreserving {α : Type u_3} {β : Type u_4} {f : List α → List β} (h : IsLengthPreservingBimachineComputable f) : IsBimachineComputable f

A length-preserving bimachine-computable function is bimachine-computable.

theorem IsLengthPreservingBimachineComputable.length_eq {α : Type u_3} {β : Type u_4} {f : List α → List β} (h : IsLengthPreservingBimachineComputable f) (x : List α) : (f x).length = x.length

Functions computed by letter-to-letter bimachines are length-preserving.

theorem IsBimachineComputable.of_mealyComputable {α : Type u_3} {β : Type u_4} {f : List α → List β} (h : IsMealyComputable f) : IsBimachineComputable f

A Mealy-computable function is bimachine-computable (Mealy.toBimachine).