Lax765601.MapLifting

Map lifting

concepts/Lax765601/MapLifting.lean · lax-765601

definition

Loading review…

Concept map

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

In the paper

page 21 of the paper of lax-157538, Transducers

Definition

Let $f : A^* \to B^*$ be a string-to-string function. Its map lifting (Definition A.2.3 of Transducers) is the function

\mathsf{map}\, f : (A + 1)^* \to (B + 1)^*

over the alphabets extended by a fresh separator letter $\#$ , which applies $f$ to every block of the input delimited by the separator:

w_1 \# w_2 \# \cdots \# w_n \quad\mapsto\quad f(w_1) \# f(w_2) \# \cdots \# f(w_n),

where the strings $w_1, \ldots, w_n$ do not use the separator. The map lifting is the construction by which a transducer is applied to a list of input strings in parallel; it is used many times in the book, first in the proof of the Krohn–Rhodes theorem (Lemma A.2.4), and the prime regular functions of Part C are map liftings.

Lean source view on GitHub

1	import Mathlib.Data.List.Basic
2
3	/-!
4	---
5	title: Map lifting
6	type: definition
7	---
8	Let $f : A^* \to B^$ be a string-to-string function. Its map lifting*
9	(Definition A.2.3 of Transducers) is the function
10	$\mathsf{map}\, f : (A + 1)^* \to (B + 1)^*$
11	over the alphabets extended by a fresh separator letter $\#$ , which applies $f$ to
12	every block of the input delimited by the separator:
13	$w_1 \# w_2 \# \cdots \# w_n \quad\mapsto\quad f(w_1) \# f(w_2) \# \cdots \# f(w_n),$
14	where the strings $w_1, \ldots, w_n$ do not use the separator. The map lifting
15	is the construction by which a transducer is applied to a list of input strings
16	in parallel; it is used many times in the book, first in the proof of the
17	Krohn–Rhodes theorem (Lemma A.2.4), and the prime regular functions of Part C
18	are map liftings.
19
20	# Formalization notes
21
22	The alphabet `A + 1` is `Option A`, the separator being `none`. `splitSep` cuts a
23	string over `Option A` into its maximal separator-free blocks, always producing
24	one block more than there are separators — the empty string is the one block
25	`[]`, and `w #` ends with an empty block — so that `mapLift f` is the
26	concatenation of the images of the blocks with the separator put back between
27	them, exactly as displayed. With this reading the map lifting is defined on
28	every string over `Option A`, including those beginning or ending with a
29	separator or with consecutive separators, which then delimit empty blocks.
30	-/
31
32	namespace Lax765601.MapLifting
33
34	/-- Cut a string over `A + 1` (the separator being `none`) into its maximal blocks
35	without the separator; there is always one block more than there are separators.
36	-/
37	def splitSep {A : Type} : List (Option A) → List (List A)
38	\| [] => [[]]
39	\| none :: w => [] :: splitSep w
40	\| some a :: w =>
41	match splitSep w with
42	\| [] => [[a]]
43	\| u :: us => (a :: u) :: us
44
45	/-- The map lifting of `f`: apply `f` to every block delimited by the separator,
46	`w₁ # ⋯ # wₙ ↦ f w₁ # ⋯ # f wₙ`. -/
47	def mapLift {A B : Type} (f : List A → List B) (w : List (Option A)) : List (Option B) :=
48	List.intercalate [none] ((splitSep w).map (fun u => (f u).map some))
49
50	end Lax765601.MapLifting
51

Formalization notes

The alphabet $A + 1$ is $Option A$ , the separator being $none$ . $splitSep$ cuts a string over $Option A$ into its maximal separator-free blocks, always producing one block more than there are separators — the empty string is the one block $[]$ , and `w #` ends with an empty block — so that $mapLift f$ is the concatenation of the images of the blocks with the separator put back between them, exactly as displayed. With this reading the map lifting is defined on every string over $Option A$ , including those beginning or ending with a separator or with consecutive separators, which then delimit empty blocks.

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