Logical query optimization by proof-tree transformation

AbstractFor certain sets of logical rules, one can demonstrate that for every proof tree there is another tree proving the same fact and having a special “normal” form and thereby establish several useful properties of programs. Such a demonstration can be carried out in two parts: first establish that some containment holds between pieces of proof trees, and then show that repeated application of a transformation based on this containment converts every proof tree to the normal form. In this paper, we explore the power of arguments based on such proof-tree transformations and show that they provide a general tool for program optimization. We develop techniques to demonstrate useful proof-tree containments and show how certain program properties can be tested by using these containments in normal-form arguments. We discuss two techniques for demonstrating proof-tree containments. One is to reduce the question to one of conjunctive-query containment. A more powerful method is to test whether one conjunctive query is contained in the infinite union of conjunctive queries formed by expanding a set of recursive rules. We then consider two applications of these techniques. First, we give tests for commutativity of linear rules. When linear rules commute, we can reduce the complexity of “counting” methods for query evaluation from exponential to polynomial; commutativity is also an important element of separability in the sense of Naughton. A second application is to test whether certain non-linear rules are equivalent to linear rules that are obtained from them in a natural way