Conjunctive query

Conjectura.Defs.ComputerScience.Databases.ConjunctiveQuery

/-
Copyright (c) 2026 The Conjectura Authors. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: The Conjectura Authors
-/
import Conjectura.Defs.ComputerScience.Databases.RelationInstance

/-! # Conjunctive query -/

namespace Conjectura.Databases

/-- A **conjunctive query** is the select–project–join fragment: a set of atoms that
must all be matched by one assignment of variables to values. Query containment and
evaluation for this fragment are the two problems most of database theory is about,
and both are NP-complete. -/
abbrev ConjunctiveQuery (Var Attr Val : Type*) :=
  Set (RelationInstance Attr Val × (Attr → Var))

end Conjectura.Databases