Lax Lean Archive

Model Checking and Weighted Fagin Definability

Lax496464.WH_B3_LogicProblems · concepts/Lax496464/WH_B3_LogicProblems.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

    The two families of parameterized problems that define the hierarchies.

    Model checking p-MC(Φ)p\text{-MC}(\Phi) for a class Φ\Phi of formulas. Instance: a structure A\mathcal A and a formula φ∈Φ\varphi \in \Phi. Parameter: ∣φ∣|\varphi|. Question: is φ(A)≠∅\varphi(\mathcal A) \ne \emptyset, that is, do some elements of A\mathcal A satisfy φ\varphi when assigned to its free variables? [FG06, Section 4.2]

    Weighted Fagin definability p-WDφp\text{-WD}_\varphi for a formula φ(X)\varphi(X) with a free relation variable XX of arity ss. Instance: a structure A\mathcal A and k∈Nk \in \mathbb N. Parameter: kk. Question: is there a relation S⊆AsS \subseteq A^s with ∣S∣=k|S| = k such that A⊨φ(S)\mathcal A \models \varphi(S)? [FG06, p. 95]

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

    Lean source view on GitHub

    1import Lax496464.WH_B2_FirstOrder
    2import Lax888481.ParameterizedComplexity
    3
    4/-!
    5---
    6title: Model Checking and Weighted Fagin Definability
    7type: definition
    8---
    9The two families of parameterized problems that define the hierarchies.
    10
    11**Model checking** p-MC(Φ)p\text{-MC}(\Phi) for a class Φ\Phi of formulas. *Instance:* a structure
    12A\mathcal A and a formula φ∈Φ\varphi \in \Phi. *Parameter:* ∣φ∣|\varphi|. *Question:* is
    13φ(A)≠∅\varphi(\mathcal A) \ne \emptyset, that is, do some elements of A\mathcal A satisfy φ\varphi
    14when assigned to its free variables? [FG06, Section 4.2]
    15
    16**Weighted Fagin definability** p-WDφp\text{-WD}_\varphi for a formula φ(X)\varphi(X) with a free relation
    17variable XX of arity ss. *Instance:* a structure A\mathcal A and k∈Nk \in \mathbb N.
    18*Parameter:* kk. *Question:* is there a relation S⊆AsS \subseteq A^s with ∣S∣=k|S| = k such that
    19A⊨φ(S)\mathcal A \models \varphi(S)? [FG06, p. 95]
    20
    21# Formalization Notes
    22
    23**Words.** An instance of model checking is the word of the structure followed by the word of the
    24formula; an instance of weighted definability is the word of the structure followed by kk. Both
    25parts are self-delimiting, so a word determines them. The parameter is the size of the formula, or
    26the last entry.
    27
    28**Model checking.** The formula does not use the relation variable, and it is false in a structure
    29whose vocabulary it does not fit. Its free variables range over the universe. The class Φ\Phi
    30restricts the instances only: the yes-instances of p-MC(Φ)p\text{-MC}(\Phi) are those of
    31p-MC(Φ′)p\text{-MC}(\Phi') for every Φ′⊇Φ\Phi' \supseteq \Phi that lie in the smaller domain.
    32
    33**Weighted definability.** The formula of p-WDφp\text{-WD}_\varphi is fixed, so each formula and arity
    34give one problem. The formulas defining the hierarchies are sentences, evaluated under an arbitrary
    35assignment (here the one sending every variable to 00). A relation of kk tuples is a finite set
    36of lists of length ss over the universe. A formula that does not fit the vocabulary has no
    37witness.
    38-/
    39
    40namespace Lax496464.WH_B3_LogicProblems
    41
    42open Lax496464.WH_B1_Structures Lax496464.WH_B2_FirstOrder
    43open Lax888481.ParameterizedComplexity (Problem)
    44
    45/-- The word `x` is the word of the structure `A` followed by the word of the formula `φ`. -/
    46def EncodesMC (x : List ℕ) (A : Structure) (φ : Formula) : Prop :=
    47 ∃ y, Encodes y A ∧ x = y ++ φ.encode
    48
    49/-- `φ(A) ≠ ∅`: the formula fits the vocabulary of `A`, does not use the relation variable, and is
    50satisfied by some assignment of universe elements to its free variables. -/
    51def Models (A : Structure) (φ : Formula) : Prop :=
    52 φ.Fits A.arities 0 ∧ φ.NoSetVar ∧
    53 ∃ ρ : Assignment, (∀ v ∈ φ.freeVars, ρ v < A.size) ∧ Sat A ∅ φ ρ
    54
    55open Classical in
    56/-- The parameter of a model-checking word: the size of its formula (`0` on other words). -/
    57noncomputable def mcParam (x : List ℕ) : ℕ :=
    58 if h : ∃ p : Structure × Formula, EncodesMC x p.1 p.2 then (Classical.choose h).2.size else 0
    59
    60/-- **`p-MC(Φ)`**, parameterized model checking for the class `Φ` of formulas. -/
    61noncomputable def pMC (Φ : Set Formula) : Problem where
    62 Domain := {x | ∃ A φ, EncodesMC x A φ ∧ φ ∈ Φ ∧ φ.NoSetVar}
    63 Yes x := ∃ A φ, EncodesMC x A φ ∧ Models A φ
    64 param := mcParam
    65
    66/-- The word `x` is the word of the structure `A` followed by the number `k`. -/
    67def EncodesWD (x : List ℕ) (A : Structure) (k : ℕ) : Prop :=
    68 ∃ y, Encodes y A ∧ x = y ++ [k]
    69
    70/-- A **witness** of weight `k` for `φ(X)` in `A`, with `X` of arity `s`: a set of `k` tuples of
    71length `s` over the universe that, taken as the value of `X`, makes `φ` true. -/
    72def Witness (A : Structure) (φ : Formula) (s k : ℕ) : Prop :=
    73 φ.Fits A.arities s ∧ ∃ S : Finset (List ℕ), S.card = k ∧
    74 (∀ t ∈ S, t.length = s ∧ ∀ a ∈ t, a < A.size) ∧ Sat A ↑S φ fun _ => 0
    75
    76/-- **`p-WD_φ`**, weighted Fagin definability of `φ(X)` with `X` of arity `s`. -/
    77def pWD (φ : Formula) (s : ℕ) : Problem where
    78 Domain := {x | ∃ A k, EncodesWD x A k}
    79 Yes x := ∃ A k, EncodesWD x A k ∧ Witness A φ s k
    80 param x := x.getLast?.getD 0
    81
    82end Lax496464.WH_B3_LogicProblems
    83
    Formalization Notes

    Words. An instance of model checking is the word of the structure followed by the word of the formula; an instance of weighted definability is the word of the structure followed by kk. Both parts are self-delimiting, so a word determines them. The parameter is the size of the formula, or the last entry.

    Model checking. The formula does not use the relation variable, and it is false in a structure whose vocabulary it does not fit. Its free variables range over the universe. The class Φ\Phi restricts the instances only: the yes-instances of p-MC(Φ)p\text{-MC}(\Phi) are those of p-MC(Φ′)p\text{-MC}(\Phi') for every Φ′⊇Φ\Phi' \supseteq \Phi that lie in the smaller domain.

    Weighted definability. The formula of p-WDφp\text{-WD}_\varphi is fixed, so each formula and arity give one problem. The formulas defining the hierarchies are sentences, evaluated under an arbitrary assignment (here the one sending every variable to 00). A relation of kk tuples is a finite set of lists of length ss over the universe. A formula that does not fit the vocabulary has no witness.

    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…