Lax Lean Archive

Draft — mutable and not usable as a dependency; its citation marks the draft state.

Lax916827.RegularFunctions

Regular functions

concepts/Lax916827/RegularFunctions.lean · lax-916827

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.

    Concept map

    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    In the paper

    Definition

    The map reverse function is the map lifting of string reversal, applied blockwise between separators, and the map duplicate function is the map lifting of string duplication w↦www \mapsto ww:

    123#45#6789↦321#54#9876,123#45#6789↦123123#4545#67896789.123\#45\#6789 \mapsto 321\#54\#9876, \qquad 123\#45\#6789 \mapsto 123123\#4545\#67896789.

    Neither is rational. A string-to-string function is regular (Definition C.0.1 of Transducers) if it can be obtained as a finite composition of functions each of which is a rational function, a map reverse function or a map duplicate function. The regular functions are the third step of the transducer ladder; Part C shows that they are the functions of two-way transducers, of streaming string transducers, of string-to-string mso transductions and of regular terms.

    Lean source view on GitHub

    1import Lax765601.MapLifting
    2import Lax765601.CompositionClosure
    3import Lax132576.RationalFunctions
    4
    5/-!
    6---
    7title: Regular functions
    8type: definition
    9---
    10The *map reverse* function is the map lifting of string reversal, applied
    11blockwise between separators, and the *map duplicate* function is the map
    12lifting of string duplication w↦www \mapsto ww:
    13123#45#6789↦321#54#9876,123#45#6789↦123123#4545#67896789.123\#45\#6789 \mapsto 321\#54\#9876, \qquad 123\#45\#6789 \mapsto 123123\#4545\#67896789.
    14Neither is rational. A string-to-string function is *regular* (Definition
    15C.0.1 of *Transducers*) if it can be obtained as a finite composition of
    16functions each of which is a rational function, a map reverse function or a map
    17duplicate function. The regular functions are the third step of the transducer
    18ladder; Part C shows that they are the functions of two-way transducers,
    19of streaming string transducers, of string-to-string mso transductions and of
    20regular terms.
    21
    22# Formalization notes
    23
    24Map reverse and map duplicate are families of functions, one for every
    25alphabet `A`, of type `(A + 1)* → (A + 1)*` with `Option A` for `A + 1`. In the
    26family `RegularFam` they appear up to renaming: `f : A* → B*` is a map reverse if
    27the alphabets are in bijection with some `Option A₀` and `f` is `mapReverse A₀`
    28transported along the bijections. `IsRegularFun` is the composition closure of
    29`Lax765601.CompositionClosure`.
    30-/
    31
    32namespace Lax916827.RegularFunctions
    33
    34open Lax765601.MapLifting Lax765601.CompositionClosure Lax132576.RationalFunctions
    35
    36/-- The map reverse function `w₁ # ⋯ # wₙ ↦ reverse w₁ # ⋯ # reverse wₙ`. -/
    37def mapReverse (A : Type) : List (Option A) → List (Option A) := mapLift List.reverse
    38
    39/-- The map duplicate function `w₁ # ⋯ # wₙ ↦ w₁w₁ # ⋯ # wₙwₙ`. -/
    40def mapDuplicate (A : Type) : List (Option A) → List (Option A) := mapLift (fun w => w ++ w)
    41
    42/-- The family of prime regular functions: rational functions, and the map reverse
    43and map duplicate functions, up to a renaming of the alphabets. -/
    44def RegularFam : Family := fun A B f =>
    45 IsRationalFun f ∨
    46 (∃ (A₀ : Type) (e : A ≃ Option A₀) (e' : B ≃ Option A₀),
    47 ∀ w, f w = (mapReverse A₀ (w.map e)).map e'.symm) ∨
    48 (∃ (A₀ : Type) (e : A ≃ Option A₀) (e' : B ≃ Option A₀),
    49 ∀ w, f w = (mapDuplicate A₀ (w.map e)).map e'.symm)
    50
    51/-- A string-to-string function is regular if it is a finite composition of
    52rational functions, map reverse and map duplicate. -/
    53def IsRegularFun {A B : Type} (f : List A → List B) : Prop := CompClosure RegularFam A B f
    54
    55end Lax916827.RegularFunctions
    56

    Formalization notes

    Map reverse and map duplicate are families of functions, one for every alphabet AA, of type (A+1)∗→(A+1)∗(A + 1)* → (A + 1)* with OptionAOption A for A+1A + 1. In the family RegularFamRegularFam they appear up to renaming: f:A∗→B∗f : A* → B* is a map reverse if the alphabets are in bijection with some OptionA0Option A₀ and ff is mapReverseA0mapReverse A₀ transported along the bijections. IsRegularFunIsRegularFun is the composition closure of Lax765601.CompositionClosureLax765601.CompositionClosure.

    Builds on

    Used by

    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…