Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Decision problems of the core on bit strings

Lax832283.StringProblems · concepts/Lax832283/StringProblems.lean · lax-832283

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.

    Natural Language Statement

    Definition

    A vocabulary of the NP core, with finitely many relation symbols, is numbered by a list of arities. A table of the Immerman–Vardi entry, of that list of arities, then reads as a structure on an initial segment of the natural numbers, and a decision problem of the core reads as a property of tables and as a Boolean query. The empty table is a no-instance, the classes of the core being about nonempty structures. A word that encodes no table is in no language of the two entries, so nothing else needs care.

    Concept map
    5 concepts; 2 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Lean source view on GitHub

    1import Mathlib.ModelTheory.Syntax
    2import Mathlib.Data.Fin.Tuple.Basic
    3import Mathlib.Logic.Equiv.Fin.Basic
    4import Mathlib.Data.List.OfFn
    5import Mathlib.Data.Finite.Card
    6import Mathlib.Algebra.BigOperators.Group.List.Basic
    7import Mathlib.Algebra.Group.Nat.Defs
    8import Mathlib.Algebra.Group.Action.Defs
    9import Mathlib.Data.List.FinRange
    10import Mathlib.ModelTheory.Semantics
    11import Mathlib.ModelTheory.Complexity
    12import Mathlib.Tactic.FinCases
    13import Lax751879.OrderedStructures
    14import Lax904597.Problems
    15import Lax988886.FiniteStructures
    16
    17/-!
    18---
    19title: Decision problems of the core on bit strings
    20type: definition
    21---
    22A vocabulary of the NP core, with finitely many relation symbols, is numbered by a
    23list of arities. A table of the Immerman–Vardi entry, of that list of arities, then reads
    24as a structure on an initial segment of the natural numbers, and a decision problem of
    25the core reads as a property of tables and as a Boolean query. The empty table is a
    26no-instance, the classes of the core being about nonempty structures. A word that encodes
    27no table is in no language of the two entries, so nothing else needs care.
    28-/
    29
    30namespace Lax832283.StringProblems
    31
    32open Lax751879.OrderedStructures Lax904597.Problems Lax988886.FiniteStructures
    33
    34open FirstOrder
    35
    36/-- An enumeration of the relation symbols of `L`, listing their arities. -/
    37structure FinVocab (L : Language.{0, 0}) where
    38 /-- The arities of the symbols, in the order of the enumeration. -/
    39 σ : List ℕ
    40 /-- The symbol of a given number, with its arity. -/
    41 sym : Fin σ.length ≃ Σ n, L.Relations n
    42 /-- The list records the arity of each symbol. -/
    43 arity_sym : ∀ i, (sym i).1 = σ.get i
    44
    45namespace FinVocab
    46
    47variable {L : Language.{0, 0}}
    48
    49variable (V : FinVocab L)
    50
    51/-- The number of a given symbol. -/
    52def toSym {n : ℕ} (R : L.Relations n) : Fin V.σ.length :=
    53 V.sym.symm ⟨n, R⟩
    54
    55end FinVocab
    56
    57open FirstOrder Language Structure
    58
    59
    60
    61variable {L : Language.{0, 0}}
    62
    63/-- Read a table of the archive's formalism as a structure of the library. -/
    64@[reducible]
    65def ofOrdered [L.IsRelational] (V : FinVocab L) (S : OrderedStructure V.σ) :
    66 L.Structure (Fin S.size) where
    67 funMap f := isEmptyElim f
    68 RelMap {n} R v := S.relation (V.toSym R) (v ∘ Fin.cast
    69 (show V.σ.get (V.toSym R) = n by rw [← V.arity_sym, FinVocab.toSym, Equiv.apply_symm_apply]))
    70 = true
    71
    72/-- A decision problem of the library, as a property of the archive's structures. The
    73empty structure is a no-instance. -/
    74def toProperty [L.IsRelational] (V : FinVocab L) (P : DecisionProblem L) :
    75 Property V.σ :=
    76 fun S => 0 < S.size ∧ @DecisionProblem.Holds L _ P (Fin S.size) (ofOrdered V S)
    77
    78/-- A decision problem of the library, as a Boolean query on ordered structures. -/
    79def toQuery [L.IsRelational] (V : FinVocab L) (P : DecisionProblem L) : Query V.σ 0 :=
    80 fun S => toProperty V P S.structureValue
    81
    82end Lax832283.StringProblems
    83
    Builds on
    Used by
    From Mathlib

    Discussion

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

    Loading discussion…