Inverse Unfold Problem and Its Heuristic Solving

ABSTRACT. Unfold/fold transformations have been widely studied in various programming paradigms and are used in program transformations, theorem proving, and so on. In this paper, by using an example, we show that finding the inverse of one-step unfolding is not easy, i.e., a challenging task. We formalize this problem by regarding one-step program transformation as a relation. Focusing unfolding on pure-constructor systems whose class is a subclass of conditional term rewriting systems, we discuss some correctness issue of the inverse problem of one-step unfolding. We propose a heuristic procedure to solve the problem, and show its successful examples. We improve the procedure, and show examples for which the improvement takes effect.