Lax765601.AperiodicPumping

Aperiodicity as a pumping property

concepts/Lax765601/AperiodicPumping.lean · lax-765601

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✓Lax765601.AperiodicPumping

⊢Lax765601Proofs.Results.aperiodic_iff_pumping

In the paper

page 28 of the paper of lax-157538, Transducers

Theorem

A function $f$ computed by a Mealy machine is aperiodic if and only if for all input strings $u, v, w$ there are output strings $x, y, z$ and a number $k$ such that

f(u v^{n+k} w) = x y^n z \qquad \text{for all } n > 0

(Claim A.2.9 of Transducers). The right-to-left direction is immediate, since the last letter of $x y^n z$ does not depend on $n$ . For the other direction, aperiodicity fixes the last $|v|$ letters of $f(u v^n)$ for large $n$ , so that from some point on the output ends with repetitions of a fixed string $y$ of length $|v|$ , and fixes the last $|w|$ letters of $f(u v^n w)$ , which gives $z$ . The pumping form is what makes aperiodicity compatible with composition: the shift $k$ of $f \cdot g$ is the sum of the shifts of $f$ and $g$ .

Lean source view on GitHub

1	import Lax765601.MealyMachine
2	import Lax765601.Aperiodicity
3
4	/-!
5	---
6	title: Aperiodicity as a pumping property
7	type: theorem
8	---
9	A function $f$ computed by a Mealy machine is aperiodic if and only if for all
10	input strings $u, v, w$ there are output strings $x, y, z$ and a number $k$ such
11	that
12	$f(u v^{n+k} w) = x y^n z \qquad \text{for all } n > 0$
13	(Claim A.2.9 of Transducers). The right-to-left direction is immediate, since
14	the last letter of $x y^n z$ does not depend on $n$ . For the other direction,
15	aperiodicity fixes the last $\|v\|$ letters of $f(u v^n)$ for large $n$ , so that
16	from some point on the output ends with repetitions of a fixed string $y$ of
17	length $\|v\|$ , and fixes the last $\|w\|$ letters of $f(u v^n w)$ , which gives $z$ .
18	The pumping form is what makes aperiodicity compatible with composition: the
19	shift $k$ of $f \cdot g$ is the sum of the shifts of $f$ and $g$ .
20
21	# Formalization notes
22
23	`npow v n` is `vⁿ`. The hypothesis that `f` is computed by a Mealy machine is
24	used only in the left-to-right direction; no finiteness of the alphabets is
25	needed.
26	-/
27
28	namespace Lax765601.AperiodicPumping
29
30	open Lax765601.MealyMachine Lax765601.Aperiodicity
31
32	/-- A Mealy function is aperiodic if and only if it has the pumping property: for
33	all `u, v, w` there are `x, y, z` and `k` with `f (u v^(n+k) w) = x yⁿ z` for all
34	`n > 0`. -/
35	axiom aperiodic_iff_pumping {A B : Type} {f : List A → List B} (hf : IsMealy f) :
36	Aperiodic f ↔
37	∀ u v w : List A, ∃ (x y z : List B) (k : ℕ), ∀ n > 0,
38	f (u ++ npow v (n + k) ++ w) = x ++ npow y n ++ z
39
40	end Lax765601.AperiodicPumping
41

Show Proof

Formalization notes

$npow v n$ is $vⁿ$ . The hypothesis that $f$ is computed by a Mealy machine is used only in the left-to-right direction; no finiteness of the alphabets is needed.

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