Lax765601.Aperiodicity

Aperiodic string-to-string functions

concepts/Lax765601/Aperiodicity.lean · lax-765601

definition

Loading review…

Concept map

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

In the paper

page 27 of the paper of lax-157538, Transducers

Definition

A length preserving string-to-string function $f$ is aperiodic (Definition A.2.7 of Transducers) if for all input strings $u, v, w$ the last letter of

f(u v^n w)

is the same for all sufficiently large $n$ . Aperiodicity says that the function cannot have periodic behaviour: the function on $a^*$ whose last output letter says whether the input has length at least two is aperiodic, while the one whose last letter gives the parity of the length is not. By the arbitrary choice of $w$ , the last $k$ output letters are eventually fixed as well, for every $k$ . Theorem A.2.8 shows that the aperiodic functions computed by Mealy machines are exactly the compositions of flip-flop machines.

Lean source view on GitHub

1	import Mathlib.Data.List.Basic
2
3	/-!
4	---
5	title: Aperiodic string-to-string functions
6	type: definition
7	---
8	A length preserving string-to-string function $f$ is aperiodic (Definition
9	A.2.7 of Transducers) if for all input strings $u, v, w$ the last letter of
10	$f(u v^n w)$
11	is the same for all sufficiently large $n$ . Aperiodicity says that the function
12	cannot have periodic behaviour: the function on $a^*$ whose last output letter
13	says whether the input has length at least two is aperiodic, while the one whose
14	last letter gives the parity of the length is not. By the arbitrary choice of
15	$w$ , the last $k$ output letters are eventually fixed as well, for every $k$ .
16	Theorem A.2.8 shows that the aperiodic functions computed by Mealy machines are
17	exactly the compositions of flip-flop machines.
18
19	# Formalization notes
20
21	The last letter is taken as an element of `Option B`: the definition asks that the
22	sequence `n ↦ (f (u vⁿ w)).getLast?` be eventually constant, "no letter" being an
23	admissible constant value. This is a deliberate correction of the printed
24	definition, which asks for an actual output letter `b`: with `u = v = w = ε` —
25	allowed, since the printed side condition "`uvw` nonempty" constrains the input,
26	and a length preserving function maps `ε` to `ε` — there is no last letter at
27	all, so no function would be aperiodic as printed. With the `Option`-valued
28	reading the whole of Section A.2.3 goes through. The book's side conditions that
29	`f` be length preserving and that `uvw` be nonempty are not used and are dropped.
30	`npow v n` is the string `vⁿ`.
31	-/
32
33	namespace Lax765601.Aperiodicity
34
35	/-- The `n`-fold concatenation `vⁿ` of a string with itself. -/
36	def npow {A : Type} (v : List A) : ℕ → List A
37	\| 0 => []
38	\| n + 1 => v ++ npow v n
39
40	/-- A string-to-string function is aperiodic if for all input strings `u, v, w` the
41	last letter of `f (u vⁿ w)` — as an element of `Option B`, so that "no letter" is
42	an admissible value — is the same for all sufficiently large `n`. -/
43	def Aperiodic {A B : Type} (f : List A → List B) : Prop :=
44	∀ u v w : List A, ∃ o : Option B, ∃ N : ℕ, ∀ n ≥ N, (f (u ++ npow v n ++ w)).getLast? = o
45
46	end Lax765601.Aperiodicity
47

Formalization notes

The last letter is taken as an element of $Option B$ : the definition asks that the sequence $n ↦ (f (u vⁿ w)).getLast?$ be eventually constant, "no letter" being an admissible constant value. This is a deliberate correction of the printed definition, which asks for an actual output letter $b$ : with $u = v = w = ε$ — allowed, since the printed side condition " $uvw$ nonempty" constrains the input, and a length preserving function maps $ε$ to $ε$ — there is no last letter at all, so no function would be aperiodic as printed. With the $Option$ -valued reading the whole of Section A.2.3 goes through. The book's side conditions that $f$ be length preserving and that $uvw$ be nonempty are not used and are dropped. $npow v n$ is the string $vⁿ$ .

Builds on

none

Used by

From Mathlib

Mathlib.Data.List.Basic

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