Lax132576.SequentialTransducers

Sequential transducers

concepts/Lax132576/SequentialTransducers.lean · lax-132576

definition

Loading review…

Concept map

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

In the paper

page 69 of the paper of lax-157538, Transducers

Definition

A sequential transducer (Section B.4.2 of Transducers) is defined like a Mealy machine, except that its transition function has type

Q \times A \to Q \times B^*,

so that a transition may produce an output string of any length, including the empty one, instead of exactly one letter. The functions computed by sequential transducers, the sequential functions, lie strictly between the Mealy machines and the rational functions; Theorem B.4.6 characterises them without reference to a machine.

Lean source view on GitHub

1	import Mathlib.Data.Finite.Defs
2
3	/-!
4	---
5	title: Sequential transducers
6	type: definition
7	---
8	A sequential transducer (Section B.4.2 of Transducers) is defined like a
9	Mealy machine, except that its transition function has type
10	$Q \times A \to Q \times B^*,$
11	so that a transition may produce an output string of any length, including the
12	empty one, instead of exactly one letter. The functions computed by sequential
13	transducers, the sequential functions, lie strictly between the Mealy
14	machines and the rational functions; Theorem B.4.6 characterises them without
15	reference to a machine.
16
17	# Formalization notes
18
19	`run` concatenates the output strings of the transitions taken from a given
20	state, and `eval` is the run from the initial state; `IsSequential f` asks for a
21	finite state space.
22	-/
23
24	namespace Lax132576.SequentialTransducers
25
26	/-- A sequential transducer: a Mealy machine whose transitions produce output
27	strings of variable length. -/
28	structure Sequential (A B Q : Type) where
29	/-- The initial state. -/
30	init : Q
31	/-- The transition function: a target state and an output string. -/
32	step : Q → A → Q × List B
33
34	namespace Sequential
35
36	variable {A B Q : Type}
37
38	/-- The output produced from a given state on an input string. -/
39	def run (T : Sequential A B Q) : Q → List A → List B
40	\| _, [] => []
41	\| q, a :: w => (T.step q a).2 ++ T.run (T.step q a).1 w
42
43	/-- The semantics of a sequential transducer. -/
44	def eval (T : Sequential A B Q) (w : List A) : List B := T.run T.init w
45
46	/-- The transition function of the underlying automaton. -/
47	def transFun (T : Sequential A B Q) : Q → A → Q := fun q a => (T.step q a).1
48
49	end Sequential
50
51	/-- A function computed by a sequential transducer with a finite state space. -/
52	def IsSequential {A B : Type} (f : List A → List B) : Prop :=
53	∃ (Q : Type) (_ : Finite Q) (T : Sequential A B Q), T.eval = f
54
55	end Lax132576.SequentialTransducers
56

Formalization notes

$run$ concatenates the output strings of the transitions taken from a given state, and $eval$ is the run from the initial state; $IsSequential f$ asks for a finite state space.

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