Some equivalent transformations of recursive programs based on their schematic properties (Q794422)

The paper presents a series of new transformations of recursive program schemes which preserve functional equivalence relation. They are considered to be a contribution into techniques useful for transformational development and synthesis of programs (that start usually with a recursive specification), optimization etc. All the presented transformations are based on such semantical properties of fragments of recursive programs that are independent of a particular interpretation \({\mathcal I}\) of the used operations (or, in other words, basic functions) and are revealed automatically by global flow analysis of programs. This is both alternative and supplement to Burstall- Darlington fold-unfold technique which uses only properties given by rewriting rules that form a fixed part of transformation system and are to be presented by a man. Fragments whose properties are analyzed and to which transformations are locally applied, are occurrences of terms in a scheme, properties, defined in the paper by induction on term's structure, include: 1) a variable \(x\) affects predicate checks during the course of computation of a given term \(\tau\) on some \({\mathcal I}\); 2) whenever computation of a \(\tau\) terminates, its value equals the value of \(t\), where given term \(t\) does not contain calls to defined functions (plus some variations of these property); 3) for given \(\tau\), if its computation on some \({\mathcal I}\) does not terminate then computation of a term \(\sigma\) on \({\mathcal I}\) also does not terminate. These properties may be useful not for transformations only, but also for proving various assertions about programs. Complexity of searching terms with these properties can vary from polynomial to exponential, depending on degree of completeness of the search. Six equivalent transformations are presented, including substitution of a term by term without calls, various commutations of basic and defined functions, elimination of recursion over ''almost'' invariant arguments, elimination of useless test. They are shown to allow significant simplification of a recursive program structure.