Lax Lean Archive

Lifting type trees through a merge

Lax185574.MergeLift · concepts/Lax185574/MergeLift.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

    Lemma

    Fix ℓ ≤ k and q ∈ ℕ. Let G be a partial graph and ā ∈ V(G)^ℓ. Given tree^G_{k,q}(ā) and two distinct colors P, Q, one can compute tree^H_{k,q}(ā), where H = merge_{P,Q}(G), in time poly_{k,q}(‖tree^G_{k,q}(ā)‖).

    Concept map
    15 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 48 of this submission's paper

    Lean source view on GitHub

    1import Lax185574.TypeTrees
    2import Lax185574.ConstructionSequences
    3import Lax185574.Algorithms
    4
    5/-!
    6---
    7title: Lifting type trees through a merge
    8type: lemma
    9---
    10Fix ℓ ≤ k and q ∈ ℕ. Let G be a partial graph and ā ∈ V(G)^ℓ. Given
    11tree^G_{k,q}(ā) and two distinct colors P, Q, one can compute
    12tree^H_{k,q}(ā), where H = merge_{P,Q}(G), in time
    13poly_{k,q}(‖tree^G_{k,q}(ā)‖).
    14
    15# Formalization notes
    16
    17The merge is `Lax185574.ConstructionSequences.merge`, which recolors Q
    18to P. The algorithm is an algorithm in the sense of
    19`Lax185574.Algorithms`, one for all k and q. Its input is the triple of
    20the type tree, P and Q. The size ‖τ‖ is the length of the encoding of
    21τ, and the time is `O((‖τ‖ + 1)^a)`, where the degree `a` and the
    22constant `c` may depend on k and q.
    23-/
    24
    25namespace Lax185574.MergeLift
    26
    27open Lax185574.Encoding Lax185574.Algorithms
    28open Lax185574.PartialGraphs Lax185574.TypeTrees Lax185574.ConstructionSequences
    29
    30/-- **Merge lift.** One algorithm computes the type tree of a tuple
    31after a merge from its type tree before, in time polynomial in the size
    32of the tree. -/
    33axiom exists_program_mergeLift :
    34 ∃ A : Algorithm, ∀ k q : ℕ, ∃ c a : ℕ,
    35 ∀ (n : ℕ) (G : PartialGraph (Fin n)) (ℓ : ℕ) (u : Fin ℓ → Fin n) (P Q : ℕ),
    36 ℓ ≤ k → P ≠ Q →
    37 A.Computes c (tree G k q u, P, Q) (tree (merge G P Q) k q u)
    38 (((encode (tree G k q u)).length + 1) ^ a)
    39
    40end Lax185574.MergeLift
    41
    Show Proof
    Formalization notes

    The merge is Lax185574.ConstructionSequences.mergeLax185574.ConstructionSequences.merge, which recolors Q to P. The algorithm is an algorithm in the sense of Lax185574.AlgorithmsLax185574.Algorithms, one for all k and q. Its input is the triple of the type tree, P and Q. The size ‖τ‖ is the length of the encoding of τ, and the time is O((‖τ‖+1)a)O((‖τ‖ + 1)^a), where the degree aa and the constant cc may depend on k and q.

    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…