Tuple calculus
The tuple calculus is a calculus that was introduced by Edgar F. Codd as part of the relational model in order to give a declarative database query language for this data model. It formed the inspiration for the database query languages QUEL and SQL of which the latter, although far less faithful to the original relational model and calculus, is now used in almost all relational database management systems as the ad-hoc query language. Along with the tuple calculus Codd also introduced the domain calculus which is closer to first-order logic and showed that these two calculi (and the relational algebra) are equivalent in expressive power.Definition of the Calculus
The fundamental assumption in this calculus is that variables range over tuples as they are defined in the relational model. (In what follows the term tuple is always used in that meaning) The atoms of our language are going to be statements about such variables and defined by the following context-free grammar:
- B ::= (T.A = T.A) | (T.A = C) | R(T)
- (t.name = "Codd") -- tuple t has a name attribute and its value is "Codd"
- (t.age = s.age) -- t has an age attribute and s has an age attrbute with the same value
- Book(t) -- tuple t is present in relation Book.
- F ::= B | ( F ∧ F ) | ( F ∨ F ) | ¬ F | ∃ T ( F ) | ∀ T ( F )
- t.name = "C. J. Date" ∨ t.name = "H. Darwen"
- Book(t) ∨ Magazine(t)
- ∀ t ( ¬ ( Book(t) ∧ t.author = "C. J. Date" ∧ ¬ ( t.subject = "relational model")))
We will assume that the quantifiers quantify over the universe of all tuples. It is easy to see that then a closed formula, i.e., a formula with no free variables, is either true or false for a certain database instance. This means that we can already use those to ask boolean queries, i.e., queries that result in either "yes" or "no". If it is not closed then given a database instance a formula defines a set of bindings, i.e., a function b of the free variables to tuples, such that the formula becomes true iff every free variable x in it is replaced with b(x).
A query language should not only make statements about the contents of the database but it should also be able to construct new tuples that are not yet in the database. For this purpose the tuple constructor is introduced that can construct a tuple given a certain variable binding. Its syntax is defined as follows:
- K::= ( A:T.A, ..., A:T.A )
- ( ) -- constructs the empty tuple
- (employee:t.name, manager:s.name) -- constructs a tuple with attributes names "employee" and "manager" and gives them resepectively the values of the "name" of t and the "name" of s.
- it must bind all the variables in the constructor, and
- if t.a appears in the konstructor then t should be bound to a tuple with an a attribute.
- Q ::= { K | F }
- { (name:t.name) | Employee(t) ∧ t.wage = 50.000 }
- { (supplier:s.name, article:p.name) | Supplier(s) ∧ Project(p) ∧ ∃ a ( Supplies(a) ∧ s.s# = a.s# ∧ a.p# = p.p# ) }
We define P(f) and N(f) as functions that map a formula f to a set of pairs (t, a) with t a tuple variable and a an attribute name. The intended meaning of these functions is that P(f) contains a pair (t, a) if in all bindings that make f true the variable t is bound to a tuple with an attribute a, and for N(f) this holds if this is the case for all bindings that make f false. The value of these functions can be inductively defined (and therefore computed) as follows:
| P( t.a = s.b ) = { (t, a), (s, b) } | N( t.a = s.b ) = ∅ |
| P( t.a = c ) = { (t, a) } | N( t.a = c ) = ∅ |
| P( r(t) ) = { (t, a) : a is in the header r } | \N( r(t) ) = ∅ |
| P( f ∧ g ) = P(f) ∪ P(g) | N( f ∧ g ) = N(f) ∩ N(g) |
| P( f ∨ g ) = P(f) ∩ P(g) | N( f ∨ g ) = N(f) ∪ N(g) |
| P( ¬ f ) = N(f) | N( ¬ f ) = P(f) |
| P( ∀ t ( f ) ) = { (s, a) ∈ P(f) : s ≠ t } | N( ∀ t ( f ) ) = { (s, a) ∈ N(f) : s ≠ t } |
| P( ∃ t ( f ) ) = { (s, a) ∈ P(f) : s ≠ t } | N( ∃ t ( f ) ) = { (s, a) ∈ N(f) : s ≠ t } |
We then call a query expression { k | f } well formed if for every occurrence of t.a in k it holds that (t, a) is in P(f). It will be clear that the result of every well formed query expression is well defined.
- Discuss safeness to prevent that the result may be infinite. Actually we should also check if the comparisos are legal according to the schema, but this is not strictly necessary.


