Lax765601.ElementaryProperties

Prefix preservation and length preservation

concepts/Lax765601/ElementaryProperties.lean · lax-765601

definition

Loading review…

Concept map

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

In the paper

page 66 of the paper of lax-157538, Transducers

Definition

Three elementary properties of a string-to-string function $f : A^* \to B^*$ that the characterisation theorems of the book are stated with.

$f$ is prefix preserving if $w \sqsubseteq v$ implies $f(w) \sqsubseteq f(v)$ , where $\sqsubseteq$ is the prefix order on strings.
$f$ is length preserving, or letter-to-letter, if $|f(w)| = |w|$ for every input string $w$ .
$f$ is prefix determined if the first $n$ output letters depend only on the first $n$ input letters: input strings that agree on their first $n$ letters have outputs that agree on their first $n$ letters.

For a letter-to-letter function, being prefix determined says exactly that the $n$ -th output letter depends only on the first $n$ input letters, which is condition (3) of the Myhill–Nerode lemma for Mealy machines (Lemma A.2.10), and it is the determinism condition of Theorem B.2.7; prefix preservation and length preservation together are the shape of the machine-independent characterisation of Mealy machines (Theorem B.4.1).

Lean source view on GitHub

1	import Mathlib.Data.List.Infix
2
3	/-!
4	---
5	title: Prefix preservation and length preservation
6	type: definition
7	---
8	Three elementary properties of a string-to-string function $f : A^* \to B^*$ that
9	the characterisation theorems of the book are stated with.
10
11	* $f$ is prefix preserving if $w \sqsubseteq v$ implies $f(w) \sqsubseteq f(v)$ ,
12	where $\sqsubseteq$ is the prefix order on strings.
13	* $f$ is length preserving, or letter-to-letter, if $\|f(w)\| = \|w\|$ for every
14	input string $w$ .
15	* $f$ is prefix determined if the first $n$ output letters depend only on the
16	first $n$ input letters: input strings that agree on their first $n$ letters
17	have outputs that agree on their first $n$ letters.
18
19	For a letter-to-letter function, being prefix determined says exactly that the
20	$n$ -th output letter depends only on the first $n$ input letters, which is
21	condition (3) of the Myhill–Nerode lemma for Mealy machines (Lemma A.2.10), and
22	it is the determinism condition of Theorem B.2.7; prefix preservation and length
23	preservation together are the shape of the machine-independent characterisation
24	of Mealy machines (Theorem B.4.1).
25
26	# Formalization notes
27
28	`<+:` is mathlib's prefix relation on lists. The three definitions quantify over
29	all strings of the input alphabet and carry no finiteness hypothesis.
30	-/
31
32	namespace Lax765601.ElementaryProperties
33
34	/-- `f` is prefix preserving: `w ⊑ v` implies `f w ⊑ f v`. -/
35	def PrefixPreserving {A B : Type} (f : List A → List B) : Prop :=
36	∀ w v : List A, w <+: v → f w <+: f v
37
38	/-- `f` is length preserving, i.e. letter-to-letter: the output has the length of
39	the input. -/
40	def LengthPreserving {A B : Type} (f : List A → List B) : Prop :=
41	∀ w : List A, (f w).length = w.length
42
43	/-- `f` is prefix determined: the first `n` output letters depend only on the
44	first `n` input letters. -/
45	def PrefixDetermined {A B : Type} (f : List A → List B) : Prop :=
46	∀ (w v : List A) (n : ℕ), w.take n = v.take n → (f w).take n = (f v).take n
47
48	end Lax765601.ElementaryProperties
49

Formalization notes

$<+:$ is mathlib's prefix relation on lists. The three definitions quantify over all strings of the input alphabet and carry no finiteness hypothesis.

Builds on

none

Used by

From Mathlib

Mathlib.Data.List.Infix

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