On Verifying a Query Optimizer: A Correctness

Proof for a Real-World Query Rewrite Rule

by

Bryan Yongbing Feng

An essay in fulfilment of the

course requirement for the degree of

Master of Mathematics

in Computer Science

Waterloo, Ontario, Canada, 1994

\begin{matrix}c \\ ◯ \end{matrix}Bryan Yongbing Feng 1994

Abstract

It is generally accepted that rule-based query optimization is a more flexible approach to supporting high-level query languages. However, current practice involves very limited consideration of the issue of rule validity (or correctness). Consequently, the reliability of rule-based query optimization will tend to diminish as both the expressiveness of query languages and complexity of the underlying data models increase.

This has motivated members of the Advanced Database Systems Laboratory at our institution to develop a refinement calculus that enables a formal specification of rewrite rules used in current relational and object-oriented optimization technology. This essay reports on an experiment to apply this calculus to capture the intentions underlying a rule used in an optimizer for an experimental object-oriented database system, also developed in our laboratory, and then to attempt proving the validity of this rule. Perhaps most significantly, we learned from this experiment:

(1) that our original informal understanding of the intentions underlying the rule was incorrect, and

(2) that our first few attempts at a formal specification of this rule were not valid.

We believe that this constitutes clear evidence that the issue of rewrite rule validity for existing query optimization technology has now become crucial in achieving essential levels of reliability in database systems.

Acknowledgements

Thanks go to my supervisor Grant Weddell. Without his patience, support and guidance, the work would never have been done. His careful reading through all the proofs makes the work reliable.

Also, thanks go to my friend Martin van Bommel. His careful proofreading of the earlier drafts of this essay make the final version more readable.

Bryan Yongbing Feng

Contents

1 Introduction 1 2 Preliminary 2 3 Read/Write Sets for A Query 7 4 Two Important Axioms for the Nest Operator 13

4.1 Associativity for the Nest Operator . . . . . . . . . . . . . . . . . . . 13 4.2 Commutativity for the Nest Operator . . . . . . . . . . . . . . . . . . 15

5 Correctness of A Real-World Rewrite Rule 24 5.1 More Related Axioms . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 5.2 The Derivation of the Correctness . . . . . . . . . . . . . . . . . . . . 28

6 Conclusion 44

List of Tables

1 A Real-World Query Rewrite Rule (in its original form) . . . . . . . . 2 2 A Grammar for the Wide-Spectrum Algebra (modified version) …. 3 3 Inference Axioms for the Refinement Calculus . . . . . . . . . . . . . 6 4 Bound Set and Var Set for the Wide-Spectrum Algebra . . . . . . . . 8 5 A Real-World Query Rewrite Rule (in the refinement calculus) …. 29

1 Introduction

Query optimization continues to be one of the great challenges in post-relational database systems. Since an ad hoc query facility is still one of the mandatory features in next generation of database systems [ABD^{+}89], lots of research effort has been devoted to it, among which is work on query rewriting techniques using rulebased query optimization models [BG92, FG91, FG86, Fre87, GD87, GM93, PHH92]. However, unfortunately, two important issues adhering to the rule-based systems - rule formalization (logic) and rule control - are rarely considered in these works.

In the paper [CW93], two leading members of the Advanced Database Systems Laboratory at our institution presented the development of a wide-spectrum algebra and a refinement calculus that enable a formal specification of rewrite rules used in current relational and object-oriented optimization technology. In this essay, I am reporting an experiment to apply this calculus to capture the intentions underlying a rule (see Table 1) used in the optimizer for an experimental object-oriented database system, also developed in our laboratory, and then to prove the validity of this rule. The motivation for the work is as follows: complex semantic query rewrite rules, instead of simple syntax query rewrite rules, are playing the central role in rule-based query optimizers, and the correctness of semantic rewrite rules are not trivial.

In the following sections, I will briefly review the wide-spectrum algebra and the refinement calculus over it, introduce some basic concepts on the correctness of the query rewrite rules, prove some basic axioms for the refinement calculus, and finally derive the correctness of the real-world query rewrite rule.

Table 1: A Real-World Query Rewrite Rule (in its original form)

(SelectCondSpecialize

(Find > QInfo > Type > ∗ FEList1 (AndHeap > ∗ PList1) (Scan > V > ScanSpec) (AndHeap > ∗ PList2 > Pred

where (Free <q Pred ’(< V)) > ∗ PList3) > ∗ FEList2) (Find < QInfo < Type << FEList1 (AndHeap < Pred << PList1) (Scan < V < ScanSpec) (AndHeap << PList2 << PList3) << FEList2))

2 Preliminary

A query language is called wide-spectrum if it can be used uniformly to express both

user level queries as well as low-level evaluation strategies or physical access plans. A

wide-spectrum query language would uniformly express a query in any stage during

query optimization and evaluation, so it provides a logical basis for the query rewrite

rule formalization. In the paper [CW93], Dr. Weddell and Dr. Coburn defined such

a language (algebra), and further formally defined a refinement calculus over the

language. The following is a brief summary of the paper.

In the syntax aspect, the algebra and the calculus are defined in terms of an

indexed non-terminal grammer, a context-free grammer with indexed non-terminals

(refer to Table 2), which allows high-order logic behaviors. In the semantics aspect,

they are based on a simple graph-based data model, following a general trend [Bee89, 2 PRELIMINARY 3

Table 2: A Grammar for the Wide-Spectrum Algebra (modified version)

productions  description
R → “(” Clause R R* “)” Inference constraint.
| “(” Ref E E “)”  Refinement constraint.
| “(” Neq S S “)”  Syntactic inequality constraint.
| “(” Empty F “)”  Syntactic empty set constraint.
| ⋯
E → S  Object quantification.
| S “:=” Pd  Navigation.
| S “:=” S “{” S* “}” Index scan.
| S “:=” S “(” S* “)” Method call.
| S “:” S  Type checking predicate.
| S “=” S  Equality predicate.
| S “<” S  Ordering predicate.
| “(” Keep S* E “)”  Keep.
| “(” Filter S* E “)” Filter.
| “(” Not E “)”  Simple compliment.
| “(” Cross E* “)”  Cross product.
| “(” Perm E “)”  Permutation.
| “(” Nest E E “)”  Nested cross product.
| “(” Inter E* “)”  Interleave.
| “(” Cat E E “)”  Concatenation.
| “(” Sort O* E “)”  Sort.
| ⋯
F → “(” Bound E “)”  Bounded variable set.
| “(” Var E “)”  All variable set.
| “(” Union F F “)”  Set union operation.
| “(” Intersect F F “)” Set intersection.
| …
Pd → S | Pd “.” S  Path description.
O → S D  Sort condition.
D → asc | desc  Sort direction.
S → (a symbol in S)  A class, attribute, function or variable name.
X* → ϵ | X | X* X*  (where X is one of {R, S, E, O})

Day89, GPvG90], and a possible result semantics in terms of a list of tuples is proposed to the algebra, and further extended to the calculus.

Based on the possible results semantics, a set of possible results is defined for each of the operators in the algebra with respect to the underlying database and a complete tuple. For a query expression E, the interpretation is denoted as: [[E]]_{db}^{t}. For example, the interpretation for the Nest operator is defined as follows:

[[(Nest E_{1} E_{2})]]_{db}^{t} =^{def} ⋃_{l∈[[E_{1}]]_{db}^{t}} J (db, E_{2}, l)

where

J (db, E, l_{1}) =^{def} \{ \begin{matrix}\{()\}, if len(l_{1}) = 0, \\ \{app(l_{2}, l_{3})|l_{2} ∈ [[E]]_{db}^{hd(l_{1})} and l_{3} ∈ J (db, E, tl(l_{1}))\}, \\ otherwise \end{matrix}

For better expressing the query, we have modified the Cross operator by splitting it into two operators: one is still called Cross, and the other one is called Perm. Here we give semantics of the new Cross and Perm operators as follows: Cross Product “(Cross E_{1}, …, E_{n})” adds to its output the union of all the lists of tuples. Each tuple in a given list consists of each possible combination of a tuple from the ith argument list with tuples from the remaining argument lists.

[[(Cross E_{1}, …, E_{2})]]_{db}^{t} =^{def} \{ \begin{matrix}\{(t)\}, if n = 0, \\ ⋃_{i=1}^{n} [[(Nest E_{i} (Cross E_{1}, …, E_{i−1}, E_{i+1}, E_{n}))]]_{db}^{t}, \\ otherwise. \end{matrix}

Perm “(Perm E)” returns all permutation of lists of tuples from its arguments.

[[(Perm E)]]_{db}^{t} =^{def} {l′ ∈ perm(l)|l ∈ [[E]]_{db}^{t}}

Further, the semantics of the refinement calculus is defined through the model theory and the proof theory:

Model Theory A database db is a model for a ground rule R, written db ⊧ R, if and only if one of the three conditions holds.

1. If R is the syntactic constraint “(Neq S_{1} S_{2})”, then S_{1} and S_{2} are distinct symbols.

2. If R is the refinement constraint “(Ref E_{1} E_{2})”, then [[E_{2}]]_{db}^{t} ⊆ [[E_{1}]]_{db}^{t} for any complete tuple t over V_{db}.

3. If R is the inference constraint “(Clause R R_{1}, …, R_{n})”, then db ⊧ R if db ⊧ R_{i} for each 1 ≤ i ≤ n.

A database db is a model for a non-ground rule R, also written db ⊧ R, if and only if db ⊧ R′ for each ground rule R′ where R ⇒^{∗} R′ (substitution). R is a logical consequence of rules R_{1}, …, R_{n}, written {R_{1}, …, R_{n}} ⊧ R, if and only if, for any database db, db ⊧ R if db ⊧ R_{i} for each 1 ≤ i ≤ n. If {} ⊧ R, R is called an axiom in the calculus.

Proof Theory Let {R, R_{1}, …, R_{n}} denote an arbitrary collection of rules. There

is a derivation of R from {R_{1}, …, R_{n}}, written

{R_{1}, …, R_{n}} ⊢ R

if and only if R = R_{i} for some 1 ≤ i ≤ n, or can be derived from {R_{1}, …, R_{n}} using the inference axioms in Table 3.

Table 3: Inference Axioms for the Refinement Calculus

name  definition
(substitution)  \frac{R}{Rψ}
(modus ponens) \frac{R_{1}, …, R_{n}, (Clause R R_{1}, …, R_{n})}{R}
(known axiom) \frac{There exists a proof that \{\} ⊧ R}{R}

Although the semantics given by the proof theory is sound, but not complete, the calculus could be used in storage definition, generic optimization, database dependency, etc..

For better expressing the rewrite rule, we extend the calculus with an Empty Set Constraints, which is:

“(” Empty F “)”

where F denotes a set of symbols, and the semantics for the empty set constraint is straight-forward and simple: a database db is a model for an empty set constraint “(Empty F)” if and only if F is an empty set. The union and intersection of sets are defined as usual, and in the next section, I will discuss the two special symbol sets generated by (Bound E) and (Var E).

In general, the definition of the semantics of the refinement calculus provides two ways to prove whether or not a given rule is an axiom: One way is to use the model theory to prove an axiom by referring to the semantics of the wide-spectrum algebra, and the other way is to use the proof theory to derive an axiom from a set of known axioms. The first way is mandatory to prove the basic axioms, however is not the proper way to prove a complex axiom, since it seldom use existing axioms, and the proof principle is irregular, which results that the proof is out of control in both size and complexity. On the other hand, although the proof theory is not complete, the second way is more preferable if we could classify a set of basic axioms, because the proof process could be done in a mechanical manner. In this essay, I will use the first way to prove some basic axioms, and then show the second way by deriving the correctness of a real-world rewrite rule.

3 Read/Write Sets for A Query

In order to explore the proof process of the axioms in the refinement calculus, it is necessary to define some basic concepts for the wide-spectrum algebra, and to examine the related properties.

Given a ground query, we are interested in two kinds of symbol sets, as defined below.

definition 3.1 A set of variables {S_{1}, …, S_{n}} is called a write set for a ground query E if and only if for any database db and any complete tuple t over V_{db}, for each l ∈ [[E]]_{db}^{t}

nth(l, i)[α(t) − {S_{1}, …, S_{n}}] = t[α(t) − {S_{1}, …, S_{n}}],

for 1 ≤ i ≤ len(l).

□

Table 4: Bound Set and Var Set for the Wide-Spectrum Algebra

E  (Bound E)  (Var E)
S  {S}  {S}
S := P d  {S}  {S} ∪ head(P d)^{∗}
S := S′{S_{1}, …, S_{n}}  {S}  {S, S′, S_{1}, …, S_{n}}
S := S′(S_{1}, …, S_{n})  {S}  {S, S′, S_{1}, …, S_{n}}
P d : {S_{1}, …, S_{n}}  {}  {S_{1}, …, S_{n}} ∪ head(P d)
P d = P d′  {}  head(P d) ∪ head(P d′)
P d < P d′  {}  head(P d) ∪ head(P d′)
(Keep S_{1}, …, S_{n} E)  (Bound E) ∩ {S_{1}, …, S_{n}} (Var E) ∪ {S_{1}, …, S_{n}}
(Filter S_{1}, …, S_{n} E)  (Bound E)  (Var E) ∪ {S_{1}, …, S_{n}}
(Not E)  (Bound E)  (Var E)
(Cross E_{1}, …, E_{n})  ⋃_{1≤i≤n}(Bound E_{i})  ⋃_{1≤i≤n}(Var E_{i})
(Nest E_{1} E_{2})  (Bound E_{1}) ∪ (Bound E_{2}) (Var E_{1}) ∪ (Var E_{2})
(Inter E_{1}, …, E_{n}) ⋃_{1≤i≤n}(Bound E_{i}) ⋃_{1≤i≤n}(Var E_{i})
(Cat E_{1} E_{2})  (Bound E_{1}) ∪ (Bound E_{2}) (Var E_{1}) ∪ (Var E_{2})
(Sort S_{1} D_{1}, …, S_{n} D_{n} E) (Bound E)  (Var E) ∪ {S_{1}, …, S_{n}}

definition 3.2 A set of variables {S_{1}, …, S_{n}} is called a read set for a ground query E if and only if for any database db and any pair of complete tuples t_{1} and t_{2} over V_{db}, for which t_{1}[{S_{1}, …, S_{n}}] = t_{2}[{S_{1}, …, S_{n}}], the following statement holds:

{l_{1}[{S_{1}, …, S_{n}}]|l_{1} ∈ [[E]]_{db}^{t_{1}}} = {l_{2}[{S_{1}, …, S_{n}}]|l_{2} ∈ [[E]]_{db}^{t_{2}}}.
□

∗Only the first symbol in the path sequence is bounded to a vertex. Here head(P d) denotes the singleton set of the first symbol in P d.

Also, for a given ground query, there are two syntax symbol sets associated with it, which are the Bound set and the Var set, respectively.

definition 3.3 Given a ground query E, (Bound E) and (Var E) are defined recursively in Table 4, respectively.

□

The following theorem shows that the two special sets fall into the two interesting catalogs, respectively.

Theorem 3.1 For any ground query E, (Bound E) is a write set, and (Var E) is both a write set and a read set.

Proof:

First, we prove that (Bound E) and (Var E) are a write set and a read set, respectively, by the induction on the depth of the query (tree).

basis. The depth of the query tree is 1, and from the definition table, it is easy to see there are seven kinds of queries falling into this category. Due to the space limit, we only take one kind of query as an example to prove. The others can be proved similarly.

Suppose that the query is S := P d, then according to the definition, for any database db and any complete tuple t over V_{db},

[[S := P d]]_{db}^{t} = perm(F(S, list({v ∈ V_{db}|(db, t, P d) ⇝ v})) ≺ t).

So, for each l ∈ [[S := P d]]_{db}^{t}, by definition of F and ≺,

nth(l, i)[α(t) − {S}] = t[α(t) − {S}],

for 1 ≤ i ≤ len(l). Because (Bound S := P d) = {S}, it is a write set.

For any database db and any pair of complete tuples t_{1} and t_{2} over V_{db}, if

t_{1}[head(P d)] = t_{2}[head(P d)],

then

{v_{1} ∈ V_{db}|(db, t_{1}, P d) ⇝ v_{1}} = {v_{2} ∈ V_{db}|(db, t_{2}, P d) ⇝ v_{2}}.

So, according to the definition, F(S, list({v_{1} ∈ V_{db}|(db, t_{1}, P d) ⇝ v_{1}})) = F(S, list({v_{2} ∈ V_{db}|(db, t_{2}, P d) ⇝ v_{2}}))

{l_{1}[{S}]|l_{1} ∈ [[S := P d]]_{db}^{t_{1}}} = {l_{2}[{S}]|l_{2} ∈ [[S := P d]]_{db}^{t_{2}}}.

Now, let’s consider the projection on the head(P d) set. If head(P d) = {S}, (Var S := P d) = {S}. Therefore, (Var S := P d) is a read set by definition. Otherwise, head(P d) ∩ (Bound S := P d) = ∅, so head(P d) ⊆ (α(t) − (Bound S := P d)). For any complete tuple t over V_{db}, and for each l ∈ [[S := P d]]_{db}^{t},

nth(l, i)[head(P d)] = t[head(P d)], for all 1 ≤ i ≤ len(l).

Therefore,

{l_{1}[{S} ∪ head(P d)]|l_{1} ∈ [[S := P d]]_{db}^{t_{1}}} = {l_{2}[{S} ∪ head(P d)]|l_{2} ∈ [[S := P d]]_{db}^{t_{2}}}. Because t_{1}[(Var S := P d)] = t_{2}[(Var S := P d)] implies t_{1}[head(P d)] = t_{2}[head(P d)], and (Var S := P d) = {S} ∪ head(P d), therefore,

{l_{1}[(Var S := P d)]|l_{1} ∈ [[S := P d]]_{db}^{t_{1}}} = {l_{2}[(Var S := P d)]|l_{2} ∈ [[S := P d]]_{db}^{t_{2}}}. The basis holds.

Induction. Assume the conclusion is true for all the query trees whose depth are less than n, and now we consider the case that the query tree has depth of n, n > 1.

Now, the query tree may be one of eight kinds. Due to the space limit, we also only prove one kind as an example, and leave others to interested readers. Here, we consider the Keep operator as the root of the query tree, i.e., the query E′ is of form:

(Keep S_{1}, …, S_{n} E),

and the corresponding Bound and Var sets are, (Bound E′) = (Bound E) ∩{S_{1}, …, S_{n}},

(Var E′) = (Var E) ∪{S_{1}, …, S_{n}}.

According to the definition, for any database db and any complete tuple t over V_{db},

[[(Keep S_{1}, …, S_{n} E)]]_{db}^{t} = {l′|∃l ∈ [[E]]_{db}^{t} such that l′ = (l[S_{1}, …, S_{n}] ≺ t)},

therefore, for each l′ ∈ [[(Keep S_{1}, …, S_{n} E)]]_{db}^{t},

nth(l′, i)[α(t) − {S_{1}, …, S_{n}}] = t[α(t) − {S_{1}, …, S_{n}}].

Because the depth of E is less than n, by assumption, (Bound E) is a write set, i.e., for any database db and any complete tuple t over V_{db}, for each l ∈ [[E]]_{db}^{t},

nth(l, i)[α(t) − (Bound E)] = t[α(t) − (Bound E)].

For each l′ ∈ [[(Keep S_{1}, …, S_{n} E)]]_{db}^{t}, there exists l ∈ [[E]]_{db}^{t} such that

l′ = (l[S_{1}, …, S_{n}] ≺ t),

therefore,

nth(l′, i)[α(t) − (Bound E)] = t[α(t) − (Bound E)].

Thus, by set theory, nth(l′, i)[α(t) − (Bound E) ∩ {S_{1}, …, S_{n}}] = t[α(t) − (Bound E) ∩ {S_{1}, …, S_{n}}], i.e., (Bound E′) is a write set.

Now, we try to prove that (Var E′) is a read set. For any database db, let t_{1} and t_{2} are two complete tuples over V_{db} such that t_{1}[(Var E′)] = t_{2}[(Var E′)], i.e.,

t_{1}[(Var E) ∪ {S_{1}, …, S_{n}}] = t_{2}[(Var E) ∪ {S_{1}, …, S_{n}}],

which implies

t_{1}[(Var E)] = t_{2}[(Var E)].

By assumption,

{l_{1}[(Var E)]|l_{1} ∈ [[E]]_{db}^{t_{1}}} = {l_{2}[(Var E)]|l_{2} ∈ [[E]]_{db}^{t_{2}}}.

Further, {l_{1}[(Var E) ∪ {S_{1}, …, S_{n}}]|l_{1} ∈ [[E]]_{db}^{t_{1}}} = {l_{2}[(Var E) ∪ {S_{1}, …, S_{n}}]|l_{2} ∈ [[E]]_{db}^{t_{2}}}.

By the definition of the Keep operator,

[[E′]]_{db}^{t_{1}} = [[E′]]_{db}^{t_{2}},

so, {l_{1}[(Var E) ∪ {S_{1}, …, S_{n}}]|l_{1} ∈ [[E′]]_{db}^{t_{1}}} = {l_{2}[(Var E) ∪ {S_{1}, …, S_{n}}]|l_{2} ∈ [[E′]]_{db}^{t_{2}}}, which means that (Var E′) is a read set.

By the basis and induction part, we can draw the conclusion that for a ground query E, (Bound E) and (Var E) are a write set and a read set, respectively.

Now, we prove that (Var E) is a write set, too.

By the definition of the Bound and Var set, for any ground query E,

(Bound E) ⊆ (Var E),

so, for any database db and any complete tuple t over V_{db},

(α(t) − (Var E)) ⊆ (α(t) − (Bound E)).

(Bound E) is a write set, so for any database db and any complete tuple t over V_{db}, for each l ∈ [[E]]_{db}^{t},

nth(l, i)[α(t) − (Bound E)] = t[α(t) − (Bound E)],

for each 1 ≤ i ≤ len(l), which implies

nth(l, i)[α(t) − (Var E)] = t[α(t) − (Var E)],

for each 1 ≤ i ≤ len(l).

Thus, (Var E) is a write set, too.

□

4 Two Important Axioms for the Nest Operator

Since the query algebra is operator-oriented, to explore the axioms for the refinement calculus, and finally to analyze the correctness for rule-based query optimization, it is beneficial to examine the basic properties of each operator. In this section, we focus on one important operator, Nest, and examine its associativity and commutativity.

4.1 Associativity for the Nest Operator

Lemma 4.1 For any database db, any query E, and any pair of lists l_{1} and l_{2},

J (db, E, app(l_{1}, l_{2})) = {app(l′_{1}, l′_{2})|l′_{1} ∈ J (db, E, l_{1}) and l′_{2} ∈ J (db, E, l_{2})}.

Proof: By induction of length of list l_{1}.

basis. Trivial for len(l_{1}) = 0.

induction. True for len(l_{1}) < n. Consider when len(l_{1}) = n.

By definition,

J (db, E, app(l_{1}, l_{2})) = {app(l_{3}, l_{4})|l_{3} ∈ [[E]]_{db}^{hd(l_{1})} and l_{4} ∈ J (db, E, app(tl(l_{1}), l_{2})}. Applying the assumption,

l_{4} ∈ {app(l_{5}, l′_{2})|l_{5} ∈ J (db, E, tl(l_{1})) and l′_{2} ∈ J (db, E, l_{2})},

therefore,

app(l_{3}, l_{4}) = app(l_{3}, app(l_{5}, l′_{2})) = app(app(l_{3}, l_{5}), l′_{2}).

Also by definition,

app(l_{3}, l_{5}) ∈ J (db, E, l_{1}).

Let it be l′_{1}, then the lemma is true for len(l) = n. □

Lemma 4.2 For any database db, any pair of queries E_{1} and E_{2}, and any list l, 4 TWO IMPORTANT AXIOMS FOR THE NEST OPERATOR 14

J (db, (Nest E_{1} E_{2}), l) = ⋃_{l′∈J (db,E_{1},l)} J (db, E_{2}, l′).

Proof: By induction of length of list l.

basis. Trivial for len(l) = 0.

induction. True for len(l) < n. Consider when len(l) = n.

By definition,

J (db, (Nest E_{1} E_{2}), l)

= {app(l_{1}, l_{2})|l_{1} ∈ [[(Nest E_{1} E_{2})]]_{db}^{hd(l)} and l_{2} ∈ J (db, (Nest E_{1} E_{2}), tl(l))}.

Further by definition,

[[(Nest E_{1} E_{2})]]_{db}^{hd(l)} = ⋃_{l_{3}∈[[E_{1}]]_{db}^{hd(l)}} J (db, E_{2}, l_{3}).

Applying the assumption,

J (db, (Nest E_{1} E_{2}), tl(l)) = ⋃_{l_{4}∈J (db,E_{1},tl(l))} J (db, E_{2}, l_{4}).

So, by set theory, J (db, (Nest E_{1} E_{2}), l) = ⋃_{l_{3}∈[[E_{1}]]_{db}^{hd(l)} and l_{4}∈J (db,E_{1},tl(l))}{app(l_{1}, l_{2})|l_{1} ∈ J (db, E_{2}, l_{3}) and l_{2} ∈ J (db, E_{2}, l_{4})}. By Lemma 4.1,

J (db, (Nest E_{1} E_{2}), l) = ⋃_{l_{3}∈[[E_{1}]]_{db}^{hd(l)} and l_{4}∈J (db,E_{1},tl(l))} J (db, E_{2}, app(l_{3}, l_{4})). Let l′ be app(l_{3}, l_{4}), then we get

J (db, (Nest E_{1} E_{2}), l) = ⋃_{l′∈J (db,E_{1},l)} J (db, E_{2}, l′)).

Therefore, the lemma is true for len(l) = n. □

Theorem 4.1 Associativity holds for the operator Nest, i.e., (Ref (Nest (Nest E1 E2) E3) (Nest E1 (Nest E2 E3))) (Ref (Nest E1 (Nest E2 E3)) (Nest (Nest E1 E2) E3))

4 TWO IMPORTANT AXIOMS FOR THE NEST OPERATOR 15 both are axioms. Proof: By the definition of axiom.

For any database db and any complete tuple t over V_{db}, by definition,

[[(Nest (Nest E_{1} E_{2}) E_{3})]]_{db}^{t} = ⋃_{l∈[[(Nest E_{1} E_{2})]]_{db}^{t}} J (db, E_{3}, l)
= ⋃_{l∈⋃_{l′∈[[E_{1}]]{t \atop db}} J (db,E_{2},l′)}(db, E_{3}, l)
= ⋃_{l′∈[[E_{1}]]_{db}^{t}}(⋃_{l∈J (db,E_{2},l′)}(db, E_{3}, l))
[[(Nest E_{1} (Nest E_{2} E_{3}))]]_{db}^{t} = ⋃_{l′∈[[E_{1}]]_{db}^{t}} J (db, (Nest E_{2} E_{3}), l′)

By Lemma 4.2,

[[(Nest (Nest E_{1} E_{2}) E_{3})]]_{db}^{t} = [[(Nest E_{1} (Nest E_{2} E_{3}))]]_{db}^{t}

Therefore, the two reference rules are axioms.

□

4.2 Commutativity for the Nest Operator

Unlike associativity, in general, commutativity does not hold for the Nest operator. However, a nice property holds under certain conditions. Lemma 4.3 Given two expressions E_{1} and E_{2} such that

(Bound E_{1}) ∩ (Var E_{2}) = ∅ ,

then for any database db and any complete tuple t over V_{db}, for each l ∈ [[E_{1}]]_{db}^{t}, 4 TWO IMPORTANT AXIOMS FOR THE NEST OPERATOR 16

{l′[(Var E_{2})] ≺ t|l′ ∈ [[E_{2}]]_{db}^{nth(l,i)}} = [[E_{2}]]_{db}^{t}

for 1 ≤ i ≤ len(l). Proof: According to Theorem 3.1, for each l ∈ [[E_{1}]]_{db}^{t}, for any 1 ≤ i ≤ len(l),

nth(l, i)[α(t) − (Bound E_{1})] = t[α(t) − (Bound E_{1})].

Because E_{1} and E_{2} satisfy the emptyset condition

(Bound E_{1}) ∩ (Var E_{2}) = ∅,

we have

(Var E_{2}) ⊆ α(t) − (Bound E_{1}),

so,

nth(l, i)[(Var E_{2})] = t[(Var E_{2})].

Also by Theorem 3.1,

{l′[(Var E_{2})] ≺ t|l′ ∈ [[E_{2}]]_{db}^{nth(l,i)}} = {l′′[(Var E_{2})] ≺ t|l′′ ∈ [[E_{2}]]_{db}^{t}}. Because l′′ ∈ [[E_{2}]]_{db}^{t}, we know that

l′′[(Var E_{2})] ≺ t = l′′,

thus

{l′[(Var E_{2})] ≺ t|l′ ∈ [[E_{2}]]_{db}^{nth(l,i)}} = [[E_{2}]]_{db}^{t}.
□

Lemma 4.4 Given two ground queries E_{1} and E_{2} such that

(Bound E_{1}) ∩ (Var E_{2}) = ∅,

for any database db and any complete tuple t over V_{db}, for a list l satisfying that there exists l′ and app(l′, l) ∈ [[E_{1}]]_{db}^{t},

J (db, E_{2}, l) ≠ {()} if and only if [[E_{2}]]_{db}^{nth(l,i)} ≠ {()},

for each 1 ≤ i ≤ len(l).

4 TWO IMPORTANT AXIOMS FOR THE NEST OPERATOR 17

Proof:

if. For each 1 ≤ i ≤ len(l), [[E_{2}]]_{db}^{nth(l,i)} ≠ {()}.

And by the definition of J,

J (db, E_{2}, l) = \{ \begin{matrix}\{()\} & if len(l) = 0 \\ \{app(l_{1}, l_{2})|l_{1} ∈ [[E_{2}]]_{db}^{hd(l)} and l_{2} ∈ J (db, E_{2}, tl(l))\} & otherwise \end{matrix}

so, it is trivial to conclude J (db, E_{2}, l) ≠ {()}.

only if. J (db, E_{2}, l) ≠ {()}.

By definition, there must exist a tuple in l, say nth(l, j) for some 1 ≤ j ≤ len(l), which satisfies

[[E_{2}]]_{db}^{nth(l,j)} ≠ {()}.

By Theorem 3.1, and the condition for l, there exists l′ such that app(l′, l) ∈ [[E_{1}]]_{db}^{t},

nth(l, i)[α(t) − (Bound E_{1})] = t[α(t) − (Bound E_{1})],

for 1 ≤ i ≤ len(l).

Because of the empty condition,

(Bound E_{1}) ∩ (Var E_{2}) = ∅,

the above statement can be written as,

nth(l, i)[(Var E_{2})] = t[(Var E_{2})],

for 1 ≤ i ≤ len(l). Further, by Lemma 4.3,

{l′[(Var E_{2})] ≺ t|l′ ∈ [[E_{2}]]_{db}^{nth(l,i)}} = [[E_{2}]]_{db}^{t},

for 1 ≤ i ≤ len(l).

Therefore, [[E_{2}]]_{db}^{nth(l,j)} ≠ {()}, implies [[E_{2}]]_{db}^{nth(l,i)} ≠ {()}, for for 1 ≤ i ≤ len(l). □ Lemma 4.5 Let E_{1}, E_{2}, db, t and l_{1} denote a pair of ground queries, a database, a complete tuple and a list of tuples, respectively, which satisfy the following conditions:

C1. (Bound E_{1}) ∩ (Var E_{2}) = ∅,

C2. db ⊧ (Ref E_{2} (Filter E_{2})),

C3. l_{1} ∈ {l′_{1}|∃l′′_{1} s.t. app(l′′_{1}, l′_{1}) ∈ [[E_{1}]]_{db}^{t}},

If J (db, E_{2}, l_{1}) ≠ {()}, then for any non-empty l_{2} ∈ [[E_{2}]]_{db}^{t}, there exists l ∈ J (db, E_{2}, l_{1}) such that

C4. l[α(t) − (Bound E_{2})] ≺ t = l_{1},

C5. nth(l, i)[(Var E_{2})] = hd(l_{2})[(Var E_{2})], for all 1 ≤ i ≤ len(l).

Proof: By induction on the length of l_{1}.

basis. There are two basic cases here. len(l_{1}) = 0 and len(l_{1}) = 1. If len(l_{1}) = 0, the lemma is trivial by the definition of the J function. Now, consider len(l_{1}) = 1, i.e., l_{1} consists of a single tuple, and we have tl(l_{1}) = ().

By definition,

J (db, E_{2}, l_{1}) = [[E_{2}]]_{db}^{hd(l_{1})}.

Based on C2, we have, for any complete tuple t over V_{db}, for each l_{2} ∈ [[E_{2}]]_{db}^{t},

len(l_{2}) = 0, or len(l_{2}) = 1,

which means that if J (db, E_{2}, l_{1}) ≠ {()}, there exists at least a non-empty list l ∈ J (db, E_{2}, l_{1}), and for any non-empty list l ∈ J (db, E_{2}, l_{1}), len(l) = 1.

By Theorem 3.1 and C3, for any complete tuple t over V_{db}, hd(l_{1})[α(t) − (Bound E_{1})] = t[α(t) − (Bound E_{1})], and adding C1,

hd(l_{1})[(Var E_{2})] = t[(Var E_{2})],

then by Lemma 4.3,

{l[(Var E_{2})] ≺ t|l ∈ [[E_{2}]]_{db}^{hd(l_{1})}} = [[E_{2}]]_{db}^{t}.

Now, for any non-empty list l_{2} ∈ [[E_{2}]]_{db}^{t}, there exists a non-empty list l ∈ [[E_{2}]]_{db}^{hd(l_{1})} such that

hd(l)[(Var E_{2})] = hd(l_{2})[(Var E_{2})],

and by Theorem 3.1,

hd(l)[α(t) − (Bound E_{2})] ≺ t = hd(l_{1}).

Because len(l) = 1, conclusions C4 and C5 hold.

So, the basis is true.

Induction. Assume the lemma is true for len(l_{1}) < n, and now consider the case when len(l_{1}) = n.

If J (db, E_{2}, l_{1}) ≠ {()}, by Lemma 4.4,

[[E_{2}]]_{db}^{hd(l_{1})} ≠ {()}, and J (db, E_{2}, tl(l_{1})) ≠ {()}.

Because tl(l_{1}) still satisfies C3, by the assumption, if J (db, E_{2}, tl(l_{1})) ≠ {()}, then for any non-empty l_{2} ∈ [[E_{2}]]_{db}^{t}, there exists l′′ ∈ J (db, E_{2}, tl(l_{1})) such that

l′′[α(t) − (Bound E_{2})] ≺ t = tl(l_{1}),

nth(l′′, i)[(Var E_{2})] = hd(l_{2})[(Var E_{2})],

for all 1 ≤ i ≤ len(l′′).

And similar to the basis for len(l) = 1, if [[E_{2}]]_{db}^{hd(l_{1})} ≠ {()}, then

{l′[(Var E_{2})] ≺ t|l′ ∈ [[E_{2}]]_{db}^{hd(l_{1})}} = [[E_{2}]]_{db}^{t}.

Now, for any non-empty list l_{2} ∈ [[E_{2}]]_{db}^{t}, there exists a non-empty list l′ ∈ [[E_{2}]]_{db}^{hd(l_{1})} such that

len(l′) = 1,

hd(l′)[(Var E_{2})] = hd(l_{2})[(Var E_{2})],

and by Theorem 3.1,

hd(l′)[α(t) − (Bound E_{2})] ≺ t = hd(l_{1}).

Now, we fix l_{2}, and let l = app(l′, l′′). By the definition of J, l ∈ J (db, E_{2}, l_{1}), and len(l) ≠ 0. Further, it is easy to see that l satisfies C4 and C5. So, the induction is true.

By the basis and the induction, we can draw the conclusion that the lemma is true.

□

Now, it is time to state and prove the commutative property for the Nest operator.

Theorem 4.2 The inference rule

( Clause (Ref (Nest E1 E2) (Nest E2 E1))

(Ref E2 (Filter E2))

(Empty (Intersect (Bound E1) (Var E2))) (Empty (Intersect (Var E1) (Bound E2))))

is an axiom.

Proof: By contradiction.

If the rewrite rule is not an axiom, there exist a database db and a ground rule R, which is of the form:

(Clause (Ref (Nest E_{1} E_{2}) (Nest E_{2} E_{1}))

(Ref E_{2} (Filter E_{2}))

(Empty (Intersect (Bound E_{1}) (Var E_{2}))) (Empty (Intersect (Var E_{1}) (Bound E_{2})))), such that for some complete tuple t,

1. db ⊧ (Ref E_{2} (Filter E_{2}))

2. db ⊧ (Empty (Intersect (Bound E_{1}) (Var E_{2})))

3. db ⊧ (Empty (Intersect (Var E_{1}) (Bound E_{2}))), and

4. [[(Nest E_{2} E_{1})]]_{db}^{t} ⊈ [[(Nest E_{1} E_{2})]]_{db}^{t}.

Now, we try to contradict condition 4, based on condition 1, 2 and 3. Here, the empty list and the non-empty lists are considered separately.

Empty list. For any database db and any complete tuple t over V_{db}, if there exists an empty list in [[(Nest E_{2} E_{1})]]_{db}^{t}, according to the definition of operator Nest,

[[(Nest E_{2} E_{1})]]_{db}^{t} = ⋃_{l_{2}∈[[E_{2}]]_{db}^{t}} J (db, E_{1}, l_{2}),

there must exist l_{2} ∈ [[E_{2}]]_{db}^{t} such that () ∈ J (db, E_{1}, l_{2}). Further, by function J, l_{2} could be an empty list or a non-empty list.

l_{2} is an empty list. By Lemma 4.3, there exists a list l_{1} ∈ [[E_{1}]]_{db}^{t},

{l′[(Var E_{2})] ≺ t|l′ ∈ [[E_{2}]]_{db}^{nth(l_{1},i)}} = [[E_{2}]]_{db}^{t},

which implies

() ∈ [[E_{2}]]_{db}^{nth(l,i)},

for 1 ≤ i ≤ len(l_{1}), so, by the definition of function J, () ∈ J (db, E_{2}, l_{1}), which indicates that () ∈ [[(Nest E_{1} E_{2})]]_{db}^{t}.

l_{2} is a non-empty list. By the key condition, we know that len(l_{2}) = 1, i.e., l_{2} is a list consisting of a single tuple hd(l_{2}), so

J (db, E_{1}, l_{2}) = [[E_{1}]]_{db}^{hd(l_{2})}.

By Lemma 4.3 (with condition 3), 4 TWO IMPORTANT AXIOMS FOR THE NEST OPERATOR 22

{l′[(Var E_{1})] ≺ t|l′ ∈ [[E_{1}]]_{db}^{hd(l_{2})}} = [[E_{1}]]_{db}^{t},

so we have () ∈ [[E_{1}]]_{db}^{t}, which means () ∈ [[(Nest E_{1} E_{2})]]_{db}^{t}.

Non-empty list. For any database db and any complete tuple t over V_{db}, if there exists a non-empty list l ∈ [[(Nest E_{2} E_{1})]]_{db}^{t}, there must be a non-empty list l′ ∈ [[E_{2}]]_{db}^{t} such that l ∈ J (db, E_{1}, l′). By the key condition, l ∈ [[E_{1}]]_{db}^{hd(l′)}.

According to Theorem 3.1,

hd(l′)[(Var E_{1})] = t[(Var E_{1})],

and further by Lemma 4.3 (with condition 3),

{l[(Var E_{1})] ≺ t|l ∈ [[E_{1}]]_{db}^{hd(l′)}} = [[E_{1}]]_{db}^{t},

so, there exists a corresponding list l_{1} ∈ [[E_{1}]]_{db}^{t} such that

l[(Var E_{1})] = l_{1}[(Var E_{1})].

Two possibilities are considered here.

Empty possibility. J (db, E_{2}, l_{1}) = {()}. By definition

[[E_{2}]]_{db}^{hd(l_{1})} = {()},

and by Theorem 3.1,

hd(l_{1})[(Var E_{2})] = t[(Var E_{2})],

so, finally by Lemma 4.3,

[[E_{2}]]_{db}^{t} = {()}.

By definitions,

[[(Nest E_{2} E_{1})]]_{db}^{t} = {()}.

Because we have l is a non-empty list in [[(Nest E_{2} E_{1})]]_{db}^{t}, so there is no such a possibility.

Non-empty possibility. J (db, E_{2}, l_{1}) ≠ {()}. By Lemma 4.5, there is l_{2} ∈ J (db, E_{2}, l_{1}) such that

l_{2}[α(t) − (Bound E_{2})] ≺ t = l_{1},

nth(l_{2}, i)[(Var E_{2})] = hd(l′)[(Var E_{2})],

which implies

l_{2}[(Var E_{1})] = l[(Var E_{1})],
nth(l_{2}, i)[(Var E_{2})] = nth(l, i)[(Var E_{2})],

for all 1 ≤ i ≤ len(l_{2}). So, we have

l[(Var E_{1}) ∪ (Var E_{2})] = l_{2}[(Var E_{1}) ∪ (Var E_{2})].

Finally, by Theorem 3.1, l = l_{2}, which means

l ∈ [[(Nest E_{1} E_{2})]]_{db}^{t}.

Because of the generality of l, we can say

[[(Nest E_{2} E_{1})]]_{db}^{t} ⊆ [[(Nest E_{1} E_{2})]]_{db}^{t},

which contradicts to the assumption, therefore the rewrite rule is an axiom.

□

From this theorem, an interesting axiom could be drawn directly.

Corollary 4.2.1 The inference rule

( Clause (Ref (Nest E1 E2) (Cross E1 E2))

(Ref E2 (Filter E2))

(Empty (Intersect (Bound E1) (Var E2))) (Empty (Intersect (Var E1) (Bound E2))))

is an axiom.

Proof: The proof is conducted by contradiction. Let’s assume that the given rule is not an axiom, so there must exist a database db and a ground rule R (generated from the given rule by substitution), which is of the form:

(Clause (Ref (Nest E_{1} E_{2}) (Cross E_{1} E_{2}))

(Ref E_{2} (Filter E_{2}))

(Empty (Intersect (Bound E_{1}) (Var E_{2}))) (Empty (Intersect (Var E_{1}) (Bound E_{2})))),

such that for some complete tuple t,

1. db ⊧ (Ref E_{2} (Filter E_{2}))

2. db ⊧ (Empty (Intersect (Bound E_{1}) (Var E_{2})))

3. db ⊧ (Empty (Intersect (Var E_{1}) (Bound E_{2}))), and

4. [[(Cross E_{1} E_{2})]]_{db}^{t} ⊈ [[(Nest E_{1} E_{2})]]_{db}^{t}.

However, by the theorem 4.2, under the condition 1, 2 and 3, we have

[[(Nest E_{2} E_{1})]]_{db}^{t} ⊆ [[(Nest E_{1} E_{2})]]_{db}^{t}.

and by the definition of the Cross operator,

[[(Cross E1 E2)]]_{db}^{t} = [[(Nest E1 E2)]]_{db}^{t} ∪ [[(Nest E2 E1)]]_{db}^{t}

so for any database db and complete tuple t,

[[(Cross E_{1} E_{2})]]_{db}^{t} ⊆ [[(Nest E_{1} E_{2})]]_{db}^{t}.

which is contradictory to the assumption.

Therefore, the given rule is an axiom.

□

5 Correctness of A Real-World Rewrite Rule

A query rewrite rule is an inference rule defined in the refinement calculus with the following fixed format:

(Clause (Ref E_{1} E_{2}) R_{1}, …, R_{n})

We say a query rewrite rule is correct if and only if it is an axiom.

In this section, we use the refinement calculus inference axioms (given in Table

3) to derive the correctness of a real-world rewrite rule from a set of axioms in the

refinement calculus. This derivation shows the proof theory for the calculus, although

the theory is not complete.

5.1 More Related Axioms

Before we get into the derivation of the correctness of the real-world rewrite rule, we

need to prove four more related basic axioms to be used in the derivation.

Theorem 5.1 The following rules are axioms.

1. (Ref (Cross E*1 E1 E*2) (Nest E1 (Cross E*1 E*2)))

2. (Clause

(Ref (Nest E1 (Cross E*1)) (Cross E1 E*1))

(Ref E1 (Filter E1))

(Empty (Intersect (Var (Cross E*1)) (Bound E1))) (Empty (Intersect (Bound (Cross E*1)) (Var E1))))

3. (Clause

(Clause (Ref (Nest E1 E2) (Nest E3 E4)) R*1)

(Clause (Ref E1 E2) R*1) (Clause (Ref E3 E4) R*1))

4. (Clause

(Clause (Ref E1 E2) R*1) (Clause (Ref E1 E3) R*1) (Clause (Ref E3 E2) R*1))

Proof: We prove them one by one, based on the model theory of the refinement calculus.

Rule 1. It is trivial by the definition of the Cross operator.

Rule 2. As usual, the proof is by contradiction. If the rule is not an axiom, then for some ground rule substituted from the rule, which is of the form

(Clause (Ref (Nest E_{1} (Cross E_{2}, …, E_{n})) (Cross E_{1} E_{2}, …, E_{n}))

(Ref E_{1} (Filter E_{1}))

(Empty (Intersect (Var (Cross E_{2}, …, E_{n})) (Bound E_{1}))) (Empty (Intersect (Bound (Cross E_{2}, …, E_{n})) (Var E_{1})))),

there must exist a database db, which satisfies,

1. db ⊧ (Ref E_{1} (Filter E_{1})),

2. db ⊧ (Empty (Intersect (Var (Cross E_{2}, …, E_{n})) (Bound E_{1}))),

3. db ⊧ (Empty (Intersect (Bound (Cross E_{2}, …, E_{n})) (Var E_{1}))), and

4. [[(Cross E_{1}, E_{2}, …, E_{n})]]_{db}^{t} ⊈ [[(Nest E_{1} (Cross E_{2}, …, E_{n}))]]_{db}^{t}, for some complete tuple t.

However, by the definition of the Cross operator,

[[(Cross E_{1}, …, E_{n})]]_{db}^{t}
= ⋃_{1≤i≤n} [[(Nest E_{i} (Cross E_{1}, …, E_{i−1}, E_{i+1}, …, E_{n}))]]_{db}^{t}
= ⋃_{1≤q_{1}≤n,...,1≤q_{n}≤n} [[(Nest E_{q_{1}} (Nest … (Nest E_{q_{n}})))]]_{db}^{t}

where q_{1}, …, q_{n} is a permutation of the number 1, …, n, therefore every list l ∈ [[(Cross E_{1}, …, E_{n})]]_{db}^{t} must belong to some

[[(Nest E_{q_{1}} (Nest … (Nest E_{q_{n}})))]]_{db}^{t} .

Without losing generality, let’s assume q_{t} be 1 (1/leqt/leqn). By the commutativity and the associativity of the Nest operator (Theorem 4.1 and 4.2), we can exchange subexpressions E_{q_{1}} and E_{q_{t}} inside the last expression, and have the equation below:

[[(Nest E_{q_{1}} (Nest … (Nest E_{q_{n}})))]]_{db}^{t} = [[(Nest E_{q_{t}} (Nest … (Nest E_{q_{t−1}} (Nest E_{q_{1}} (Nest E_{q_{t+1}} … (Nest E_{q_{n}})))))]]_{db}^{t}.

It is easy to see that q_{1}, …, q_{t−1}, q_{t+1}, …, q_{n} is a permutation of 2, …, n, and also by the definition of the Cross operator, any list l′ in

[[(Nest E_{q_{2}} (Nest … (Nest E_{q_{t−1}} (Nest E_{q_{1}} (Nest E_{q_{t+1}} … (Nest E_{q_{n}})))))]]_{db}^{t}, belongs to [[(Cross E_{2}, …, E_{n})]]_{db}^{t}. Therefore, back to the definition of the Nest operator, we have

l ∈ [[(Nest E_{1} (Cross E_{2}, …, E_{n}))]]_{db}^{t}.

Since the arbitrariness of l, the assumption is wrong, so Rule 2 is an axiom.

Rule 3. By contradiction. If the rule is not an axiom, there exists a ground rule of the form:

(Clause

(Clause (Ref (Nest E_{1} E_{2}) (Nest E_{3} E_{4})) R_{1}, …, R_{n})
(Clause (Ref E_{1} E_{3}) R_{1}, …, R_{n})
(Clause (Ref E_{2} E_{4}) R_{1}, …, R_{n}))

which satisfies:

1. db ⊧ (Clause (Ref E_{1} E_{3}) R_{1}, …, R_{n}), 2. db ⊧ (Clause (Ref E_{2} E_{4}) R_{1}, …, R_{n}), and

3. db |̸= (Clause (Ref (Nest E_{1} E_{2}) (Nest E_{3} E_{4})) R_{1}, …, R_{n})

db ⊧ (Clause (Ref E_{1} E_{3}) R_{1}, …, R_{n}) means:

db ⊧ (Ref E_{1} E_{3})) if db ⊧ R_{i}, for 1 ≤ i ≤ n.

db ⊧ (Clause (Ref E_{2} E_{4}) R_{1}, …, R_{n}) means:

db ⊧ (Ref E_{2} E_{4})) if db ⊧ R_{i}, for 1 ≤ i ≤ n.

Since (Clause (Ref (Nest E1 E2) (Nest E3 E4)) (Ref E1 E3) (Ref E2 E4)) is an axiom (refer to [CW93]), we have

db ⊧ (Ref (Nest E_{1} E_{2}) (Nest E_{3}E_{4})) if \{ \begin{matrix}db ⊧ (Ref E1 E3) \\ db ⊧ (Ref E2 E4) \end{matrix}

Therefore,

db ⊧ (Ref (Nest E_{1} E_{2}) (Nest E_{3} E_{4})) if if db ⊧ R_{i}, for 1 ≤ i ≤ n. which implies

db ⊧ (Clause (Ref (Nest E_{1} E_{2}) (Nest E_{3} E_{4})) R_{1}, …, R_{n}),

so the assumption is wrong, and Rule 3 is an axiom.

Rule 4. Can be proved in the same way as the last one. We leave the proof for the interested readers.

□

5.2 The Derivation of the Correctness

In general, the real-world rewrite rules are much more complex than the axioms that have been proved so far. Although the rewrite rules can be proved from the model Table 5: A Real-World Query Rewrite Rule (in the refinement calculus)

(Clause (Ref

(Nest E1

(Nest (Cross E*1)

(Nest E2 (Nest (Cross E*2 E3 E*3) E4)))) (Nest E1

(Nest (Cross E3 E*1)

(Nest E2 (Nest (Cross E*2 E*3) E4))))) (Ref E3 (Filter E3)) (Empty (Intersect (Bound E2) (Var E3))) (Empty (Intersect (Bound (Cross E*1)) (Var E3))) (Empty (Intersect (Var E2) (Bound E3))) (Empty (Intersect (Var (Cross E*1)) (Bound E3))))

theory (like the proofs we have gone through so far), it would be much easier to

derive them from a set of basic and simple axioms. Actually, we are very interested

in proving (i.e., derivation) from the proof theory because of its mechanical nature.

Due to the incompleteness of the proof theory, one of future work is to find out a base

set of axioms which could be used in general to prove the correctness of a rule-based

query optimizer.

With the power of the refinement calculus, we apply it to capture the intentions

underlying a real-world rule. In Table 5, we shows a formal specification in the

refinement calculus for the real-world rewrite rule mentioned earlier (referring to

Table 1). The rewrite rule was originally represented in a Lisp-like language, and

is translated into the refinement calculus for the analysis of its correctness. The

function of this rewrite rule is to generate a canonical form of a query expression by

moving all the predicates together, so that more semantic query optimizations would

be applied to the canonical form later on.

Now, let’s prove the correctness of the real-world rewrite rule by derivation (the

proof theory).

1. known axiom, refer to Theorem 5.1

(Ref (Cross E*1 E1 E*2)

(Nest E1 (Cross E*1 E*2)))

2. known axiom, Associativity of Nest, refer to Theorem 4.1

(Ref (Nest (Nest E1 E2) E3)

(Nest E1 (Nest E2 E3)))

3. substitution of 2 by { E1/E3, E2/(Cross E*2 E*3), E3/E4 }

(Ref (Nest (Nest E3 (Cross E*2 E*3)) E4) (Nest E3 (Nest (Cross E*2 E*3) E4)))

4. known axiom, refer to the paper [CW93]

(Clause (Ref (Nest E1 E2) (Nest E3 E4)) (Ref E1 E3) (Ref E2 E4))

5. substitution of 1 by { E*1/E*2, E1/E3, E*2/E*3 }

(Ref (Cross E*2 E3 E*3)

(Nest E3 (Cross E*2 E*3)))

6. substitution of 4 by { E1/(Cross E*2 E3 E*3), E2/E4, E3/(Nest E3 (Cross E*2 E*3)) }

(Clause

(Ref (Nest (Cross E*2 E3 E*3) E4)

(Nest (Nest E3 (Cross E*2 E*3)) E4)) (Ref (Cross E*2 E3 E*3) (Nest E3 (Cross E*2 E*3))))^{†}

7. modus ponens 5 and 6

(Ref (Nest (Cross E*2 E3 E*3) E4)

(Nest (Nest E3 (Cross E*2 E*3)) E4))

8. substitution of 4 by { E1/E2, E2/(Nest (Cross E*2 E3 E*3) E4), E3/E2, E4/(Nest (Nest E3 (Cross E*2 E*3)) E4) }

(Clause

(Ref (Nest E2 (Nest (Cross E*2 E3 E*3) E4))

(Nest E2 (Nest (Nest E3 (Cross E*2 E*3)) E4))) (Ref (Nest (Cross E*2 E3 E*3) E4)

(Nest (Nest E3 (Cross E*2 E*3)) E4)))

9. modus ponens 7 and 8

(Ref (Nest E2 (Nest (Cross E*2 E3 E*3) E4)) (Nest E2 (Nest (Nest E3 (Cross E*2 E*3)) E4)))

10. substitution of 4 by { E1/E2, E2/(Nest (Nest E3 (Cross E*2 E*3)) E4), E3/E2, E4/(Nest E3 (Nest (Cross E*2 E*3) E4)) }

(Clause

(Ref (Nest E2 (Nest (Nest E3 (Cross E*2 E*3)) E4))

(Nest E2 (Nest E3 (Nest (Cross E*2 E*3) E4)))) (Ref (Nest (Nest E3 (Cross E*2 E*3)) E4)

(Nest E2 (Nest E3 (Nest (Cross E*2 E*3) E4))))

11. modus ponens 3 and 10

(Ref (Nest E2 (Nest (Nest E3 (Cross E*2 E*3)) E4)) (Nest E2 (Nest E3 (Nest (Cross E*2 E*3) E4))))

12. known axiom, Associativity of Nest, refer to Theorem 4.1

(Ref (Nest E1 (Nest E2 E3))

(Nest (Nest E1 E2) E3))

13. substitution of 12 by { E1/E2, E2/E3, E3/(Nest (Cross E*2 E*3) E4) }

(Ref (Nest E2 (Nest E3 (Nest (Cross E*2 E*3) E4))) (Nest (Nest E2 E3) (Nest (Cross E*2 E*3) E4)))

14. known axiom, refer to the paper [CW93]

(Clause (Ref E1 E2) (Ref E1 E3) (Ref E3 E2))

15. substitution of 14 by { E1/(Nest E2 (Nest (Nest E3 (Cross E*2 E*3)) E4)), E2/(Nest (Nest E2 E3) (Nest (Cross E*2 E*3) E4)), E3/(Nest E2 (Nest E3 (Nest (Cross E*2 E*3) E4))) }

(Clause

(Ref (Nest E2 (Nest (Nest E3 (Cross E*2 E*3)) E4))

(Nest (Nest E2 E3) (Nest (Cross E*2 E*3) E4))) (Ref (Nest E2 (Nest (Nest E3 (Cross E*2 E*3)) E4))

(Nest E2 (Nest E3 (Nest (Cross E*2 E*3) E4)))) (Ref (Nest E2 (Nest E3 (Nest (Cross E*2 E*3) E4)))

(Nest (Nest E2 E3) (Nest (Cross E*2 E*3) E4))))

16. modus ponens 11, 13 and 15

(Ref (Nest E2 (Nest (Nest E3 (Cross E*2 E*3)) E4)) (Nest (Nest E2 E3) (Nest (Cross E*2 E*3) E4)))

17. substitution of 14 by { E1/(Nest E2 (Nest (Cross E*2 E3 E*3) E4))), E2/(Nest (Nest E2 E3) (Nest (Cross E*2 E*3) E4)), E3/(Nest E2 (Nest (Nest E3 (Cross E*2 E*3)) E4)) }

(Clause

(Ref (Nest E2 (Nest (Cross E*2 E3 E*3) E4)))

(Nest (Nest E2 E3) (Nest (Cross E*2 E*3) E4))) (Ref (Nest E2 (Nest (Cross E*2 E3 E*3) E4)))

(Nest E2 (Nest (Nest E3 (Cross E*2 E*3)) E4))) (Ref (Nest E2 (Nest (Nest E3 (Cross E*2 E*3)) E4))

(Nest (Nest E2 E3) (Nest (Cross E*2 E*3) E4))))

18. modus ponens 9, 16 and 17

(Ref (Nest E2 (Nest (Cross E*2 E3 E*3) E4))) (Nest (Nest E2 E3) (Nest (Cross E*2 E*3) E4)))

19. known axiom, Commutativity of Nest, refer to Theorem 4.2

(Clause (Ref (Nest E1 E2) (Nest E2 E1)) (Ref E2 (Filter E2)) (Empty (Intersect (Var E1) (Bound E2))) (Empty (Intersect (Bound E1) (Var E2))))

20. substitution of 19 by { E1/E2, E2/E3 }

(Clause (Ref (Nest E2 E3) (Nest E3 E2)) (Ref E3 (Filter E3)) (Empty (Intersect (Var E2) (Bound E3))) (Empty (Intersect (Bound E2) (Var E3))))

21. known axiom, refer to Theorem 5.1

(Clause (Clause (Ref (Nest E1 E2) (Nest E3 E4)) R*1) (Clause (Ref E1 E2) R*1) (Clause (Ref E3 E4) R*1))

22. substitution of 21 by { E1/(Nest E2 E3), E2/(Nest (Cross E*2 E*3) E4), E3/(Nest E3 E2), E4/(Nest (Cross E*2 E*3) E4)), R*1/R_{1} R_{2} R_{3} } where R_{1} represents (Ref E3 (Filter E3)), R_{2} indicates (Empty (Intersect (Var E2) (Bound E3))), and R_{3} means (Empty (Intersect (Bound E2) (Var E3)))^{‡} (Clause

‡For simplicity, we use these symbols in the following substitutions.

(Clause

(Ref (Nest (Nest E2 E3) (Nest (Cross E*2 E*3) E4))

(Nest (Nest E3 E2) (Nest (Cross E*2 E*3) E4))) (Ref E3 (Filter E3)) (Empty (Intersect (Var E2) (Bound E3))) (Empty (Intersect (Bound E2) (Var E3))))

(Clause (Ref (Nest E2 E3) (Nest E3 E2)) (Ref E3 (Filter E3)) (Empty (Intersect (Var E2) (Bound E3))) (Empty (Intersect (Bound E2) (Var E3)))))

23. modus ponens 20 and 22

(Clause

(Ref (Nest (Nest E2 E3) (Nest (Cross E*2 E*3) E4))

(Nest (Nest E3 E2) (Nest (Cross E*2 E*3) E4))) (Ref E3 (Filter E3)) (Empty (Intersect (Var E2) (Bound E3))) (Empty (Intersect (Bound E2) (Var E3))))

24. known axiom, refer to Theorem 5.1

(Clause (Clause (Ref E1 E2) R*1) (Clause (Ref E1 E3) R*1) (Clause (Ref E3 E2) R*1))

25. substitution of 24 by { E1/(Nest E2 (Nest (Cross E*2 E3 E*3) E4))), E2/(Nest (Nest E3 E2) (Nest (Cross E*2 E*3) E4)), E3/(Nest (Nest E2 E3) (Nest (Cross E*2 E*3) E4)), R*1/R_{1} R_{2} R_{3} } (Clause

(Clause (Ref (Nest E2 (Nest (Cross E*2 E3 E*3) E4)))

(Nest (Nest E3 E2) (Nest (Cross E*2 E*3) E4))) (Ref E3 (Filter E3)) (Empty (Intersect (Var E2) (Bound E3))) (Empty (Intersect (Bound E2) (Var E3))))

(Clause (Ref (Nest E2 (Nest (Cross E*2 E3 E*3) E4)))

(Nest (Nest E2 E3) (Nest (Cross E*2 E*3) E4))) (Ref E3 (Filter E3)) (Empty (Intersect (Var E2) (Bound E3))) (Empty (Intersect (Bound E2) (Var E3))))

(Clause (Ref (Nest (Nest E2 E3) (Nest (Cross E*2 E*3) E4))

(Nest (Nest E3 E2) (Nest (Cross E*2 E*3) E4))) (Ref E3 (Filter E3)) (Empty (Intersect (Var E2) (Bound E3))) (Empty (Intersect (Bound E2) (Var E3)))))

26. modus ponens 18, 23 and 25

(Clause

(Ref (Nest E2 (Nest (Cross E*2 E3 E*3) E4)))

(Nest (Nest E3 E2) (Nest (Cross E*2 E*3) E4))) (Ref E3 (Filter E3)) (Empty (Intersect (Var E2) (Bound E3))) (Empty (Intersect (Bound E2) (Var E3))))

27. substitution of 2 by { E1/E2, E3/(Nest (Cross E*2 E*3) E4) }

(Ref (Nest (Nest E3 E2) (Nest (Cross E*2 E*3) E4)) (Nest E3 (Nest E2 (Nest (Cross E*2 E*3) E4))))

28. substitution of 24 by { E1/(Nest E2 (Nest (Cross E*2 E3 E*3) E4))), E2/(Nest E3 (Nest E2 (Nest (Cross E*2 E*3) E4))), E3/(Nest (Nest E3 E2) (Nest (Cross E*2 E*3) E4)), R*1/R_{1} R_{2} R_{3} } (Clause

(Clause (Ref (Nest E2 (Nest (Cross E*2 E3 E*3) E4)))

(Nest E3 (Nest E2 (Nest (Cross E*2 E*3) E4)))) (Ref E3 (Filter E3)) (Empty (Intersect (Var E2) (Bound E3))) (Empty (Intersect (Bound E2) (Var E3))))

(Clause (Ref (Nest E2 (Nest (Cross E*2 E3 E*3) E4)))

(Nest (Nest E3 E2) (Nest (Cross E*2 E*3) E4))) (Ref E3 (Filter E3)) (Empty (Intersect (Var E2) (Bound E3))) (Empty (Intersect (Bound E2) (Var E3))))

(Clause (Ref (Nest (Nest E3 E2) (Nest (Cross E*2 E*3) E4))

(Nest E3 (Nest E2 (Nest (Cross E*2 E*3) E4)))) (Ref E3 (Filter E3)) (Empty (Intersect (Var E2) (Bound E3))) (Empty (Intersect (Bound E2) (Var E3)))))

29. modus ponens 26, 27 and 28

(Clause

(Ref (Nest E2 (Nest (Cross E*2 E3 E*3) E4)))

(Nest E3 (Nest E2 (Nest (Cross E*2 E*3) E4)))) (Ref E3 (Filter E3)) (Empty (Intersect (Var E2) (Bound E3))) (Empty (Intersect (Bound E2) (Var E3))))

30. substitution of 21 by { E1/(Cross E*1), E2/(Nest E2 (Nest (Cross E*2 E3 E*3) E4)), E3/(Cross E*1), E4/(Nest E3 (Nest E2 (Nest (Cross E*2 E*3) E4))), R*1/R_{1} R_{2} R_{3} } (Clause

(Clause

(Ref (Nest (Cross E*1)

(Nest E2 (Nest (Cross E*2 E3 E*3) E4))) (Nest (Cross E*1)

(Nest E3 (Nest E2 (Nest (Cross E*2 E*3) E4)))))

(Ref E3 (Filter E3)) (Empty (Intersect (Var E2) (Bound E3))) (Empty (Intersect (Bound E2) (Var E3))))

(Clause

(Ref (Nest E2 (Nest (Cross E*2 E3 E*3) E4))

(Nest E3 (Nest E2 (Nest (Cross E*2 E*3) E4)))) (Ref E3 (Filter E3)) (Empty (Intersect (Var E2) (Bound E3))) (Empty (Intersect (Bound E2) (Var E3)))))

31. modus ponens 29 and 30

(Clause

(Ref (Nest (Cross E*1)

(Nest E2 (Nest (Cross E*2 E3 E*3) E4))) (Nest (Cross E*1)

(Nest E3 (Nest E2 (Nest (Cross E*2 E*3) E4)))))

(Ref E3 (Filter E3)) (Empty (Intersect (Var E2) (Bound E3))) (Empty (Intersect (Bound E2) (Var E3))))

32. substitution of 12 by { E1/(Cross E*1), E2/E3, E3/(Nest E2 (Nest (Cross E*2 E*3) E4)) }

(Ref (Nest (Cross E*1)

(Nest E3 (Nest E2 (Nest (Cross E*2 E*3) E4)))) (Nest (Nest (Cross E*1) E3)

(Nest E2 (Nest (Cross E*2 E*3) E4))))

33. substitution of 24 by { E1/(Nest (Cross E*1) (Nest E2 (Nest (Cross E*2 E3 E*3) E4))), E2/(Nest (Nest (Cross E*1) E3) (Nest E2 (Nest (Cross E*2 E*3) E4))), E3/(Nest (Cross E*1) (Nest E3 (Nest E2 (Nest (Cross E*2 E*3) E4)))), R*1/R_{1} R_{2} R_{3} } (Clause

(Clause

(Ref (Nest (Cross E*1)

(Nest E2 (Nest (Cross E*2 E3 E*3) E4))) (Nest (Nest (Cross E*1) E3)

(Nest E2 (Nest (Cross E*2 E*3) E4))))

(Ref E3 (Filter E3)) (Empty (Intersect (Var E2) (Bound E3))) (Empty (Intersect (Bound E2) (Var E3))))

(Clause

(Ref (Nest (Cross E*1)

(Nest E2 (Nest (Cross E*2 E3 E*3) E4))) (Nest (Cross E*1)

(Nest E3 (Nest E2 (Nest (Cross E*2 E*3) E4)))))

(Ref E3 (Filter E3)) (Empty (Intersect (Var E2) (Bound E3))) (Empty (Intersect (Bound E2) (Var E3))))

(Clause

(Ref (Nest (Cross E*1)

(Nest E3 (Nest E2 (Nest (Cross E*2 E*3) E4)))) (Nest (Nest (Cross E*1) E3)

(Nest E2 (Nest (Cross E*2 E*3) E4))))

(Ref E3 (Filter E3)) (Empty (Intersect (Var E2) (Bound E3))) (Empty (Intersect (Bound E2) (Var E3)))))

34. modus ponens 31, 32 and 33

(Clause

(Ref (Nest (Cross E*1)

(Nest E2 (Nest (Cross E*2 E3 E*3) E4))) (Nest (Nest (Cross E*1) E3)

(Nest E2 (Nest (Cross E*2 E*3) E4))))

(Ref E3 (Filter E3)) (Empty (Intersect (Var E2) (Bound E3))) (Empty (Intersect (Bound E2) (Var E3))))

35. known axiom, refer to Theorem 5.1

(Clause (Ref (Nest (Cross E*1) E1) (Cross E1 E*1))) (Ref E1 (Filter E1)) (Empty (Intersect (Var (Cross E*1)) (Bound E1))) (Empty (Intersect (Bound (Cross E*1)) (Var E1))))

36. substitution of 35 by { E1/E3 }

(Clause (Ref (Nest (Cross E*1) E3) (Cross E3 E*1))) (Ref E3 (Filter E3)) (Empty (Intersect (Var (Cross E*1)) (Bound E3))) (Empty (Intersect (Bound (Cross E*1)) (Var E3))))

37. substitution of 21 by {E1/(Nest (Cross E*1) E3), E2/(Nest E2 (Nest (Cross E*2 E*3) E4)), E3/(Cross E3 E*1), E4/(Nest E2 (Nest (Cross E*2 E*3) E4))), R*1/R_{1} R_{4} R_{5} } where R_{4} indicates (Empty (Intersect (Var (Cross E*1)) (Bound E3))), and R_{5} means (Empty (Intersect (Bound (Cross E*1)) (Var E3)))

(Clause

(Clause

(Ref (Nest (Nest (Cross E*1) E3)

(Nest E2 (Nest (Cross E*2 E*3) E4))) (Nest (Cross E3 E*1)

(Nest E2 (Nest (Cross E*2 E*3) E4))))

(Ref E3 (Filter E3))

(Empty (Intersect (Var (Cross E*1)) (Bound E3))) (Empty (Intersect (Bound (Cross E*1)) (Var E3))))

(Clause (Ref (Nest (Cross E*1) E3) (Cross E3 E*1))) (Ref E3 (Filter E3)) (Empty (Intersect (Var (Cross E*1)) (Bound E3))) (Empty (Intersect (Bound (Cross E*1)) (Var E3)))))

38. modus ponens 36 and 37

(Clause

(Ref (Nest (Nest (Cross E*1) E3)

(Nest E2 (Nest (Cross E*2 E*3) E4))) (Nest (Cross E3 E*1)

(Nest E2 (Nest (Cross E*2 E*3) E4))))

(Ref E3 (Filter E3)) (Empty (Intersect (Var (Cross E*1)) (Bound E3))) (Empty (Intersect (Bound (Cross E*1)) (Var E3))))

39. substitution of 24 by { E1/(Nest (Cross E*1) (Nest E2 (Nest (Cross E*2 E3 E*3) E4))), E2/(Nest (Cross E3 E*1) (Nest E2 (Nest (Cross E*2 E*3) E4))), E3/(Nest (Nest (Cross E*1) E3) (Nest E2 (Nest (Cross E*2 E*3) E4))), R*1/R_{1} R_{2} R_{3} R_{4} R_{5} } (Clause

(Clause

(Ref (Nest (Cross E*1)

(Nest E2 (Nest (Cross E*2 E3 E*3) E4))) (Nest (Cross E3 E*1)

(Nest E2 (Nest (Cross E*2 E*3) E4))))

(Ref E3 (Filter E3)) (Empty (Intersect (Var E2) (Bound E3))) (Empty (Intersect (Bound E2) (Var E3))) (Empty (Intersect (Var (Cross E*1)) (Bound E3))) (Empty (Intersect (Bound (Cross E*1)) (Var E3))))

(Clause

(Ref (Nest (Cross E*1)

(Nest E2 (Nest (Cross E*2 E3 E*3) E4))) (Nest (Nest (Cross E*1) E3)

(Nest E2 (Nest (Cross E*2 E*3) E4))))

(Ref E3 (Filter E3)) (Empty (Intersect (Var E2) (Bound E3))) (Empty (Intersect (Bound E2) (Var E3))) (Empty (Intersect (Var (Cross E*1)) (Bound E3))) (Empty (Intersect (Bound (Cross E*1)) (Var E3))))

(Clause

(Ref (Nest (Nest (Cross E*1) E3)

(Nest E2 (Nest (Cross E*2 E*3) E4))) (Nest (Cross E3 E*1)

(Nest E2 (Nest (Cross E*2 E*3) E4))))

(Ref E3 (Filter E3)) (Empty (Intersect (Var E2) (Bound E3))) (Empty (Intersect (Bound E2) (Var E3))) (Empty (Intersect (Var (Cross E*1)) (Bound E3))) (Empty (Intersect (Bound (Cross E*1)) (Var E3)))))

40. modus ponens 34, 38 and 39

(Clause

(Ref (Nest (Cross E*1)

(Nest E2 (Nest (Cross E*2 E3 E*3) E4))) (Nest (Cross E3 E*1)

(Nest E2 (Nest (Cross E*2 E*3) E4))))

(Ref E3 (Filter E3)) (Empty (Intersect (Var E2) (Bound E3))) (Empty (Intersect (Bound E2) (Var E3))) (Empty (Intersect (Var (Cross E*1)) (Bound E3))) (Empty (Intersect (Bound (Cross E*1)) (Var E3))))

41. substitution of 21 by { E2/(Nest (Cross E*1) (Nest E2 (Nest (Cross E*2 E3 E*3) E4))), E3/E1, E4/(Nest (Cross E3 E*1) (Nest E2 (Nest (Cross E*2 E*3) E4))), R*1/R_{1} R_{2} R_{3} R_{4} R_{5} } (Clause

(Clause

(Ref (Nest E1

(Nest (Cross E*1) (Nest E2

(Nest (Cross E*2 E3 E*3) E4))))

(Nest E1

(Nest (Cross E3 E*1)

(Nest E2 (Nest (Cross E*2 E*3) E4)))))

(Ref E3 (Filter E3)) (Empty (Intersect (Var E2) (Bound E3))) (Empty (Intersect (Bound E2) (Var E3))) (Empty (Intersect (Var (Cross E*1)) (Bound E3))) (Empty (Intersect (Bound (Cross E*1)) (Var E3))))

(Clause

(Ref (Nest (Cross E*1)

(Nest E2 (Nest (Cross E*2 E3 E*3) E4))) (Nest (Cross E3 E*1)

(Nest E2 (Nest (Cross E*2 E*3) E4))))

(Ref E3 (Filter E3)) (Empty (Intersect (Var E2) (Bound E3))) (Empty (Intersect (Bound E2) (Var E3))) (Empty (Intersect (Var (Cross E*1)) (Bound E3))) (Empty (Intersect (Bound (Cross E*1)) (Var E3)))))

42. modus ponens 40 and 41

(Clause

(Ref (Nest E1

(Nest (Cross E*1) (Nest E2

(Nest (Cross E*2 E3 E*3) E4))))

(Nest E1

(Nest (Cross E3 E*1)

(Nest E2 (Nest (Cross E*2 E*3) E4)))))

(Ref E3 (Filter E3)) (Empty (Intersect (Var E2) (Bound E3))) (Empty (Intersect (Bound E2) (Var E3))) (Empty (Intersect (Var (Cross E*1)) (Bound E1))) (Empty (Intersect (Bound (Cross E*1)) (Var E1))))

6 Conclusion

It is generally accepted that rule-based query optimization is a more flexible approach to supporting high-level query languages. However, current practice involves very limited consideration of the issue of rule validity (or correctness). Consequently, the reliability of rule-based query optimization will tend to diminish as both the expressiveness of query languages and complexity of the underlying data models increase.

In the Advanced Database Systems Laboratory at our institution, with the desire of increasing the expressive power of query languages and with the need of coping with the complex objects, a wide-spectrum query algebra and a refinement calculus over it was proposed [CW93]. In this essay, based on the calculus, I look into the issue of the analysis of the correctness of query rewrite rules for rule-based query optimizers.

In my work, I extended the calculus to better express query rewrite rules, proved additional basic axioms for the calculus in its model theory, and exhibited a derivation of a real-world query rewrite rule in its proof theory. Most significantly, we learned from this work:

(1) that our original informal understanding of the intentions underlying the rule was incorrect,

(2) that our first few attempts at a formal specification of this rule were not valid,

(3) that proofs in the model theory are sometimes needed for basic axioms (but that knowledge of existing axioms can simplify this),

(4) that there is reasonable prospect that the proof theory will suffice to establish the correctness of the real-world query rewrite rules, and (5) that the nature of our derivations in the proof theory suggests that the process

can be automated.

Future directions in this line of research include:

(1) establishing correctness for the remaining rewrite rules that comprises the rule-

based query optimizer in our research database system, and

(2) further extending and refining the algebra and the calculus to facilitate ex-

pressing other queries and rewrite rules.

In regard to the first direction, we anticipate that completing this process will

produce a base set of axioms that are likely to be sufficient for deriving rewrite rules

used in other existing and future query optimizers.

In regard to the second direction, the following shows an example: by introducing

a new syntactic constraint “(Pred E*)” with the semantics that a database is a model

for it if and only if each query in E* is a predicate, the real-world rewrite rule (refer

to Table 1) would be translated to a more readable (albeit less general) form:

(Clause (Ref

(Nest E1

(Nest (Cross E*1)

(Nest E2 (Nest (Cross E*2 E3 E*3) E4)))) (Nest E1

(Nest (Cross E3 E*1)

(Nest E2 (Nest (Cross E*2 E*3) E4))))) (Pred E*1) (Pred E3) (Empty (Intersect (Bound E2) (Var E3))

References

[ABD^{+}89] M. Atkinson, F. Bancilhon, D. DeWitt, K. Dittrich, D. Maier, and S. Zdonik. The object-oriented database system manifesto. In Proceedings of the First International Conference on Deductive and Object-Oriented Databases, December 1989.

[Bee89] C. Beeri. Formal models for object-oriented databases. In Proceedings of the First International Conference on Deductive aand Object-Oriented Databases, December 1989.

[BG92] Ludger Becker and Ralf Hartmut Guting. Rule-based optimization and query processing in an extensible geometric database system. ACM Transactions on Database Systems, 17(2), June 1992.

[CW93] Neil Coburn and Grant E. Weddell. A logic for rule-based query optimization in graph-based data model. In Proceedings of the Third International Conference on Deductive aand Object-Oriented Databases, 1993.

[Day89] U. Dayal. Queries and views in an object-oriented data model. In Proceedings of the Second International Workshop on Database Programming Languages, June 1989.

[FG86] J. C. Freytag and N. Goodman. Rule-based translation of relational queries into iterative programs. In Proceedings of ACM SIGMOD International Conference on Management of Data, 1986.

[FG91] Béatrice Finance and Georges Gardarin. A rule-based query rewriter in an extensible dbms. In IEEE Conference on Data Engineering, 1991.

[Fre87] J. C. Freytag. A rule-based view of query optimization. In Proceedings of ACM SIGMOD International Conference on Management of Data, 1987.

[GD87] Goetz Graefe and David J. DeWitt. The exodus optimizer generator. In Proceedings of ACM SIGMOD International Conference on Management of Data, 1987.

[GM93] Goetz Graefe and William J. McKenna. The volcano optimizer generator: Extensibility and efficient search. In IEEE Conference on Data Engineering, 1993.

[GPvG90] M. Gyssens, J. Paredaens, and D. van Gucht. A graph-oriented object database model. In Proceeding of the Third ACM Symposium on Principles of Database Systems, 1990.

[PHH92] Hamid Pirahesh, Joseph M. Hellerstein, and Waqar Hasan. Extensible/rule based query rewrite optimization in starburst. In Proceedings of ACM SIGMOD International Conference on Management of Data, 1992.