Computing with conditional rewrite rules

Abstract

We present a method for validating abstract data type specifications. The method takes as input a set of ground terms L0 and a set of conditional equations A0 over L0. The object of this method is to find a normal form function, Norm, for the pair 〈 L0, A0 〉. The function Norm is computed as a sequence of step functions S1, S2,.., Sn. Each step function Si, 0 ≤ i ≤ n, takes as input a pair 〈 Li−1, Ai−1 〉, where Li−1 is a set of ground terms and Ai is a set of conditional equations over the set of terms Li−1. At each step i, a set of equations Ei is selected from the set of theorems of the pair 〈 Li−1, Ai−1 〉. The set of equations Ei is transformed into a set of reductions Ri. The step function Si is defined as the top-down reduction extention of Ri to Li−1. The output of Si is the pair 〈 Li, Ai 〉, where Li is the set of normal forms of Li−1 under the set of reductions Ri and Ai is the set of normal forms of the equations in Ai−1 under the same set of reductions. This way, a theorem in the system 〈 Li−1, Ai−1 〉 becomes a theorem in the system 〈 Li, Ai 〉. The last step, Sn, has as output the pair 〈 Ln, φ 〉. The only theorems in 〈 Ln, φ 〉 are the identities. This way the sequence (Formula presented.) gives us a procedure to compute the normal form of the terms in 〈 L0, A0 〉. In this paper we present criteria for choosing the sets of equations Ei which simplify the pair 〈 Li−1, Ai−1 〉. We also present results that characterize the output set 〈 Li, Ai 〉 of Si as a function of the set 〈 Li−1, Ai−1 〉 and of the set of reductions Ri. If the sets of reductions Ri are confluent and terminating, then they can be combined, by using a priority system similar to the one developed by Baeten, Bergstra and Klop, to form a confluent and terminating set of reductions on the set 〈 L0, A0 〉.