Worked example: Boolean conjunctive queries – evaluation and containment #

This file is a tutorial: it walks, step by step, through the addition of a new problem domain to the library, with NP-completeness proofs at the end. It is meant to be read top to bottom, and to serve as a template for formalizing further problems. The domain is database theory: Boolean conjunctive queries (BCQs) over relational databases with set semantics, and the two classical decision problems about them, both NP-complete by the results of Chandra and Merlin (1977):

evaluation (combined complexity): given a query q and a database D, does q hold in D?
containment: given queries q₁ and q₂, is every database satisfying q₁ also a model of q₂?

To keep the tutorial focused we fix the schema to a single binary relation E – graph databases. This loses no complexity-theoretic generality (both problems are already NP-hard for this schema) and everything below extends mechanically to any fixed relational schema. A BCQ is then an expression ∃ x₁ … xₖ, E(t₁, t₁') ∧ … ∧ E(tₘ, tₘ') where each term tᵢ is a variable or a constant.

The recipe, common to every problem in the library:

Vocabulary: a relational FirstOrder.Language whose finite structures are the problem instances.
Semantics: a Prop-valued predicate on structures of that vocabulary, total on all structures (also the meaningless “junk” ones), with the convention for junk made explicit.
Invariance: the predicate is isomorphism-invariant, giving a bundled DecisionProblem.
Membership: the problem is in NP, either by exhibiting a Σ₁ second-order definition (SigmaSODefinable) or by an FO reduction to a problem already in NP.
Hardness: an FO reduction from an NP-hard problem of the catalog.
Completeness: combine 4 and 5.

This tutorial wraps that recipe in the full user-facing arc, which is how the steps below are numbered: start from the concrete problem in the user's own formalism (step 1), construct the encoding with the machinery of DescriptiveComplexity.Encoding – size bounds discharged at construction (step 3) – prove the encoded problem equivalent to the concrete one (step 6), and only then establish the NP-completeness of the encoded variant, which faithfulness reads back to the concrete data. The two encoding obligations – semantic equivalence and size-faithfulness – are both machine-checked, and they are arguably the steps a library user should worry about most.

Evaluation goes through this arc directly (steps 1–9); containment reuses evaluation on both sides – its membership is an FO reduction to evaluation and its hardness an FO reduction from evaluation – with the classical Chandra–Merlin homomorphism theorem (DescriptiveComplexity.queryContained_iff_hom) as the bridge. The reductions are all order-free and quantifier-free.

Main results:

DescriptiveComplexity.CQEval, DescriptiveComplexity.CQContainment: the two bundled decision problems;
DescriptiveComplexity.queryContained_iff_hom: the Chandra–Merlin theorem – containment holds iff there is a homomorphism from the right query to the canonical database of the left one;
DescriptiveComplexity.concreteQueryHolds_iff_queryHolds: semantic faithfulness of the encoding – on instances built (by DescriptiveComplexity.queryDbStructure) from a concrete query (a list of atoms) and a concrete database (a list of facts), the abstract semantics agrees with the textbook one;
DescriptiveComplexity.cqEncoding with DescriptiveComplexity.cqEncoding_faithful: the bundled encoding – size bounds discharged by construction, semantics faithful – and DescriptiveComplexity.cqDecoding, the computable decoding back, with DescriptiveComplexity.cqEvalWF_NP_complete, completeness on well-formed instances;
DescriptiveComplexity.threeCol_fo_reduction_cqEval : ThreeCol ≤ᶠᵒ CQEval;
DescriptiveComplexity.cqContainment_fo_reduction_cqEval : CQContainment ≤ᶠᵒ CQEval;
DescriptiveComplexity.cqEval_fo_reduction_cqContainment : CQEval ≤ᶠᵒ CQContainment;
DescriptiveComplexity.cqEval_NP_complete and DescriptiveComplexity.cqContainment_NP_complete.

Step 1: the concrete problem, in the user's own formalism #

A user of the library does not start from finite structures: they start from concrete data. Here a Boolean conjunctive query over variables V and constants C is a list of atoms – each argument in V ⊕ C – and a graph database is a list of facts over the constants, with the textbook semantics ConcreteQueryHolds (some assignment of the variables to constants sends every atom to a fact). Nothing in this step mentions model theory; it is the problem as a database theorist states it, and it is what the final completeness theorem will be about, through the faithfulness theorem of step 6.

Encoding this data into finite structures carries two obligations – the encoding must preserve the meaning (semantic equivalence, step 6) and the size (no padding, no compression, step 3) – and the machinery of DescriptiveComplexity.Encoding makes both machine-checked. Stating the size obligation needs the whole family of instances to be a single type, so the data is also packaged as a record CQInstance of its dimensions and contents. Two choices in the packaging are dictated by the machinery itself, and both are the kind of judgement call the size bounds exist to catch:

Finite sets, not lists. With List-valued atoms an instance could repeat one atom arbitrarily often: its declared size grows without bound while the encoded universe stays put, and the no-compression bound le_card of step 3 would be simply false. Under set semantics the honest concrete object is a finite set of atoms anyway.
The size counts n and m, not just the sets. The universe is the variables and constants: with 2 ^ k variables and a one-atom query, a size that only counted the sets would hide an exponential universe, and the no-padding bound card_le would be false.

The packaged type also carries m + 1 constants, so the nonempty-database junk convention of the equivalence theorem (step 6) holds by construction.

Worked example: Boolean conjunctive queries – evaluation and containment #

Step 1: the concrete problem, in the user's own formalism #

Step 2: the vocabulary of evaluation instances #

Step 3: the encoding, size bounds discharged at construction #

Step 4: semantics #

Step 5: isomorphism-invariance and the bundled problem #

Step 6: faithfulness – the encoded problem is the concrete one #

Step 7: membership in NP #

Step 8: NP-hardness, by reduction from 3-colorability #

Step 9: completeness of evaluation #

Step 10: containment – vocabulary, semantics, and the Chandra–Merlin theorem #

Step 11: containment is in NP, by reduction to evaluation #

Step 12: containment is NP-hard, by reduction from evaluation #

Where to go from here #