Lax132576.SequentialCharacterisation

Machine-independent characterisation of sequential functions

concepts/Lax132576/SequentialCharacterisation.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.SequentialCharacterisation

⊢Lax132576Proofs.Results.isSequential_iff

In the paper

page 69 of the paper of lax-157538, Transducers

Theorem

A function $f : A^* \to B^*$ is sequential if and only if it (a) is continuous, (b) is prefix preserving, (c) outputs $\varepsilon$ on the input $\varepsilon$ , and (d) has the bounded increase property: the increase of output length caused by extending the input by one letter,

\sup_{w \in A^*,\, a \in A} |f(wa)| - |f(w)|,

is finite (Theorem B.4.6 of Transducers, Ginsburg and Rose). The derivative $wa \mapsto f(w)^{-1} f(wa)$ , well defined by prefix preservation and of finite image by bounded increase, is shown to be computed by a finite automaton — its length by continuity modulo a large enough number, and then its value by continuity again.

Lean source view on GitHub

1	import Lax765601.Continuity
2	import Lax765601.ElementaryProperties
3	import Lax132576.SequentialTransducers
4
5	/-!
6	---
7	title: Machine-independent characterisation of sequential functions
8	type: theorem
9	---
10	A function $f : A^* \to B^*$ is sequential if and only if it (a) is continuous,
11	(b) is prefix preserving, (c) outputs $\varepsilon$ on the input $\varepsilon$ ,
12	and (d) has the bounded increase property: the increase of output length
13	caused by extending the input by one letter,
14	$\sup_{w \in A^*,\, a \in A} \|f(wa)\| - \|f(w)\|,$
15	is finite (Theorem B.4.6 of Transducers, Ginsburg and Rose). The derivative
16	$wa \mapsto f(w)^{-1} f(wa)$ , well defined by prefix preservation and of
17	finite image by bounded increase, is shown to be computed by a finite
18	automaton — its length by continuity modulo a large enough number, and then
19	its value by continuity again.
20
21	# Formalization notes
22
23	Item (c) is the conjunct `f [] = []`. An earlier edition of the book omitted
24	it, and without it the statement is false: a sequential transducer produces no
25	output before reading any input, while $a^n \mapsto a^{n+1}$ has the three
26	other properties. Bounded increase is stated with an explicit bound `K`. Both
27	alphabets are assumed finite.
28	-/
29
30	namespace Lax132576.SequentialCharacterisation
31
32	open Lax765601.Continuity Lax765601.ElementaryProperties Lax132576.SequentialTransducers
33
34	/-- A function is sequential if and only if it maps `ε` to `ε`, is continuous,
35	prefix preserving, and has bounded increase. -/
36	axiom isSequential_iff {A B : Type} [Finite A] [Finite B] (f : List A → List B) :
37	IsSequential f ↔
38	f [] = [] ∧ Continuous f ∧ PrefixPreserving f ∧
39	∃ K : ℕ, ∀ (w : List A) (a : A), (f (w ++ [a])).length ≤ (f w).length + K
40
41	end Lax132576.SequentialCharacterisation
42

Show Proof

Formalization notes

Item (c) is the conjunct $f [] = []$ . An earlier edition of the book omitted it, and without it the statement is false: a sequential transducer produces no output before reading any input, while $a^n \mapsto a^{n+1}$ has the three other properties. Bounded increase is stated with an explicit bound $K$ . 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