Exact computation sequences

Abstract

Exact computation sequences are sequences of the form

$$< L_0 ,A_0 > \mathop - \limits^{S_1 } > < L_1 ,A_1 > \mathop - \limits^{S_2 } > ...\mathop - \limits^{S_n } > < L_n ,\emptyset > ,$$

, where L₀ is a free algebra, A₀ is a set of conditional equations over L₀, S_i is a "step function", L _i =S _i (L _i −1), and A _i =S _i (A _i −1). Each step function is the top-down reduction extension of a set of confluent and noetherian rewrite rules. These sequences are used in solving the word problem for free algebras, since for any pair of terms t ₁,t ₂ in L,

$$t_1 = _{A_0 } t_2 iff S_n o...oS_1 \left( {t_1 } \right) = S_n o...oS_1 \left( {t_2 } \right).$$

We analyze properties of exact computation sequences such as: determining the relation between the sets <L _i−1 ,A _i−1 > and S _i , and the output pair <L _i ,A _i >, and we present criteria for choosing the equations E _i in <L _i −1,A _i −1> which are used to generate the reductions S _i . We also give examples showing how to construct exact computation sequences for several axiom systems by applying the properties and the criteria presented in the article.