Lax765601.StateTransformations

State transformations of a pre-automaton

concepts/Lax765601/StateTransformations.lean · lax-765601

definition

Loading review…

Concept map

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Definition

A pre-automaton is a deterministic finite automaton without designated initial and accepting states: an input alphabet $A$ , a state space $Q$ and a family of state transformations $\delta_a : Q \to Q$ , one for each letter $a \in A$ (Section A.2 of Transducers). The state transformation $\delta_w$ of an input string $w$ is the composition of the state transformations of its letters, in the order in which they are read.

The state transformation transducer of a pre-automaton is the Mealy machine of type $A^* \to (Q \to Q)^*$ whose $n$ -th output letter is the state transformation of the first $n$ input letters. It is the object that the proof of the Krohn–Rhodes theorem decomposes (Lemma A.2.5).

A pre-automaton satisfies the stabilisation condition (*) of Lemma A.2.11 if for every state transformation $\delta$ that arises from some input string, the sequence of powers $\delta^1, \delta^2, \ldots$ eventually stabilises on a single state transformation. This is the condition on a minimal Mealy machine that characterises aperiodicity.

Lean source view on GitHub

1	import Mathlib.Logic.Function.Iterate
2	import Lax765601.MealyMachine
3
4	/-!
5	---
6	title: State transformations of a pre-automaton
7	type: definition
8	---
9	A pre-automaton is a deterministic finite automaton without designated initial
10	and accepting states: an input alphabet $A$ , a state space $Q$ and a family of
11	state transformations $\delta_a : Q \to Q$ , one for each letter $a \in A$
12	(Section A.2 of Transducers). The state transformation $\delta_w$ of an input
13	string $w$ is the composition of the state transformations of its letters, in
14	the order in which they are read.
15
16	The state transformation transducer of a pre-automaton is the Mealy machine of
17	type $A^* \to (Q \to Q)^*$ whose $n$ -th output letter is the state
18	transformation of the first $n$ input letters. It is the object that the proof of
19	the Krohn–Rhodes theorem decomposes (Lemma A.2.5).
20
21	A pre-automaton satisfies the stabilisation condition (*) of Lemma A.2.11 if
22	for every state transformation $\delta$ that arises from some input string, the
23	sequence of powers $\delta^1, \delta^2, \ldots$ eventually stabilises on a single
24	state transformation. This is the condition on a minimal Mealy machine that
25	characterises aperiodicity.
26
27	# Formalization notes
28
29	A pre-automaton is just its transition function `δ : Q → A → Q`; no structure is
30	introduced. `strTrans δ w` is the state transformation of the string `w`, a
31	left fold of `δ` along `w`, so that the letters act in reading order. The
32	transition function of the state transformation transducer stores the state
33	transformation of the prefix read so far as its state and outputs it after every
34	letter, as the book describes; its state space `Q → Q` is finite when `Q` is.
35	`f^[n]` is the `n`-th iterate of `f`.
36	-/
37
38	namespace Lax765601.StateTransformations
39
40	open Lax765601.MealyMachine
41
42	/-- The state transformation of an input string, for the pre-automaton `δ`: the
43	letters act one after the other, in reading order. -/
44	def strTrans {A Q : Type} (δ : Q → A → Q) (w : List A) : Q → Q := fun q => w.foldl δ q
45
46	/-- The stabilisation condition (*) of Lemma A.2.11: for every state
47	transformation `δ_w` arising from an input string, the sequence of its powers
48	`δ_w¹, δ_w², …` eventually stabilises. -/
49	def TransAperiodic {A Q : Type} (δ : Q → A → Q) : Prop :=
50	∀ w : List A, ∃ N : ℕ, ∀ n ≥ N, (strTrans δ w)^[n] = (strTrans δ w)^[N]
51
52	/-- The state transformation transducer of a pre-automaton: the Mealy machine
53	whose `n`-th output letter is the state transformation of the first `n` input
54	letters. -/
55	def stateTransTransducer {A Q : Type} (δ : Q → A → Q) : Mealy A (Q → Q) (Q → Q) where
56	init := id
57	step := fun t a => (fun q => δ (t q) a, fun q => δ (t q) a)
58
59	end Lax765601.StateTransformations
60

Formalization notes

A pre-automaton is just its transition function $δ : Q → A → Q$ ; no structure is introduced. $strTrans δ w$ is the state transformation of the string $w$ , a left fold of $δ$ along $w$ , so that the letters act in reading order. The transition function of the state transformation transducer stores the state transformation of the prefix read so far as its state and outputs it after every letter, as the book describes; its state space $Q → Q$ is finite when $Q$ is. $f^[n]$ is the $n$ -th iterate of $f$ .

Builds on

Lax765601.MealyMachine

Used by

From Mathlib

Mathlib.Logic.Function.Iterate

Community review

Discussion

Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.

0 comments

Loading discussion…

Lax Lean Archive

State transformations of a pre-automaton

Flags

Flag this concept