The transition monoid of a DFA

Each word induces a transformation of the states of a DFA, and reading one word after another composes these transformations. The monoid they generate is the transition monoid, the basic algebraic invariant of an automaton. It is finite when the automaton is.

Main definitions

• DFA.transitionHom: the monoid homomorphism sending a word to the transformation it induces
• DFA.transitionMonoid: the transition monoid, the range of DFA.transitionHom

Implementation notes

A word w acts on a state s by s ↦ M.evalFrom s w, and evalFrom_of_append makes this a right action, written q · u in the literature. Since Function.End composes on the left, that is an anti-homomorphism, so the target of DFA.transitionHom is the opposite monoid (Function.End σ)ᵐᵒᵖ. Its domain stays FreeMonoid α, so that its kernel is a congruence on words, comparable with the syntactic congruence.

Pin's deterministic automata are partial, so the transition monoid there sits in the monoid of partial transformations. DFA has a total step, so the transformations here are total.

References

• [Pin]

def DFA.transitionHom {α : Type u_1} {σ : Type u_2} (M : DFA α σ) : FreeMonoid α →* (Function.End σ)ᵐᵒᵖ

M.transitionHom w is the transformation of states induced by the word w.

Equations

• M.transitionHom = { toFun := fun (w : FreeMonoid α) => MulOpposite.op fun (s : σ) => M.evalFrom s (FreeMonoid.toList w), map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem DFA.unop_transitionHom_apply {α : Type u_1} {σ : Type u_2} (M : DFA α σ) (w : FreeMonoid α) (s : σ) : MulOpposite.unop (M.transitionHom w) s = M.evalFrom s (FreeMonoid.toList w)

theorem DFA.transitionHom_eq_iff {α : Type u_1} {σ : Type u_2} (M : DFA α σ) {u v : FreeMonoid α} : M.transitionHom u = M.transitionHom v ↔ ∀ (s : σ), M.evalFrom s (FreeMonoid.toList u) = M.evalFrom s (FreeMonoid.toList v)

def DFA.transitionMonoid {α : Type u_1} {σ : Type u_2} (M : DFA α σ) : Submonoid (Function.End σ)ᵐᵒᵖ

M.transitionMonoid is the monoid of transformations of the states of M induced by words.

Equations

• M.transitionMonoid = MonoidHom.mrange M.transitionHom