Lax Lean Archive

Decoding, and well-formed evaluation is NP-complete

Lax420092.DecodingAndWellFormed · concepts/Lax420092/DecodingAndWellFormed.lean · lax-420092

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

    Theorem

    The decoder is sound: an instance it reads off a presented structure has a satisfied query exactly when the presented structure is a yes-instance of CQEval. It is total on well-formed structures: every nonempty presented structure with a constant decodes to an instance. And well-formed evaluation, whose yes-instances are exactly the structures with a constant whose query holds, is NP-complete, so the restriction the decoder needs loses nothing.

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

    This concept declares 4 statements. Each proof establishes one of them relative to its assumptions.

    1 cqDecode_sound proven

    2 cqDecode_total proven

    3 wfCQEval_iff proven

    4 wfCQEval_NP_complete proven

    Lean source view on GitHub

    1import Lax904597.Problems
    2import Lax904597.Interpretations
    3import Lax904597.Classes
    4import Lax799700.Problems
    5import Lax420092.QueryDatabases
    6import Lax420092.Evaluation
    7import Lax420092.QueryPairs
    8import Lax420092.PackagedInstances
    9
    10/-!
    11---
    12title: Decoding, and well-formed evaluation is NP-complete
    13type: theorem
    14---
    15The decoder is sound: an instance it reads off a presented structure has a
    16satisfied query exactly when the presented structure is a yes-instance of
    17CQEval. It is total on well-formed structures: every nonempty presented
    18structure with a constant decodes to an instance. And well-formed
    19evaluation, whose yes-instances are exactly the structures with a constant
    20whose query holds, is NP-complete, so the restriction the decoder needs
    21loses nothing.
    22-/
    23
    24namespace Lax420092.DecodingAndWellFormed
    25
    26open FirstOrder FirstOrder.Language
    27open Lax904597.Problems Lax904597.Interpretations Lax904597.Classes Lax799700.Problems
    28open Lax420092.QueryDatabases Lax420092.Evaluation Lax420092.QueryPairs Lax420092.PackagedInstances
    29
    30/-- The decoder is sound. -/
    31axiom cqDecode_sound : ∀ (S : FinPresentation queryDb) (i : CQInstance),
    32 i ∈ cqDecode S → (ConcreteCQHolds i ↔ CQEval (Fin S.card))
    33
    34/-- The decoder is total on well-formed structures. -/
    35axiom cqDecode_total : ∀ S : FinPresentation queryDb,
    36 0 < S.card → Fin S.card ⊨ cqWFSentence → (cqDecode S).isSome
    37
    38/-- The yes-instances of WFCQEval are exactly the structures with a constant
    39whose query holds. -/
    40axiom wfCQEval_iff : ∀ (A : Type) [queryDb.Structure A],
    41 WFCQEval A ↔ (A ⊨ cqWFSentence ∧ QueryHolds A)
    42
    43/-- WFCQEval is NP-complete. -/
    44axiom wfCQEval_NP_complete : NP.Complete WFCQEval
    45
    46end Lax420092.DecodingAndWellFormed
    47
    Show ProofShow ProofShow ProofShow Proof
    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…