Editing Tuple relational calculus (section)

=== Safe queries ===

In order to limit the query expressions such that they express only domain-independent queries a syntactical notion of ''safe query'' is usually introduced. To determine whether a query expression is safe we will derive two types of information from a query. The first is whether a variable-column pair ''t''.''a'' is ''bound'' to the column of a relation or a constant, and the second is whether two variable-column pairs are directly or indirectly equated (denoted ''t''.''v'' == ''s''.''w'').

For deriving boundedness we introduce the following reasoning rules:

# in " ''v''.''a'' = ''w''.''b'' " no variable-column pair is bound,
# in " ''v''.''a'' = ''k'' " the variable-column pair ''v''.''a'' is bound,
# in " ''r''(''v'') " all pairs ''v''.''a'' are bound for ''a'' in ''type''(''v''),
# in " ''f''<sub>1</sub> ∧ ''f''<sub>2</sub> " all pairs are bound that are bound either in ''f''<sub>1</sub> or in ''f''<sub>2</sub>,
# in " ''f''<sub>1</sub> ∨ ''f''<sub>2</sub> " all pairs are bound that are bound both in ''f''<sub>1</sub> and in ''f''<sub>2</sub>,
# in " ¬ ''f'' " no pairs are bound,
# in " ∃ ''v'' : ''H'' ( ''f'' ) " a pair ''w''.''a'' is bound if it is bound in ''f'' and ''w'' <> ''v'', and
# in " ∀ ''v'' : ''H'' ( ''f'' ) " a pair ''w''.''a'' is bound if it is bound in ''f'' and ''w'' <> ''v''.

For deriving equatedness we introduce the following reasoning rules (next to the usual reasoning rules for equivalence relations: reflexivity, symmetry and transitivity):

# in " ''v''.''a'' = ''w''.''b'' " it holds that ''v''.''a'' == ''w''.''b'',
# in " ''v''.''a'' = ''k'' " no pairs are equated,
# in " ''r''(''v'') " no pairs are equated,
# in " ''f''<sub>1</sub> ∧ ''f''<sub>2</sub> " it holds that ''v''.''a'' == ''w''.''b'' if it holds either in ''f''<sub>1</sub> or in ''f''<sub>2</sub>,
# in " ''f''<sub>1</sub> ∨ ''f''<sub>2</sub> " it holds that ''v''.''a'' == ''w''.''b'' if it holds both in ''f''<sub>1</sub> and in ''f''<sub>2</sub>,
# in " ¬ ''f'' " no pairs are equated,
# in " ∃ ''v'' : ''H'' ( ''f'' ) " it holds that ''w''.''a'' == ''x''.''b'' if it holds in ''f'' and ''w''<>''v'' and ''x''<>''v'', and
# in " ∀ ''v'' : ''H'' ( ''f'' ) " it holds that ''w''.''a'' == ''x''.''b'' if it holds in ''f'' and ''w''<>''v'' and ''x''<>''v''.

We then say that a query expression { v : H | f(v) } is ''safe'' if
* for every column name ''a'' in ''H'' we can derive that ''v''.''a'' is equated with a bound pair in ''f'',
* for every subexpression of ''f'' of the form " ∀ ''w'' : ''G'' ( ''g'' ) " we can derive that for every column name ''a'' in ''G'' we can derive that ''w''.''a'' is equated with a bound pair in ''g'', and
* for every subexpression of ''f'' of the form " ∃ ''w'' : ''G'' ( ''g'' ) " we can derive that for every column name ''a'' in ''G'' we can derive that ''w''.''a'' is equated with a bound pair in ''g''.

The restriction to safe query expressions does not limit the expressiveness since all domain-independent queries that could be expressed can also be expressed by a safe query expression. This can be proven by showing that for a schema ''S'' = (''D'', ''R'', ''h''), a given set ''K'' of constants in the query expression, a tuple variable ''v'' and a header ''H'' we can construct a safe formula for every pair ''v''.''a'' with ''a'' in ''H'' that states that its value is in the active domain. For example, assume that ''K''={1,2}, ''R''={"r"} and ''h'' = { ("r", {"a, "b"}) } then the corresponding safe formula for ''v''.b is:
: ''v''.b = 1 ∨ ''v''.b = 2 ∨ ∃ ''w'' ( r(w) ∧ ( ''v''.b = ''w''.a ∨ ''v''.b = ''w''.b ) )
This formula, then, can be used to rewrite any unsafe query expression to an equivalent safe query expression by adding such a formula for every variable ''v'' and column name ''a'' in its type where it is used in the expression. Effectively this means that we let all variables range over the active domain, which, as was already explained, does not change the semantics if the expressed query is domain independent.