Lax Lean Archive

Evaluation of distance formulas on type trees

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

    Let φ(x̄) be a distFO formula of distance rank (k, q), G a partial graph and ā ∈ V(G)^ℓ with ℓ = |x̄| ≤ k. Then whether G ⊨ φ(ā) holds is decidable in polynomial time, given tree^G_{k,q}(ā) and φ.

    For a type tree τ = tree^G_{k,q}(ā) one writes τ ⊨ φ if G ⊨ φ(ā). The lemma shows that this depends on τ only.

    Concept map
    14 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.TypeTrees
    2import Lax185574.Algorithms
    3
    4/-!
    5---
    6title: Evaluation of distance formulas on type trees
    7type: lemma
    8---
    9Let φ(x̄) be a distFO formula of distance rank (k, q), G a partial graph
    10and ā ∈ V(G)^ℓ with ℓ = |x̄| ≤ k. Then whether G ⊨ φ(ā) holds is
    11decidable in polynomial time, given tree^G_{k,q}(ā) and φ.
    12
    13For a type tree τ = tree^G_{k,q}(ā) one writes τ ⊨ φ if G ⊨ φ(ā). The
    14lemma shows that this depends on τ only.
    15
    16# Formalization notes
    17
    18The algorithm is an algorithm in the sense of `Lax185574.Algorithms`,
    19one for all k and q. Its input is the pair of the type tree and the
    20formula. It decides whether `u` satisfies `φ` in time polynomial in the
    21size of the input, `O((N + 1)^a)` for an input of length `N`. The
    22degree `a` and the constant `c` may depend on k and q. The paper says
    23polynomial time, with no subscript, so this is weaker than a degree
    24independent of k and q. It suffices, since k and q are fixed in every
    25use. Running times of the paper of the form poly_{k,q} are formalized
    26in the same way. That the answer depends on τ alone is part of the
    27statement, because the output of the algorithm depends on its input
    28only.
    29-/
    30
    31namespace Lax185574.Evaluation
    32
    33open Lax185574.Encoding Lax185574.Algorithms
    34open Lax185574.PartialGraphs Lax185574.DistanceLogic Lax185574.DistanceLogic.DistFO
    35open Lax185574.TypeTrees
    36
    37/-- **Evaluation.** One algorithm decides, given `tree_{k,q}(u)` and a
    38formula `φ` of distance rank `(k, q)`, whether `u` satisfies `φ`, in
    39time polynomial in the size of the input. -/
    40axiom exists_program_eval :
    41 ∃ A : Algorithm, ∀ k q : ℕ, ∃ c a : ℕ,
    42 ∀ (n : ℕ) (G : PartialGraph (Fin n)) (ℓ : ℕ) (u : Fin ℓ → Fin n) (φ : DistFO ℓ),
    43 ℓ ≤ k → DRank k q φ →
    44 A.Decides c (tree G k q u, φ) (Sat G u φ)
    45 (((encode (tree G k q u)).length + (encode φ).length + 1) ^ a)
    46
    47end Lax185574.Evaluation
    48
    Show Proof
    Formalization notes

    The algorithm is an algorithm in the sense of Lax185574.AlgorithmsLax185574.Algorithms, one for all k and q. Its input is the pair of the type tree and the formula. It decides whether uu satisfies φφ in time polynomial in the size of the input, O((N+1)a)O((N + 1)^a) for an input of length NN. The degree aa and the constant cc may depend on k and q. The paper says polynomial time, with no subscript, so this is weaker than a degree independent of k and q. It suffices, since k and q are fixed in every use. Running times of the paper of the form poly_{k,q} are formalized in the same way. That the answer depends on τ alone is part of the statement, because the output of the algorithm depends on its input only.

    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…