Lax Lean Archive

The W-Hierarchy and the A-Hierarchy

Lax496464.WH_B4_Hierarchies · concepts/Lax496464/WH_B4_Hierarchies.lean · lax-496464

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

    For t≥0t \ge 0,

    W[t]:=[ p-WD-Πt ]fpt,A[t]:=[ p-MC(Σt) ]fpt:\mathrm{W}[t] := [\,p\text{-WD-}\Pi_t\,]^{\mathrm{fpt}}, \qquad \mathrm{A}[t] := [\,p\text{-MC}(\Sigma_t)\,]^{\mathrm{fpt}}:

    W[t]\mathrm{W}[t] is the class of parameterized problems that fpt-reduce to p-WDφp\text{-WD}_\varphi for some Πt\Pi_t-sentence φ(X)\varphi(X) [FG06, Definition 5.1], and A[t]\mathrm{A}[t] the class of those that fpt-reduce to model checking for Σt\Sigma_t-formulas [FG06, Definition 5.7].

    This characterization of the W-hierarchy by weighted Fagin definability is equivalent to the definition by weighted satisfiability of circuits of bounded weft [FG06, Theorems 5.6 and 7.20]. It places the classes, the model-checking problems and the reductions between them on the same objects, structures and first-order formulas.

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

    Lean source view on GitHub

    1import Lax496464.WH_B3_LogicProblems
    2import Lax496464.WH_A2_FptReductions
    3
    4/-!
    5---
    6title: The W-Hierarchy and the A-Hierarchy
    7type: definition
    8---
    9For t≥0t \ge 0,
    10
    11W[t]:=[ p-WD-Πt ]fpt,A[t]:=[ p-MC(Σt) ]fpt:\mathrm{W}[t] := [\,p\text{-WD-}\Pi_t\,]^{\mathrm{fpt}}, \qquad \mathrm{A}[t] := [\,p\text{-MC}(\Sigma_t)\,]^{\mathrm{fpt}}:
    12
    13
    14W[t]\mathrm{W}[t] is the class of parameterized problems that fpt-reduce to p-WDφp\text{-WD}_\varphi for
    15some Πt\Pi_t-sentence φ(X)\varphi(X) [FG06, Definition 5.1], and A[t]\mathrm{A}[t] the class of those
    16that fpt-reduce to model checking for Σt\Sigma_t-formulas [FG06, Definition 5.7].
    17
    18This characterization of the W-hierarchy by weighted Fagin definability is equivalent to the
    19definition by weighted satisfiability of circuits of bounded weft [FG06, Theorems 5.6 and 7.20]. It
    20places the classes, the model-checking problems and the reductions between them on the same
    21objects, structures and first-order formulas.
    22
    23# Formalization Notes
    24
    25p-WD-Πtp\text{-WD-}\Pi_t (`pWDPi t`) is the set of problems p-WDφp\text{-WD}_\varphi for all
    26Πt\Pi_t-sentences φ\varphi and all arities of XX; `W t` and `A t` are the closures of
    27`WH_A2_FptReductions.Closure`.
    28-/
    29
    30namespace Lax496464.WH_B4_Hierarchies
    31
    32open Lax496464.WH_B2_FirstOrder Lax496464.WH_B3_LogicProblems Lax496464.WH_A2_FptReductions
    33open Lax888481.ParameterizedComplexity (Problem)
    34
    35/-- **`p-WD-Π_t`**: the weighted definability problems of `Π_t`-sentences. -/
    36def pWDPi (t : ℕ) : Set Problem :=
    37 {P | ∃ (φ : Formula) (s : ℕ), IsPi t φ ∧ IsSentence φ ∧ P = pWD φ s}
    38
    39/-- **`W[t]`**, the `t`-th class of the W-hierarchy. -/
    40def W (t : ℕ) : Set Problem := Closure (pWDPi t)
    41
    42/-- **`A[t]`**, the `t`-th class of the A-hierarchy. -/
    43noncomputable def A (t : ℕ) : Set Problem := Closure {pMC {φ | IsSigma t φ}}
    44
    45end Lax496464.WH_B4_Hierarchies
    46
    Formalization Notes

    p-WD-Πtp\text{-WD-}\Pi_t (pWDPitpWDPi t) is the set of problems p-WDφp\text{-WD}_\varphi for all Πt\Pi_t-sentences φ\varphi and all arities of XX; WtW t and AtA t are the closures of WHA2FptReductions.ClosureWH_A2_FptReductions.Closure.

    Builds on
    Used by
    From Mathlib

    none

    Discussion

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

    Loading discussion…