Conjunctive queries and graph databases as structures
Lax420092.QueryDatabases · concepts/Lax420092/QueryDatabases.lean · lax-420092
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition
An instance of Boolean conjunctive query evaluation is a finite structure over a vocabulary with a unary relation marking the query's variables and two binary relations: the atoms of the query, over variables and constants, and the facts of the database, over constants. The schema is a single binary relation, that of graph databases; a database edge is a fact both of whose endpoints are constants, facts touching a variable being junk the semantics ignores.
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 | |
| 17 | /-! |
| 18 | --- |
| 19 | title: Conjunctive queries and graph databases as structures |
| 20 | type: definition |
| 21 | --- |
| 22 | An instance of Boolean conjunctive query evaluation is a finite structure |
| 23 | over a vocabulary with a unary relation marking the query's variables and |
| 24 | two binary relations: the atoms of the query, over variables and constants, |
| 25 | and the facts of the database, over constants. The schema is a single |
| 26 | binary relation, that of graph databases; a database edge is a fact both of |
| 27 | whose endpoints are constants, facts touching a variable being junk the |
| 28 | semantics ignores. |
| 29 | -/ |
| 30 | |
| 31 | namespace Lax420092.QueryDatabases |
| 32 | |
| 33 | open FirstOrder |
| 34 | |
| 35 | open FirstOrder.Language |
| 36 | |
| 37 | /-- The relation symbols of the language. -/ |
| 38 | inductive queryDbRel : ℕ → Type where |
| 39 | /-- `isVar x`: the element `x` is a variable of the query. -/ |
| 40 | | isVar : queryDbRel 1 |
| 41 | /-- `atom x y`: the query contains the atom `E(x, y)` (its arguments are |
| 42 | variables or constants). -/ |
| 43 | | atom : queryDbRel 2 |
| 44 | /-- `fact a b`: the database contains the fact `E(a, b)`. -/ |
| 45 | | fact : queryDbRel 2 |
| 46 | deriving DecidableEq |
| 47 | |
| 48 | /-- The relational language of BCQ evaluation instances: a query and a |
| 49 | database over a shared universe, with a unary predicate singling out the |
| 50 | query variables and binary predicates for query atoms and database facts. -/ |
| 51 | def queryDb : FirstOrder.Language := |
| 52 | ⟨fun _ => Empty, queryDbRel⟩ |
| 53 | |
| 54 | instance instIsRelationalQueryDb : FirstOrder.Language.IsRelational queryDb := fun _ => |
| 55 | (inferInstance : IsEmpty Empty) |
| 56 | |
| 57 | /-- `isVar x`: the element `x` is a variable of the query. -/ |
| 58 | abbrev qdbIsVar : queryDb.Relations 1 := |
| 59 | .isVar |
| 60 | |
| 61 | /-- `atom x y`: the query contains the atom `E(x, y)` (its arguments are |
| 62 | variables or constants). -/ |
| 63 | abbrev qdbAtom : queryDb.Relations 2 := |
| 64 | .atom |
| 65 | |
| 66 | /-- `fact a b`: the database contains the fact `E(a, b)`. -/ |
| 67 | abbrev qdbFact : queryDb.Relations 2 := |
| 68 | .fact |
| 69 | |
| 70 | open FirstOrder |
| 71 | |
| 72 | open Language Structure BoundedFormula |
| 73 | |
| 74 | section EvalShorthands |
| 75 | |
| 76 | variable {A : Type} [queryDb.Structure A] |
| 77 | |
| 78 | /-- `x` is a variable of the query. -/ |
| 79 | def QVar (x : A) : Prop := RelMap qdbIsVar ![x] |
| 80 | |
| 81 | /-- `E(x, y)` is an atom of the query. -/ |
| 82 | def QAtom (x y : A) : Prop := RelMap qdbAtom ![x, y] |
| 83 | |
| 84 | /-- `E(a, b)` is a fact of the database (raw: no constraint on `a`, `b`). -/ |
| 85 | def DbFact (x y : A) : Prop := RelMap qdbFact ![x, y] |
| 86 | |
| 87 | /-- A genuine database edge: a fact both of whose endpoints are database |
| 88 | elements (i.e., not query variables). Facts violating this are representation |
| 89 | junk and are ignored by the semantics. -/ |
| 90 | def DbEdge (x y : A) : Prop := DbFact x y ∧ ¬QVar x ∧ ¬QVar y |
| 91 | |
| 92 | end EvalShorthands |
| 93 | |
| 94 | end Lax420092.QueryDatabases |
| 95 |
Builds on
none
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