Lax765601.PrimeMealyMachines

Prime Mealy machines: reversible and flip-flop

concepts/Lax765601/PrimeMealyMachines.lean · lax-765601

definition

Loading review…

Concept map

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

In the paper

page 20 of the paper of lax-157538, Transducers

Definition

The prime Mealy machines are defined in terms of the state transformations of their letters (Definition A.2.1 of Transducers). There are two kinds.

Reversible machines: the state transformation of every letter is a permutation of the state space.
Flip-flop machines: the state transformation of every letter is either the identity or a constant, all states being mapped to the same one.

A one-state machine is both. The machine outputting $abab\cdots$ on $a^n$ is reversible; the delay machine, which shifts the input one position to the right, is a flip-flop. Since composing permutations gives a permutation and composing constants gives a constant, nothing changes if the definition is phrased for the state transformations of input strings rather than of letters.

The Krohn–Rhodes theorem (Theorem A.2.2) says that every Mealy machine is a composition of prime Mealy machines; Theorem A.2.8 characterises the compositions of flip-flops alone.

Lean source view on GitHub

1	import Mathlib.Logic.Function.Defs
2	import Lax765601.MealyMachine
3	import Lax765601.CompositionClosure
4
5	/-!
6	---
7	title: Prime Mealy machines: reversible and flip-flop
8	type: definition
9	---
10	The prime Mealy machines are defined in terms of the state transformations of
11	their letters (Definition A.2.1 of Transducers). There are two kinds.
12
13	* Reversible machines: the state transformation of every letter is a
14	permutation of the state space.
15	* Flip-flop machines: the state transformation of every letter is either the
16	identity or a constant, all states being mapped to the same one.
17
18	A one-state machine is both. The machine outputting $abab\cdots$ on $a^n$ is
19	reversible; the delay machine, which shifts the input one position to the right,
20	is a flip-flop. Since composing permutations gives a permutation and composing
21	constants gives a constant, nothing changes if the definition is phrased for the
22	state transformations of input strings rather than of letters.
23
24	The Krohn–Rhodes theorem (Theorem A.2.2) says that every Mealy machine is a
25	composition of prime Mealy machines; Theorem A.2.8 characterises the compositions
26	of flip-flops alone.
27
28	# Formalization notes
29
30	`Reversible` and `FlipFlop` are properties of a machine. The families that the
31	composition closure is taken over are families of functions (as in
32	`CompositionClosure`), so a function is a prime if it is computed by some prime
33	machine with a finite state space: `PrimeMealyFam` collects the reversible and
34	the flip-flop functions, and `FlipFlopFam` the flip-flop ones alone, for
35	Theorem A.2.8. Bijectivity is mathlib's `Function.Bijective`.
36	-/
37
38	namespace Lax765601.PrimeMealyMachines
39
40	open Lax765601.MealyMachine Lax765601.CompositionClosure
41
42	/-- A Mealy machine is reversible if the state transformation of every letter is a
43	permutation of the state space. -/
44	def Reversible {A B Q : Type} (M : Mealy A B Q) : Prop :=
45	∀ a : A, Function.Bijective (M.letterTrans a)
46
47	/-- A Mealy machine is a flip-flop if the state transformation of every letter is
48	the identity or a constant. -/
49	def FlipFlop {A B Q : Type} (M : Mealy A B Q) : Prop :=
50	∀ a : A, M.letterTrans a = id ∨ ∃ q₀ : Q, ∀ q : Q, M.letterTrans a q = q₀
51
52	/-- A function is computed by a reversible Mealy machine with a finite state
53	space. -/
54	def IsReversibleMealy {A B : Type} (f : List A → List B) : Prop :=
55	∃ (Q : Type) (_ : Finite Q) (M : Mealy A B Q), M.eval = f ∧ Reversible M
56
57	/-- A function is computed by a flip-flop Mealy machine with a finite state
58	space. -/
59	def IsFlipFlopMealy {A B : Type} (f : List A → List B) : Prop :=
60	∃ (Q : Type) (_ : Finite Q) (M : Mealy A B Q), M.eval = f ∧ FlipFlop M
61
62	/-- The family of prime Mealy machines: the functions computed by a reversible or
63	by a flip-flop machine. -/
64	def PrimeMealyFam : Family := fun _ _ f => IsReversibleMealy f ∨ IsFlipFlopMealy f
65
66	/-- The family of flip-flop Mealy machines. -/
67	def FlipFlopFam : Family := fun _ _ f => IsFlipFlopMealy f
68
69	end Lax765601.PrimeMealyMachines
70

Formalization notes

$Reversible$ and $FlipFlop$ are properties of a machine. The families that the composition closure is taken over are families of functions (as in $CompositionClosure$ ), so a function is a prime if it is computed by some prime machine with a finite state space: $PrimeMealyFam$ collects the reversible and the flip-flop functions, and $FlipFlopFam$ the flip-flop ones alone, for Theorem A.2.8. Bijectivity is mathlib's $Function.Bijective$ .

Builds on

Used by

From Mathlib

Mathlib.Logic.Function.Defs

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