Pairs of conjunctive queries and containment
Lax420092.QueryPairs · concepts/Lax420092/QueryPairs.lean · lax-420092
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition
An instance of containment is a pair of Boolean conjunctive queries over a shared universe: unary relations mark the variables of the left and of the right query, binary relations record their atoms, and the other elements are shared constants. The left query is contained in the right one when every database, over any universe and any denotation of the constants, that satisfies the left query satisfies the right one. CQContainment is the decision problem of the structures isomorphic to a pair whose left query is contained in the right one.
Concept map
Lean source view on GitHub
| 1 | import Mathlib.Tactic.FinCases |
| 2 | import Mathlib.ModelTheory.Order |
| 3 | import Mathlib.ModelTheory.Semantics |
| 4 | import Mathlib.ModelTheory.Complexity |
| 5 | import Mathlib.Data.Set.Finite.Lemmas |
| 6 | import Mathlib.Order.PiLex |
| 7 | import Mathlib.Data.Prod.Lex |
| 8 | import Mathlib.Data.Fintype.EquivFin |
| 9 | import Mathlib.Logic.Equiv.Fin.Basic |
| 10 | import Mathlib.Data.Finite.Sigma |
| 11 | import Mathlib.Data.Fintype.Lattice |
| 12 | import Mathlib.ModelTheory.Syntax |
| 13 | import Mathlib.ModelTheory.Graph |
| 14 | import Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex |
| 15 | import Mathlib.SetTheory.Cardinal.Finite |
| 16 | import Lax904597.Classes |
| 17 | import Lax799700.Problems |
| 18 | import Lax420092.Evaluation |
| 19 | |
| 20 | /-! |
| 21 | --- |
| 22 | title: Pairs of conjunctive queries and containment |
| 23 | type: definition |
| 24 | --- |
| 25 | An instance of containment is a pair of Boolean conjunctive queries over a |
| 26 | shared universe: unary relations mark the variables of the left and of the |
| 27 | right query, binary relations record their atoms, and the other elements |
| 28 | are shared constants. The left query is contained in the right one when |
| 29 | every database, over any universe and any denotation of the constants, that |
| 30 | satisfies the left query satisfies the right one. CQContainment is the |
| 31 | decision problem of the structures isomorphic to a pair whose left query is |
| 32 | contained in the right one. |
| 33 | -/ |
| 34 | |
| 35 | namespace Lax420092.QueryPairs |
| 36 | |
| 37 | open Lax420092.Evaluation |
| 38 | |
| 39 | open FirstOrder |
| 40 | |
| 41 | open FirstOrder.Language |
| 42 | |
| 43 | /-- The relation symbols of the language. -/ |
| 44 | inductive queryPairRel : ℕ → Type where |
| 45 | /-- `leftVar x`: the element `x` is a variable of the left query. -/ |
| 46 | | leftVar : queryPairRel 1 |
| 47 | /-- `rightVar x`: the element `x` is a variable of the right query. -/ |
| 48 | | rightVar : queryPairRel 1 |
| 49 | /-- `leftAtom x y`: the left query contains the atom `E(x, y)`. -/ |
| 50 | | leftAtom : queryPairRel 2 |
| 51 | /-- `rightAtom x y`: the right query contains the atom `E(x, y)`. -/ |
| 52 | | rightAtom : queryPairRel 2 |
| 53 | deriving DecidableEq |
| 54 | |
| 55 | /-- The relational language of pairs of conjunctive queries over a shared |
| 56 | universe of variables and constants. -/ |
| 57 | def queryPair : FirstOrder.Language := |
| 58 | ⟨fun _ => Empty, queryPairRel⟩ |
| 59 | |
| 60 | instance instIsRelationalQueryPair : FirstOrder.Language.IsRelational queryPair := fun _ => |
| 61 | (inferInstance : IsEmpty Empty) |
| 62 | |
| 63 | /-- `leftVar x`: the element `x` is a variable of the left query. -/ |
| 64 | abbrev qpLeftVar : queryPair.Relations 1 := |
| 65 | .leftVar |
| 66 | |
| 67 | /-- `rightVar x`: the element `x` is a variable of the right query. -/ |
| 68 | abbrev qpRightVar : queryPair.Relations 1 := |
| 69 | .rightVar |
| 70 | |
| 71 | /-- `leftAtom x y`: the left query contains the atom `E(x, y)`. -/ |
| 72 | abbrev qpLeftAtom : queryPair.Relations 2 := |
| 73 | .leftAtom |
| 74 | |
| 75 | /-- `rightAtom x y`: the right query contains the atom `E(x, y)`. -/ |
| 76 | abbrev qpRightAtom : queryPair.Relations 2 := |
| 77 | .rightAtom |
| 78 | |
| 79 | open FirstOrder |
| 80 | |
| 81 | open Language Structure BoundedFormula |
| 82 | |
| 83 | section PairShorthands |
| 84 | |
| 85 | variable {A : Type} [queryPair.Structure A] |
| 86 | |
| 87 | /-- `x` is a variable of the left query. -/ |
| 88 | def LVar (x : A) : Prop := RelMap qpLeftVar ![x] |
| 89 | |
| 90 | /-- `x` is a variable of the right query. -/ |
| 91 | def RVar (x : A) : Prop := RelMap qpRightVar ![x] |
| 92 | |
| 93 | /-- `E(x, y)` is an atom of the left query. -/ |
| 94 | def LAtom (x y : A) : Prop := RelMap qpLeftAtom ![x, y] |
| 95 | |
| 96 | /-- `E(x, y)` is an atom of the right query. -/ |
| 97 | def RAtom (x y : A) : Prop := RelMap qpRightAtom ![x, y] |
| 98 | |
| 99 | /-- `x` is a variable of either query; the non-`PairVar` elements are the |
| 100 | shared constants, whose denotation every database fixes. -/ |
| 101 | def PairVar (x : A) : Prop := LVar x ∨ RVar x |
| 102 | |
| 103 | end PairShorthands |
| 104 | |
| 105 | /-- The left query is contained in the right one: every database (over any |
| 106 | universe, with any interpretation of the constants) satisfying the left query |
| 107 | satisfies the right query. -/ |
| 108 | def QueryContained (A : Type) [queryPair.Structure A] : Prop := |
| 109 | ∀ (U : Type) (F : U → U → Prop) (ι : A → U), |
| 110 | SatisfiedIn (PairVar (A := A)) (LAtom (A := A)) F ι → |
| 111 | SatisfiedIn (PairVar (A := A)) (RAtom (A := A)) F ι |
| 112 | |
| 113 | open Lax904597.Problems Lax799700.Problems |
| 114 | |
| 115 | /-- BCQ containment: is the left query contained in the right one? -/ |
| 116 | def CQContainment : DecisionProblem queryPair := |
| 117 | DecisionProblem.ofPred QueryContained |
| 118 | |
| 119 | end Lax420092.QueryPairs |
| 120 |
Used by
From Mathlib
Mathlib.Combinatorics.SimpleGraph.Coloring.VertexMathlib.Data.Finite.SigmaMathlib.Data.Fintype.EquivFinMathlib.Data.Fintype.LatticeMathlib.Data.Prod.LexMathlib.Data.Set.Finite.LemmasMathlib.Logic.Equiv.Fin.BasicMathlib.ModelTheory.ComplexityMathlib.ModelTheory.GraphMathlib.ModelTheory.OrderMathlib.ModelTheory.SemanticsMathlib.ModelTheory.SyntaxMathlib.Order.PiLexMathlib.SetTheory.Cardinal.FiniteMathlib.Tactic.FinCases
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments