Termination preserving problem in the transformation of applicative programs

Abstract

Program transformation is a promising area of software methodology. The Folding/Unfolding method proposed by Burstall/Darlington is a simple and powerful transformation method for applicative programs. The only operations used are folding and unfolding of function definitions and substitution using laws. The major drawback of this method is that only partial correctness of functions is preserved and termination may be lost. That is if functionf ₁ is transformed tof _n , the computation off _n on an objectx will reach the same result of the computation off ₁ onx, provided the computation terminates. But there may be objectsx, on which the computation off ₁ terminates, butf _n does not. This problem has not been solved with satisfaction. The idea of “reductive measure” of functions and “reductive” transformation is put forward here to solve the problem. It has been proved that if functions “complexity” is not increased under some reductive measure in the transformation process, termination will be preserved. The termination problem is thus solved to some extent. The most important thing is that the simplicity of the original method is fully preserved. Because with the help of FP algebraic laws, the new restriction is expressed completely syntatically. Namely, only the direction of using laws (algebraic equations) for substitution is restricted.