Deterministic finite automata with output

A deterministic automaton with output (DFAO) with input alphabet α, states σ and output alphabet Δ consists of a transition function step : σ → α → σ, an initial state start and an output function output : σ → Δ. Where Mathlib's DFA only accepts or rejects a word, a DFAO attaches an arbitrary output to the state it reaches. These automata are the machines that compute automatic sequences, the objects of the theorems of Christol and Cobham.

As for Mathlib's DFA, words are read from the head of the list, and the structure does not require finitely many states; finiteness is imposed where it is used.

Main definitions and results

• TauCeti.DFAO: a deterministic automaton with output.
• TauCeti.DFAO.evalFrom, TauCeti.DFAO.eval: the state reached on a word, from a given state or from the initial state.
• TauCeti.DFAO.evalFrom_append: running on x ++ y runs on x and then on y.
• TauCeti.DFAO.toDFA: the Mathlib DFA accepting the words whose output lies in a set S; TauCeti.DFAO.mem_accepts_toDFA describes its language.
• TauCeti.DFAO.mapOutput, TauCeti.DFAO.prod: post-composition of the output, and the product automaton running two automata in parallel.
• TauCeti.DFAO.reindex: relabelling the states along an equivalence, as Mathlib's DFA.reindex.
• TauCeti.DFAO.comap: changing the input alphabet along a map.
• TauCeti.DFAO.reverse: a finite-state reversal construction, with arbitrary input and output alphabets; TauCeti.DFAO.output_eval_reverse specifies its output on every word.

References

• Andrew Bridy, Automatic sequences and curves over finite fields, Algebra & Number Theory 11 (2017), Section 2.1.
• G. Christol, T. Kamae, M. Mendès France, G. Rauzy, Suites algébriques, automates et substitutions, Bull. Soc. Math. France 108 (1980), Section 4.
• Thijmen J. P. Krebs, A more reasonable proof of Cobham's theorem, 2018, arXiv:1801.06704, Definition 2 and Lemma 5.

structure TauCeti.DFAO (α : Type u) (σ : Type v) (Δ : Type w) : Type (max (max u v) w)

A deterministic automaton with output (DFAO) with input alphabet α, states σ and output alphabet Δ: a transition function, an initial state and an output function. No finiteness is assumed.

• step : σ → α → σ

  The transition from a state on one input letter.

• start : σ

  The initial state.

• output : σ → Δ

  The output attached to a state.

theorem TauCeti.DFAO.ext_iff {α : Type u} {σ : Type v} {Δ : Type w} {x y : DFAO α σ Δ} : x = y ↔ x.step = y.step ∧ x.start = y.start ∧ x.output = y.output

theorem TauCeti.DFAO.ext {α : Type u} {σ : Type v} {Δ : Type w} {x y : DFAO α σ Δ} (step : x.step = y.step) (start : x.start = y.start) (output : x.output = y.output) : x = y

def TauCeti.DFAO.evalFrom {α : Type u} {σ : Type v} {Δ : Type w} (M : DFAO α σ Δ) (s : σ) (x : List α) : σ

M.evalFrom s x is the state reached by running M on the word x from the state s, reading x from its head.

def TauCeti.DFAO.eval {α : Type u} {σ : Type v} {Δ : Type w} (M : DFAO α σ Δ) (x : List α) : σ

M.eval x is the state reached by running M on the word x from its initial state.

@[simp]

theorem TauCeti.DFAO.evalFrom_nil {α : Type u} {σ : Type v} {Δ : Type w} (M : DFAO α σ Δ) (s : σ) : M.evalFrom s [] = s

@[simp]

theorem TauCeti.DFAO.evalFrom_cons {α : Type u} {σ : Type v} {Δ : Type w} (M : DFAO α σ Δ) (s : σ) (a : α) (x : List α) : M.evalFrom s (a :: x) = M.evalFrom (M.step s a) x

theorem TauCeti.DFAO.evalFrom_singleton {α : Type u} {σ : Type v} {Δ : Type w} (M : DFAO α σ Δ) (s : σ) (a : α) : M.evalFrom s [a] = M.step s a

@[simp]

theorem TauCeti.DFAO.evalFrom_append {α : Type u} {σ : Type v} {Δ : Type w} (M : DFAO α σ Δ) (s : σ) (x y : List α) : M.evalFrom s (x ++ y) = M.evalFrom (M.evalFrom s x) y

theorem TauCeti.DFAO.evalFrom_append_singleton {α : Type u} {σ : Type v} {Δ : Type w} (M : DFAO α σ Δ) (s : σ) (x : List α) (a : α) : M.evalFrom s (x ++ [a]) = M.step (M.evalFrom s x) a

theorem TauCeti.DFAO.eval_eq_evalFrom {α : Type u} {σ : Type v} {Δ : Type w} (M : DFAO α σ Δ) (x : List α) : M.eval x = M.evalFrom M.start x

@[simp]

theorem TauCeti.DFAO.eval_nil {α : Type u} {σ : Type v} {Δ : Type w} (M : DFAO α σ Δ) : M.eval [] = M.start

@[simp]

theorem TauCeti.DFAO.eval_cons {α : Type u} {σ : Type v} {Δ : Type w} (M : DFAO α σ Δ) (a : α) (x : List α) : M.eval (a :: x) = M.evalFrom (M.step M.start a) x

theorem TauCeti.DFAO.eval_singleton {α : Type u} {σ : Type v} {Δ : Type w} (M : DFAO α σ Δ) (a : α) : M.eval [a] = M.step M.start a

theorem TauCeti.DFAO.eval_append {α : Type u} {σ : Type v} {Δ : Type w} (M : DFAO α σ Δ) (x y : List α) : M.eval (x ++ y) = M.evalFrom (M.eval x) y

@[simp]

theorem TauCeti.DFAO.eval_append_singleton {α : Type u} {σ : Type v} {Δ : Type w} (M : DFAO α σ Δ) (x : List α) (a : α) : M.eval (x ++ [a]) = M.step (M.eval x) a

The acceptor of a set of outputs

def TauCeti.DFAO.toDFA {α : Type u} {σ : Type v} {Δ : Type w} (M : DFAO α σ Δ) (S : Set Δ) : DFA α σ

The Mathlib DFA with the transitions of M whose accepting states are those with output in S. It accepts exactly the words on which M outputs an element of S (TauCeti.DFAO.mem_accepts_toDFA).

@[simp]

theorem TauCeti.DFAO.toDFA_step {α : Type u} {σ : Type v} {Δ : Type w} (M : DFAO α σ Δ) (S : Set Δ) : (M.toDFA S).step = M.step

@[simp]

theorem TauCeti.DFAO.toDFA_start {α : Type u} {σ : Type v} {Δ : Type w} (M : DFAO α σ Δ) (S : Set Δ) : (M.toDFA S).start = M.start

@[simp]

theorem TauCeti.DFAO.toDFA_accept {α : Type u} {σ : Type v} {Δ : Type w} (M : DFAO α σ Δ) (S : Set Δ) : (M.toDFA S).accept = M.output ⁻¹' S

@[simp]

theorem TauCeti.DFAO.evalFrom_toDFA {α : Type u} {σ : Type v} {Δ : Type w} (M : DFAO α σ Δ) (S : Set Δ) (s : σ) (x : List α) : (M.toDFA S).evalFrom s x = M.evalFrom s x

@[simp]

theorem TauCeti.DFAO.eval_toDFA {α : Type u} {σ : Type v} {Δ : Type w} (M : DFAO α σ Δ) (S : Set Δ) (x : List α) : (M.toDFA S).eval x = M.eval x

@[simp]

theorem TauCeti.DFAO.mem_accepts_toDFA {α : Type u} {σ : Type v} {Δ : Type w} (M : DFAO α σ Δ) {S : Set Δ} {x : List α} : x ∈ (M.toDFA S).accepts ↔ M.output (M.eval x) ∈ S

A word is accepted by M.toDFA S exactly when M outputs an element of S on it.

Changing the output and running two automata in parallel

def TauCeti.DFAO.mapOutput {α : Type u} {σ : Type v} {Δ : Type w} (M : DFAO α σ Δ) {Δ' : Type x} (f : Δ → Δ') : DFAO α σ Δ'

Change the output alphabet of M along f: the same transitions, with output f ∘ output.

@[simp]

theorem TauCeti.DFAO.mapOutput_step {α : Type u} {σ : Type v} {Δ : Type w} (M : DFAO α σ Δ) {Δ' : Type x} (f : Δ → Δ') : (M.mapOutput f).step = M.step

@[simp]

theorem TauCeti.DFAO.mapOutput_start {α : Type u} {σ : Type v} {Δ : Type w} (M : DFAO α σ Δ) {Δ' : Type x} (f : Δ → Δ') : (M.mapOutput f).start = M.start

@[simp]

theorem TauCeti.DFAO.mapOutput_output {α : Type u} {σ : Type v} {Δ : Type w} (M : DFAO α σ Δ) {Δ' : Type x} (f : Δ → Δ') (q : σ) : (M.mapOutput f).output q = f (M.output q)

@[simp]

theorem TauCeti.DFAO.evalFrom_mapOutput {α : Type u} {σ : Type v} {Δ : Type w} (M : DFAO α σ Δ) {Δ' : Type x} (f : Δ → Δ') (s : σ) (x : List α) : (M.mapOutput f).evalFrom s x = M.evalFrom s x

@[simp]

theorem TauCeti.DFAO.eval_mapOutput {α : Type u} {σ : Type v} {Δ : Type w} (M : DFAO α σ Δ) {Δ' : Type x} (f : Δ → Δ') (x : List α) : (M.mapOutput f).eval x = M.eval x

Changing the output does not change the state reached; with TauCeti.DFAO.mapOutput_output, the output on a word is f applied to the original output.

@[simp]

theorem TauCeti.DFAO.mapOutput_id {α : Type u} {σ : Type v} {Δ : Type w} (M : DFAO α σ Δ) : M.mapOutput id = M

@[simp]

theorem TauCeti.DFAO.mapOutput_mapOutput {α : Type u} {σ : Type v} {Δ : Type w} (M : DFAO α σ Δ) {Δ' : Type x} {Δ'' : Type z} (f : Δ → Δ') (g : Δ' → Δ'') : (M.mapOutput f).mapOutput g = M.mapOutput (g ∘ f)

def TauCeti.DFAO.prod {α : Type u} {σ : Type v} {Δ : Type w} (M : DFAO α σ Δ) {τ : Type x} {Δ' : Type y} (N : DFAO α τ Δ') : DFAO α (σ × τ) (Δ × Δ')

The product automaton, running M and N in parallel on the same input and outputting the pair of their outputs.

@[simp]

theorem TauCeti.DFAO.prod_step {α : Type u} {σ : Type v} {Δ : Type w} (M : DFAO α σ Δ) {τ : Type x} {Δ' : Type y} (N : DFAO α τ Δ') (q : σ × τ) (a : α) : (M.prod N).step q a = (M.step q.1 a, N.step q.2 a)

@[simp]

theorem TauCeti.DFAO.prod_start {α : Type u} {σ : Type v} {Δ : Type w} (M : DFAO α σ Δ) {τ : Type x} {Δ' : Type y} (N : DFAO α τ Δ') : (M.prod N).start = (M.start, N.start)

@[simp]

theorem TauCeti.DFAO.prod_output {α : Type u} {σ : Type v} {Δ : Type w} (M : DFAO α σ Δ) {τ : Type x} {Δ' : Type y} (N : DFAO α τ Δ') (q : σ × τ) : (M.prod N).output q = (M.output q.1, N.output q.2)

@[simp]

theorem TauCeti.DFAO.evalFrom_prod {α : Type u} {σ : Type v} {Δ : Type w} (M : DFAO α σ Δ) {τ : Type x} {Δ' : Type y} (N : DFAO α τ Δ') (q : σ × τ) (x : List α) : (M.prod N).evalFrom q x = (M.evalFrom q.1 x, N.evalFrom q.2 x)

@[simp]

theorem TauCeti.DFAO.eval_prod {α : Type u} {σ : Type v} {Δ : Type w} (M : DFAO α σ Δ) {τ : Type x} {Δ' : Type y} (N : DFAO α τ Δ') (x : List α) : (M.prod N).eval x = (M.eval x, N.eval x)

The product automaton reaches the pair of the states reached by the two factors.

Changing the input alphabet

def TauCeti.DFAO.comap {α : Type u} {σ : Type v} {Δ : Type w} (M : DFAO α σ Δ) {α' : Type x} (f : α' → α) : DFAO α' σ Δ

Change the input alphabet along f, applying f to each letter before taking a step.

@[simp]

theorem TauCeti.DFAO.comap_step {α : Type u} {σ : Type v} {Δ : Type w} (M : DFAO α σ Δ) {α' : Type x} (f : α' → α) (s : σ) (a : α') : (M.comap f).step s a = M.step s (f a)

@[simp]

theorem TauCeti.DFAO.comap_start {α : Type u} {σ : Type v} {Δ : Type w} (M : DFAO α σ Δ) {α' : Type x} (f : α' → α) : (M.comap f).start = M.start

@[simp]

theorem TauCeti.DFAO.comap_output {α : Type u} {σ : Type v} {Δ : Type w} (M : DFAO α σ Δ) {α' : Type x} (f : α' → α) (s : σ) : (M.comap f).output s = M.output s

@[simp]

theorem TauCeti.DFAO.evalFrom_comap {α : Type u} {σ : Type v} {Δ : Type w} (M : DFAO α σ Δ) {α' : Type x} (f : α' → α) (s : σ) (w : List α') : (M.comap f).evalFrom s w = M.evalFrom s (List.map f w)

@[simp]

theorem TauCeti.DFAO.eval_comap {α : Type u} {σ : Type v} {Δ : Type w} (M : DFAO α σ Δ) {α' : Type x} (f : α' → α) (w : List α') : (M.comap f).eval w = M.eval (List.map f w)

@[simp]

theorem TauCeti.DFAO.comap_id {α : Type u} {σ : Type v} {Δ : Type w} (M : DFAO α σ Δ) : M.comap id = M

Changing the input alphabet along the identity leaves the automaton unchanged.

@[simp]

theorem TauCeti.DFAO.comap_comap {α : Type u} {σ : Type v} {Δ : Type w} (M : DFAO α σ Δ) {α' : Type x} {α'' : Type z} (f : α' → α) (g : α'' → α') : (M.comap f).comap g = M.comap (f ∘ g)

Successive changes of input alphabet compose the letter maps.

@[simp]

theorem TauCeti.DFAO.toDFA_comap {α : Type u} {σ : Type v} {Δ : Type w} (M : DFAO α σ Δ) {α' : Type x} (f : α' → α) (S : Set Δ) : (M.comap f).toDFA S = DFA.comap f (M.toDFA S)

Selecting accepting outputs commutes with changing the input alphabet.

Reversing the reading order

def TauCeti.DFAO.reverse {α : Type u} {σ : Type v} {Δ : Type w} (M : DFAO α σ Δ) : DFAO α (σ → ↑(Set.range M.output)) Δ

An automaton computing the output of M on the reversed word. Its states are functions from the original states to the image of the output map. Thus finite original states suffice for finite reversed states, even when the input or output alphabet is infinite.

@[simp]

theorem TauCeti.DFAO.reverse_step {α : Type u} {σ : Type v} {Δ : Type w} (M : DFAO α σ Δ) (f : σ → ↑(Set.range M.output)) (a : α) (q : σ) : M.reverse.step f a q = f (M.step q a)

@[simp]

theorem TauCeti.DFAO.reverse_start_coe {α : Type u} {σ : Type v} {Δ : Type w} (M : DFAO α σ Δ) (q : σ) : ↑(M.reverse.start q) = M.output q

@[simp]

theorem TauCeti.DFAO.reverse_output {α : Type u} {σ : Type v} {Δ : Type w} (M : DFAO α σ Δ) (f : σ → ↑(Set.range M.output)) : M.reverse.output f = ↑(f M.start)

theorem TauCeti.DFAO.evalFrom_reverse {α : Type u} {σ : Type v} {Δ : Type w} (M : DFAO α σ Δ) (f : σ → ↑(Set.range M.output)) (w : List α) (q : σ) : M.reverse.evalFrom f w q = f (M.evalFrom q w.reverse)

Running the reversed automaton from f precomposes f with the original run on the reversed word. This describes every state, not only the output at the initial state.

@[simp]

theorem TauCeti.DFAO.output_eval_reverse {α : Type u} {σ : Type v} {Δ : Type w} (M : DFAO α σ Δ) (w : List α) : M.reverse.output (M.reverse.eval w) = M.output (M.eval w.reverse)

The reversed automaton returns the original output on the reversed word, including the empty word and words with padding.

Relabelling the states

def TauCeti.DFAO.reindex {α : Type u} {σ : Type v} {Δ : Type w} {σ' : Type x} (g : σ ≃ σ') : DFAO α σ Δ ≃ DFAO α σ' Δ

Lift an equivalence of state types to an equivalence of automata with output: the relabelled automaton has the same transitions, initial state and outputs, read through the equivalence.

@[simp]

theorem TauCeti.DFAO.reindex_apply_step {α : Type u} {σ : Type v} {Δ : Type w} (M : DFAO α σ Δ) {σ' : Type x} (g : σ ≃ σ') (s : σ') (a : α) : ((reindex g) M).step s a = g (M.step (g.symm s) a)

@[simp]

theorem TauCeti.DFAO.reindex_apply_start {α : Type u} {σ : Type v} {Δ : Type w} (M : DFAO α σ Δ) {σ' : Type x} (g : σ ≃ σ') : ((reindex g) M).start = g M.start

@[simp]

theorem TauCeti.DFAO.reindex_apply_output {α : Type u} {σ : Type v} {Δ : Type w} (M : DFAO α σ Δ) {σ' : Type x} (g : σ ≃ σ') (s : σ') : ((reindex g) M).output s = M.output (g.symm s)

@[simp]

theorem TauCeti.DFAO.reindex_refl {α : Type u} {σ : Type v} {Δ : Type w} (M : DFAO α σ Δ) : (reindex (Equiv.refl σ)) M = M

@[simp]

theorem TauCeti.DFAO.symm_reindex {α : Type u} {σ : Type v} {Δ : Type w} {σ' : Type x} (g : σ ≃ σ') : (reindex g).symm = reindex g.symm

@[simp]

theorem TauCeti.DFAO.evalFrom_reindex {α : Type u} {σ : Type v} {Δ : Type w} (M : DFAO α σ Δ) {σ' : Type x} (g : σ ≃ σ') (s : σ') (x : List α) : ((reindex g) M).evalFrom s x = g (M.evalFrom (g.symm s) x)

@[simp]

theorem TauCeti.DFAO.eval_reindex {α : Type u} {σ : Type v} {Δ : Type w} (M : DFAO α σ Δ) {σ' : Type x} (g : σ ≃ σ') (x : List α) : ((reindex g) M).eval x = g (M.eval x)

The relabelled automaton reaches the relabelled state, so it has the same output on every word (TauCeti.DFAO.output_eval_reindex).

theorem TauCeti.DFAO.output_eval_reindex {α : Type u} {σ : Type v} {Δ : Type w} (M : DFAO α σ Δ) {σ' : Type x} (g : σ ≃ σ') (x : List α) : ((reindex g) M).output (((reindex g) M).eval x) = M.output (M.eval x)

Checks