EFFICIENT EXECUTION IN A CLASS OF TERM REWRITING SYSTEMS.

The meaning of each statement in an algebraic specification language can be defined simply. The verification of a description in such a language can be treated in the same framework of the language itself. However, in general, there is no efficient method for implementing the language. In this paper, the authors introduce an algebraic specification language which is a subclass of strongly sequential term rewriting systems (TRSs for short) with constructors of HUET-LEVY, called completely sequential TRSs. For a TRS of this class, one can determine easily the needed radices of a given term. An efficient algorithm is presented for computing, for any substitution s of constants to variables of t, the constant normal form of s(t) in R, where R is a given completely sequential TRS and t is a given term with variables. In the algorithm, directed acyclic graph (dag) representation of terms allows one to avoid the repeated computation for identical terms. Computation is carried out only when it is necessary, and a straightforward dag copy is avoided. A method for compiling dags into programs which run efficiently is presented.