Lax132576.LengthPreservingNormalForm

Length preserving rational functions have length preserving automata

concepts/Lax132576/LengthPreservingNormalForm.lean · lax-132576

proven

Loading review…

Concept map

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Evidence

Each proof establishes this claim relative to its assumptions.

no assumptions

thm✓Lax132576.LengthPreservingNormalForm

⊢Lax132576Proofs.Results.exists_nfao_length_eq

In the paper

page 67 of the paper of lax-157538, Transducers

Theorem

If a rational function is length preserving, then it is computed by an automaton with output in which the input and the output string of every transition have the same length (Lemma B.4.5 of Transducers). The book's proof takes the typing of Claim B.4.4 and works in the free group over the output alphabet: the new states are pairs $(q, x)$ of a state and a reduced string $x$ of length $\tau(q)$ , possibly negative, and a transition $q \xrightarrow{w / x^{-1} v y} p$ of the original automaton becomes the transition $(q, x) \xrightarrow{w / v} (p, y)$ , whose lengths agree.

Lean source view on GitHub

1	import Lax765601.ElementaryProperties
2	import Lax132576.RationalFunctions
3
4	/-!
5	---
6	title: Length preserving rational functions have length preserving automata
7	type: theorem
8	---
9	If a rational function is length preserving, then it is computed by an
10	automaton with output in which the input and the output string of every
11	transition have the same length (Lemma B.4.5 of Transducers). The book's
12	proof takes the typing of Claim B.4.4 and works in the free group over the
13	output alphabet: the new states are pairs $(q, x)$ of a state and a reduced
14	string $x$ of length $\tau(q)$ , possibly negative, and a transition
15	$q \xrightarrow{w / x^{-1} v y} p$ of the original automaton becomes the
16	transition $(q, x) \xrightarrow{w / v} (p, y)$ , whose lengths agree.
17
18	# Formalization notes
19
20	The conclusion asks for a finite state space and an automaton all of whose
21	transitions `(p, u, v, q)` satisfy `u.length = v.length`, whose relation is the
22	graph of `f`. Both alphabets are assumed finite.
23	-/
24
25	namespace Lax132576.LengthPreservingNormalForm
26
27	open Lax765601.ElementaryProperties Lax132576.RationalRelations Lax132576.RationalFunctions
28
29	/-- A length preserving rational function is computed by an automaton with output
30	whose every transition reads and writes strings of the same length. -/
31	axiom exists_nfao_length_eq {A B : Type} [Finite A] [Finite B]
32	{f : List A → List B} (hf : IsRationalFun f) (hlen : LengthPreserving f) :
33	∃ (Q : Type) (_ : Finite Q) (M : NFAO A B Q),
34	(∀ t ∈ M.δ, t.2.1.length = t.2.2.1.length) ∧ ∀ w v, M.rel w v ↔ v = f w
35
36	end Lax132576.LengthPreservingNormalForm
37

Show Proof

Formalization notes

The conclusion asks for a finite state space and an automaton all of whose transitions $(p, u, v, q)$ satisfy $u.length = v.length$ , whose relation is the graph of $f$ . Both alphabets are assumed finite.

Builds on

Used by

none

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