Lax Lean Archive

Map lifting

Lax765601.MapLifting · concepts/Lax765601/MapLifting.lean · lax-765601

definition

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Definition

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

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

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

    w1#w2#⋯#wn↦f(w1)#f(w2)#⋯#f(wn),w_1 \# w_2 \# \cdots \# w_n \quad\mapsto\quad f(w_1) \# f(w_2) \# \cdots \# f(w_n),

    where the strings w1,…,wnw_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.

    Concept map
    1 concept
    100%
    DefinitionThis conceptDescendants are omitted for concepts with more than 10 descendants.

    In the paper

    Lean source view on GitHub

    1import Mathlib.Data.List.Basic
    2
    3/-!
    4---
    5title: Map lifting
    6type: definition
    7---
    8Let f:A∗→B∗f : A^* \to B^* be a string-to-string function. Its *map lifting*
    9(Definition A.2.3 of *Transducers*) is the function
    10map f:(A+1)∗→(B+1)∗\mathsf{map}\, f : (A + 1)^* \to (B + 1)^*
    11over the alphabets extended by a fresh separator letter #\#, which applies ff to
    12every block of the input delimited by the separator:
    13w1#w2#⋯#wn↦f(w1)#f(w2)#⋯#f(wn),w_1 \# w_2 \# \cdots \# w_n \quad\mapsto\quad f(w_1) \# f(w_2) \# \cdots \# f(w_n),
    14where the strings w1,…,wnw_1, \ldots, w_n do not use the separator. The map lifting
    15is the construction by which a transducer is applied to a list of input strings
    16in parallel; it is used many times in the book, first in the proof of the
    17Krohn–Rhodes theorem (Lemma A.2.4), and the prime regular functions of Part C
    18are map liftings.
    19
    20# Formalization notes
    21
    22The alphabet `A + 1` is `Option A`, the separator being `none`. `splitSep` cuts a
    23string over `Option A` into its maximal separator-free blocks, always producing
    24one 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
    26concatenation of the images of the blocks with the separator put back between
    27them, 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
    29separator or with consecutive separators, which then delimit empty blocks.
    30-/
    31
    32namespace Lax765601.MapLifting
    33
    34/-- Cut a string over `A + 1` (the separator being `none`) into its maximal blocks
    35without the separator; there is always one block more than there are separators.
    36-/
    37def 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ₙ`. -/
    47def 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
    50end Lax765601.MapLifting
    51
    Formalization notes

    The alphabet A+1A + 1 is OptionAOption A, the separator being nonenone. splitSepsplitSep cuts a string over OptionAOption 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 mapLiftfmapLift 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 OptionAOption 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

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…