Termination Preserving Problem in the Transformation of Applicative Programs

Program transformation is a promising area of software methodology.TheFolding/Unfolding method proposed by Burstall/Darlington is a simple and powerfultransformation method for applicative programs.The only operations used are folding andunfolding of function definitions and substitution using laws.The major drawback of thismethod is that only partial correctness of functions is preserved and termination may be lost.That is if function f_1 is transformed to f_n,the computation of f_n on an object x will reach thesame result of the computation of f_1 on x,provided the computation terminates.But there maybe objects x,on which the computation of f_1 terminates,but f_n does not.This problem has notbeen solved with satisfaction.The idea of “reductive measure” of functions and “redactive”transformation is put forward here to solve the problem.It has been proved that if function's“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 mostimportant thing is that the simplicity of the original method is fully preserved.Because with thehelp of FP algebraic laws,the new restriction is expressed completely syntatically.Namely,onlythe direction of using laws(algebraic equations)for substitution is restricted.