Lax132576.PrimeRationalFunctions

The prime rational functions

concepts/Lax132576/PrimeRationalFunctions.lean · lax-132576

definition

Loading review…

Concept map

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

In the paper

page 49 of the paper of lax-157538, Transducers

Definition

The prime rational functions of Theorem B.2.6 of Transducers are the following four kinds of functions:

the prime Mealy machines, i.e. the reversible and the flip-flop Mealy machines;
their right-to-left variants — Mealy machines that process the input from right to left, the initial state being used after the rightmost position;
the string homomorphisms;
the function $w \mapsto w\#$ which appends a fresh separator symbol to the input string.

Theorem B.2.6 says that the rational functions are exactly the compositions of prime rational functions, the analogue of the Krohn–Rhodes theorem one step up the transducer ladder.

Lean source view on GitHub

1	import Lax765601.PrimeMealyMachines
2	import Lax132576.StringHomomorphisms
3
4	/-!
5	---
6	title: The prime rational functions
7	type: definition
8	---
9	The prime rational functions of Theorem B.2.6 of Transducers are the
10	following four kinds of functions:
11
12	1. the prime Mealy machines, i.e. the reversible and the flip-flop Mealy
13	machines;
14	2. their right-to-left variants — Mealy machines that process the input from
15	right to left, the initial state being used after the rightmost position;
16	3. the string homomorphisms;
17	4. the function $w \mapsto w\#$ which appends a fresh separator symbol to the
18	input string.
19
20	Theorem B.2.6 says that the rational functions are exactly the compositions of
21	prime rational functions, the analogue of the Krohn–Rhodes theorem one step up
22	the transducer ladder.
23
24	# Formalization notes
25
26	A right-to-left Mealy machine computes `f` exactly when the function
27	`w ↦ reverse (f (reverse w))` is computed by a Mealy machine, which is how the
28	second kind is stated. The separator function needs the output alphabet to be
29	the input alphabet plus one letter; this is expressed by a bijection
30	`e : Option A ≃ B`, the separator being `e none`. `PrimeRationalFam` is a family
31	in the sense of `Lax765601.CompositionClosure`, so that "composition of prime
32	rational functions" is its composition closure.
33	-/
34
35	namespace Lax132576.PrimeRationalFunctions
36
37	open Lax765601.CompositionClosure Lax765601.PrimeMealyMachines Lax132576.StringHomomorphisms
38
39	/-- The family of prime rational functions: prime Mealy machines, their
40	right-to-left variants, string homomorphisms, and the separator function
41	`w ↦ w #`. -/
42	def PrimeRationalFam : Family := fun A B f =>
43	PrimeMealyFam A B f ∨
44	PrimeMealyFam A B (fun w => (f w.reverse).reverse) ∨
45	(∃ φ : A → List B, f = homOf φ) ∨
46	(∃ e : Option A ≃ B, f = fun w => w.map (fun a => e (some a)) ++ [e none])
47
48	end Lax132576.PrimeRationalFunctions
49

Formalization notes

A right-to-left Mealy machine computes $f$ exactly when the function $w ↦ reverse (f (reverse w))$ is computed by a Mealy machine, which is how the second kind is stated. The separator function needs the output alphabet to be the input alphabet plus one letter; this is expressed by a bijection $e : Option A ≃ B$ , the separator being $e none$ . $PrimeRationalFam$ is a family in the sense of $Lax765601.CompositionClosure$ , so that "composition of prime rational functions" is its composition closure.

Builds on

Used by

From Mathlib

none

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