Lax Lean Archive

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

Lax194892.MarkedSquaring

Marked squaring

concepts/Lax194892/MarkedSquaring.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

    The marked squaring function (Example 33 of Transducers) copies an input string of length nn exactly nn times, underlining the first ii letters of the ii-th copy:

    1234↦1‾234  12‾34  123‾4  1234‾.1234 \mapsto \underline{1}234\;\underline{12}34\;\underline{123}4\;\underline{1234}.

    The output has length n2n^2 over the alphabet A+AA + A, one copy of the input alphabet underlined and one plain. It is the one prime function of quadratic growth that, added to the regular functions, generates the polyregular functions (Definition D.0.1).

    Lean source view on GitHub

    1import Mathlib.Data.List.Basic
    2
    3/-!
    4---
    5title: Marked squaring
    6type: definition
    7---
    8The *marked squaring* function (Example 33 of *Transducers*) copies an input
    9string of length nn exactly nn times, underlining the first ii letters of the
    10ii-th copy:
    111234↦1‾234  12‾34  123‾4  1234‾.1234 \mapsto \underline{1}234\;\underline{12}34\;\underline{123}4\;\underline{1234}.
    12The output has length n2n^2 over the alphabet A+AA + A, one copy of the input
    13alphabet underlined and one plain. It is the one prime function of quadratic
    14growth that, added to the regular functions, generates the polyregular
    15functions (Definition D.0.1).
    16
    17# Formalization notes
    18
    19Underlined letters are `Sum.inl`, plain ones `Sum.inr`; the `i`-th copy is
    20`(w.take (i+1)).map Sum.inl ++ (w.drop (i+1)).map Sum.inr`. Marked squaring is a
    21family of functions, one for each alphabet.
    22-/
    23
    24namespace Lax194892.MarkedSquaring
    25
    26/-- Marked squaring: `n` copies of an input of length `n`, the first `i` letters
    27of the `i`-th copy underlined. -/
    28def markedSquare (A : Type) (w : List A) : List (A ⊕ A) :=
    29 ((List.range w.length).map
    30 (fun i => (w.take (i + 1)).map Sum.inl ++ (w.drop (i + 1)).map Sum.inr)).flatten
    31
    32end Lax194892.MarkedSquaring
    33

    Formalization notes

    Underlined letters are Sum.inlSum.inl, plain ones Sum.inrSum.inr; the ii-th copy is (w.take(i+1)).mapSum.inl++(w.drop(i+1)).mapSum.inr(w.take (i+1)).map Sum.inl ++ (w.drop (i+1)).map Sum.inr. Marked squaring is a family of functions, one for each alphabet.

    Builds on

    none

    Used by

    From Mathlib

    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…