This paper describes some extensions of Tamaki-Sato's (1984) unfold/fold transformation of definite programs. We first propose unfold/fold rules also preserving the finite failure set (by SLD-resolution) of a definite program, which the original rules proposed by Tamaki and Sato do not. Then, we show that our unfold/fold rules can be extended to rules for stratified programs and prove that both the success set and the finite failure set (by SLDNF-resolution) of a stratified program are preserved. Preservation of equivalence of the perfect model semantics (Przymusinski (1988)) is also discussed. © 1991.
Seki, H. (1991). Unfold/fold transformation of stratified programs. Theoretical Computer Science, 86(1), 107–139. https://doi.org/10.1016/0304-3975(91)90007-O