Boolean conjunctive query evaluation
Lax420092.Evaluation · concepts/Lax420092/Evaluation.lean · lax-420092
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition
A conjunctive query with given variables and atoms over the elements of an instance is satisfied in a database, a binary relation on some universe with a denotation of the instance's elements, when some valuation of the elements into the universe agrees with the denotation on the non-variables and sends every atom to an edge of the database. The homomorphism form takes the instance's own universe as database, every non-variable denoting itself. The query of an evaluation instance holds in its database when the homomorphism condition is met with the database edges as facts, the classical semantics of Boolean conjunctive queries under set semantics. CQEval is the decision problem of the structures isomorphic to an instance whose query holds.
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 Lax420092.QueryDatabases |
| 17 | import Lax904597.Classes |
| 18 | import Lax799700.Problems |
| 19 | |
| 20 | /-! |
| 21 | --- |
| 22 | title: Boolean conjunctive query evaluation |
| 23 | type: definition |
| 24 | --- |
| 25 | A conjunctive query with given variables and atoms over the elements of an |
| 26 | instance is satisfied in a database, a binary relation on some universe |
| 27 | with a denotation of the instance's elements, when some valuation of the |
| 28 | elements into the universe agrees with the denotation on the non-variables |
| 29 | and sends every atom to an edge of the database. The homomorphism form |
| 30 | takes the instance's own universe as database, every non-variable denoting |
| 31 | itself. The query of an evaluation instance holds in its database when the |
| 32 | homomorphism condition is met with the database edges as facts, the |
| 33 | classical semantics of Boolean conjunctive queries under set semantics. |
| 34 | CQEval is the decision problem of the structures isomorphic to an instance |
| 35 | whose query holds. |
| 36 | -/ |
| 37 | |
| 38 | namespace Lax420092.Evaluation |
| 39 | |
| 40 | open Lax420092.QueryDatabases |
| 41 | |
| 42 | open FirstOrder |
| 43 | |
| 44 | open Language Structure BoundedFormula |
| 45 | |
| 46 | section GenericCore |
| 47 | |
| 48 | variable {A B : Type} |
| 49 | |
| 50 | /-- The conjunctive query with variables `VarP` and atoms `AtomP` (over |
| 51 | instance elements `A`) is satisfied in the database `F` on universe `U`, |
| 52 | where `ι` fixes the denotation of the non-variables: some valuation extends |
| 53 | `ι` and maps every atom to a database edge. -/ |
| 54 | def SatisfiedIn (VarP : A → Prop) (AtomP : A → A → Prop) {U : Type} |
| 55 | (F : U → U → Prop) (ι : A → U) : Prop := |
| 56 | ∃ v : A → U, (∀ x, ¬VarP x → v x = ι x) ∧ ∀ x y, AtomP x y → F (v x) (v y) |
| 57 | |
| 58 | /-- The homomorphism condition: satisfaction in a database carried by the |
| 59 | instance's own universe, with every non-variable denoting itself. This single |
| 60 | notion underlies both problems below. -/ |
| 61 | def CQHom (VarP : A → Prop) (AtomP FactP : A → A → Prop) : Prop := |
| 62 | SatisfiedIn VarP AtomP FactP id |
| 63 | |
| 64 | end GenericCore |
| 65 | |
| 66 | /-- The query of an evaluation instance holds in its database: there is a |
| 67 | valuation of the elements, fixing the non-variables, that maps every query |
| 68 | atom to a genuine database edge. This is the classical semantics of Boolean |
| 69 | conjunctive queries, phrased as a homomorphism into the database half of the |
| 70 | instance. -/ |
| 71 | def QueryHolds (A : Type) [queryDb.Structure A] : Prop := |
| 72 | CQHom (QVar (A := A)) (QAtom (A := A)) (DbEdge (A := A)) |
| 73 | |
| 74 | open Lax904597.Problems Lax799700.Problems |
| 75 | |
| 76 | /-- BCQ evaluation: does the query of the instance hold in its database? -/ |
| 77 | def CQEval : DecisionProblem queryDb := |
| 78 | DecisionProblem.ofPred QueryHolds |
| 79 | |
| 80 | end Lax420092.Evaluation |
| 81 |
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