Lax Lean Archive

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

Lax194892.PolyregularFunctions

Polyregular functions

concepts/Lax194892/PolyregularFunctions.lean · lax-194892

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

    A string-to-string function is polyregular (Definition D.0.1 of Transducers) if it can be obtained as a finite composition of functions each of which is either regular or a marked squaring function:

    polyregular=(regular∪marked squaring)∗.\text{polyregular} = (\text{regular} \cup \text{marked squaring})^*.

    The polyregular functions are the top step of the book's transducer ladder; Part D shows that they are the functions of for-transducers and of pebble transducers.

    Lean source view on GitHub

    1import Lax765601.CompositionClosure
    2import Lax916827.RegularFunctions
    3import Lax194892.MarkedSquaring
    4
    5/-!
    6---
    7title: Polyregular functions
    8type: definition
    9---
    10A string-to-string function is *polyregular* (Definition D.0.1 of
    11*Transducers*) if it can be obtained as a finite composition of functions each
    12of which is either regular or a marked squaring function:
    13polyregular=(regular∪marked squaring)∗.\text{polyregular} = (\text{regular} \cup \text{marked squaring})^*.
    14The polyregular functions are the top step of the book's transducer ladder;
    15Part D shows that they are the functions of for-transducers and of pebble
    16transducers.
    17
    18# Formalization notes
    19
    20As for the regular functions, marked squaring appears in the family up to a
    21renaming of the alphabets by bijections `A ≃ A₀` and `B ≃ A₀ ⊕ A₀`;
    22`IsPolyregular` is the composition closure of `Lax765601.CompositionClosure`.
    23-/
    24
    25namespace Lax194892.PolyregularFunctions
    26
    27open Lax765601.CompositionClosure Lax916827.RegularFunctions Lax194892.MarkedSquaring
    28
    29/-- The family of prime polyregular functions: regular functions and marked
    30squaring, up to a renaming of the alphabets. -/
    31def PolyregularFam : Family := fun A B f =>
    32 IsRegularFun f ∨
    33 (∃ (A₀ : Type) (e : A ≃ A₀) (e' : B ≃ A₀ ⊕ A₀),
    34 ∀ w, f w = (markedSquare A₀ (w.map e)).map e'.symm)
    35
    36/-- A function is polyregular if it is a finite composition of regular functions
    37and marked squaring. -/
    38def IsPolyregular {A B : Type} (f : List A → List B) : Prop := CompClosure PolyregularFam A B f
    39
    40end Lax194892.PolyregularFunctions
    41

    Formalization notes

    As for the regular functions, marked squaring appears in the family up to a renaming of the alphabets by bijections A≃A0A ≃ A₀ and B≃A0⊕A0B ≃ A₀ ⊕ A₀; IsPolyregularIsPolyregular 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…