next up previous contents
Next: Third Optimisation (OP3) Up: Stages of Translation Previous: Formal Definition of

Second Optimisation (OP2)


This transformation is intended to address a source of inefficiency that we have noted which is a consequence of the manipulation that is required in order to make variables range over relations rather than domains. Consider example query ``what is Fred's age'':

The TRC translation of this query appears to have more existentially quantified variables than we might expect. The translation of DRC table membership clauses always results in extra existentially quantified variables in the TRC expression. This is unavoidable. However, if we look at the TRC query, we see that the existentially quantified variable, x, which also occurred in the DRC expression has now become redundant. Any attributes associated with this variable are equated with attributes of the new existentially quantified variable. We ought therefore to be able to eliminate this redundant variable. It actually turns out that every TRC existentially quantified variable which originated from a DRC existentially quantified variable is redundant and can be optimised away. We perform this optimisation by translating the TRC expression into clausal form and applying the paramodulation inference rule (which substitutes one term for another which is equal to it) until the redundant variables have been eliminated. (Details of the conversion to clausal form and the paramodulation inference rule may be found in [Bundy, 1983].) Converting the TRC expression above into clausal form produces the clause set:

For the purposes of this example, Skolem constants have been formed by prefixing variable names with sk. We know that the variable x is redundant, so we now select a clause which equates some attribute of the Skolem constant associated with x to some other value, and then substitute this other value for all occurrences of the original. In the above example, if we choose the second clause we know we can replace all occurrences of skx.age with skt.age. Performing this substitution throughout reduces the clause set to

There are no further clauses containing the redundant variable, so we have now finished. Reconstructing the formula produces the simplified TRC expression:

which is what we would expect.

With the query ``Who works in a department that is on floor 2?'' we obtain the following TRC, which is optimised as shown:

which reduces to the following clause set:

We know that we will be able to optimise away the variable x (skolem constant skx), and we can do this by selecting the second of these clause and substituting for skx.dept throughout. This results in:

Reconstructing the TRC formula produces:

next up previous contents
Next: Third Optimisation (OP3) Up: Stages of Translation Previous: Formal Definition of

Chris Fox, September 1995