Embedded dependency

In relational database theory, an embedded dependency (ED) is a certain kind of constraint on a relational database. It is the most general type of constraint used in practice, including both tuple-generating dependencies (TGDs) and equality-generating dependencies (EGDs). EDs can express functional dependencies, join dependencies, multi-valued dependencies, inclusion dependencies, foreign key dependencies, and many more besides. An ED is a sentence in first-order logic of the form:

∀x1 ... xn, P(x1, ..., xn) → ∃z1, ..., zk, Q(y1, ..., ym)

where {z1, ..., zk} = {y1, ..., ym} \ {x1, ..., xn}, and P is a possibly empty and Q is a non-empty conjunction of relational and equality atoms. A relational atom has the form R(w1, ..., wh) and an equality atom has the form wi = wj where each of the w, ..., wh, wi, wj, are variables or constants. When all atoms in Q are equalities, the ED is an EGD, and when all atoms in Q are relational, the ED is a TGD. Every ED is equivalent to an EGD and a TGD. A TGD is said to be full when the existential quantifier is empty. An algorithm known as the chase takes as input an instance that may or may not satisfy a set of EDs, and, if it terminates (which is a priori undecidable), output an instance that does satisfy the EDs.