Lax Lean Archive

Canonical form

Lax185574.CanonicalForm · concepts/Lax185574/CanonicalForm.lean · lax-185574

proven

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

    Observation

    A type tree given by a representation whose sets need not be sorted or duplicate-free can be brought into canonical form in polynomial time.

    Concept map
    8 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    Each proof establishes this claim relative to its assumptions.

    In the paper

    • page 42 of this submission's paper

    Lean source view on GitHub

    1import Lax185574.Algorithms
    2
    3/-!
    4---
    5title: Canonical form
    6type: observation
    7---
    8A type tree given by a representation whose sets need not be sorted or
    9duplicate-free can be brought into canonical form in polynomial time.
    10
    11# Formalization notes
    12
    13The statement is made for one set: a list of elements of an encoded
    14type, possibly unsorted and with repetitions, is turned into the finite
    15set of its entries, whose encoding is the sorted duplicate-free list of
    16the encodings of the elements. The algorithm receives the list of the
    17encodings of the elements, so every element is preceded by its length,
    18and it can find the boundaries of the elements without knowing their
    19type. One algorithm works for all types. A type tree is brought into
    20canonical form by applying this at every node, from the leaves up. That
    21step is part of the proofs that use it.
    22
    23The algorithm is an algorithm in the sense of `Lax185574.Algorithms`.
    24Polynomial time means time `O((N + 1)^a)` on an input of length `N`.
    25The finite set `l.toFinset` needs decidable equality of the elements,
    26which every type has classically.
    27-/
    28
    29namespace Lax185574.CanonicalForm
    30
    31open Lax185574.Encoding Lax185574.Algorithms
    32
    33/-- **Canonical form.** One algorithm turns a list of elements, given by
    34their encodings, into the finite set of its entries, in polynomial time.
    35It sorts the encodings and removes duplicates. -/
    36axiom exists_program_canonical :
    37 ∃ (A : Algorithm) (c a : ℕ), ∀ (α : Type) [Encode α] [DecidableEq α] (l : List α),
    38 A.Computes c (l.map encode) l.toFinset (((encode (l.map encode)).length + 1) ^ a)
    39
    40end Lax185574.CanonicalForm
    41
    Show Proof
    Formalization notes

    The statement is made for one set: a list of elements of an encoded type, possibly unsorted and with repetitions, is turned into the finite set of its entries, whose encoding is the sorted duplicate-free list of the encodings of the elements. The algorithm receives the list of the encodings of the elements, so every element is preceded by its length, and it can find the boundaries of the elements without knowing their type. One algorithm works for all types. A type tree is brought into canonical form by applying this at every node, from the leaves up. That step is part of the proofs that use it.

    The algorithm is an algorithm in the sense of Lax185574.AlgorithmsLax185574.Algorithms. Polynomial time means time O((N+1)a)O((N + 1)^a) on an input of length NN. The finite set l.toFinsetl.toFinset needs decidable equality of the elements, which every type has classically.

    Builds on
    Used by

    none

    From Mathlib

    none

    Discussion

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

    Loading discussion…