Lax765601.MealyMachine

Mealy machines

concepts/Lax765601/MealyMachine.lean · lax-765601

definition

Loading review…

Concept map

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

In the paper

page 13 of the paper of lax-157538, Transducers

Definition

A Mealy machine is a deterministic finite automaton whose transitions are labelled by output letters, and which has no accepting states, since its purpose is to produce an output string rather than to accept or reject. Formally (Definition A.1.1 of Transducers), it consists of an input alphabet $A$ , an output alphabet $B$ , a state space $Q$ , an initial state $q_0 \in Q$ and a transition function

\delta : Q \times A \to Q \times B.

Its semantics is the function $f : A^* \to B^*$ obtained by running the underlying automaton on the input string and labelling each position by the output letter of the corresponding transition; it is a letter-to-letter function, the output having the same length as the input. A function is computed by a Mealy machine if it is the semantics of a Mealy machine with a finite state space.

The state transformation of an input letter $a$ is the map $Q \to Q$ describing how reading $a$ updates the state, the output being ignored; the underlying pre-automaton of the machine is the family of these maps, i.e. a deterministic automaton without initial and accepting states (Section A.2).

Lean source view on GitHub

1	import Mathlib.Data.Finite.Defs
2
3	/-!
4	---
5	title: Mealy machines
6	type: definition
7	---
8	A Mealy machine is a deterministic finite automaton whose transitions are
9	labelled by output letters, and which has no accepting states, since its purpose
10	is to produce an output string rather than to accept or reject. Formally
11	(Definition A.1.1 of Transducers), it consists of an input alphabet $A$ , an
12	output alphabet $B$ , a state space $Q$ , an initial state $q_0 \in Q$ and a
13	transition function
14	$\delta : Q \times A \to Q \times B.$
15	Its semantics is the function $f : A^* \to B^*$ obtained by running the
16	underlying automaton on the input string and labelling each position by the
17	output letter of the corresponding transition; it is a letter-to-letter
18	function, the output having the same length as the input. A function is
19	computed by a Mealy machine if it is the semantics of a Mealy machine with a
20	finite state space.
21
22	The state transformation of an input letter $a$ is the map $Q \to Q$ describing
23	how reading $a$ updates the state, the output being ignored; the underlying
24	pre-automaton of the machine is the family of these maps, i.e. a deterministic
25	automaton without initial and accepting states (Section A.2).
26
27	# Formalization notes
28
29	`Mealy A B Q` carries the initial state and the transition function; the three
30	alphabets are the type parameters. Finiteness of the state space is not part of
31	the structure — it is where it belongs, in `IsMealy`, which asks for some
32	finite state space `Q` and some machine over it. Alphabets are arbitrary types;
33	the finiteness the book assumes globally is a hypothesis of the statements that
34	need it.
35
36	`run` is the output produced from a given state, defined by recursion on the
37	input string, and `eval` is the run from the initial state. Nothing else is
38	derivable from these and is omitted; the dfa obtained by forgetting outputs is
39	`transFun`.
40	-/
41
42	namespace Lax765601.MealyMachine
43
44	/-- A Mealy machine with input alphabet `A`, output alphabet `B` and state space
45	`Q`: an initial state and a transition function `Q × A → Q × B`. -/
46	structure Mealy (A B Q : Type) where
47	/-- The initial state. -/
48	init : Q
49	/-- The transition function: a source state and an input letter determine a
50	target state and an output letter. -/
51	step : Q → A → Q × B
52
53	namespace Mealy
54
55	variable {A B Q : Type}
56
57	/-- The output produced by the machine on an input string, when started in a
58	given state. -/
59	def run (M : Mealy A B Q) : Q → List A → List B
60	\| _, [] => []
61	\| q, a :: w => (M.step q a).2 :: M.run (M.step q a).1 w
62
63	/-- The semantics of a Mealy machine: the output produced from the initial state.
64	-/
65	def eval (M : Mealy A B Q) (w : List A) : List B := M.run M.init w
66
67	/-- The state transformation of an input letter: how reading the letter updates
68	the state. -/
69	def letterTrans (M : Mealy A B Q) (a : A) : Q → Q := fun q => (M.step q a).1
70
71	/-- The underlying pre-automaton: the transition function with the output letters
72	forgotten. -/
73	def transFun (M : Mealy A B Q) : Q → A → Q := fun q a => (M.step q a).1
74
75	end Mealy
76
77	/-- A string-to-string function is computed by a Mealy machine if it is the
78	semantics of a Mealy machine with a finite state space. -/
79	def IsMealy {A B : Type} (f : List A → List B) : Prop :=
80	∃ (Q : Type) (_ : Finite Q) (M : Mealy A B Q), M.eval = f
81
82	end Lax765601.MealyMachine
83

Formalization notes

$Mealy A B Q$ carries the initial state and the transition function; the three alphabets are the type parameters. Finiteness of the state space is not part of the structure — it is where it belongs, in $IsMealy$ , which asks for some finite state space $Q$ and some machine over it. Alphabets are arbitrary types; the finiteness the book assumes globally is a hypothesis of the statements that need it.

$run$ is the output produced from a given state, defined by recursion on the input string, and $eval$ is the run from the initial state. Nothing else is derivable from these and is omitted; the dfa obtained by forgetting outputs is $transFun$ .

Builds on

none

Used by

From Mathlib

Mathlib.Data.Finite.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