We propose an unfold-fold transformation system which preserves left termination for definite programs besides its declarative semantics. The system extends our previous proposal in [BCE95] by allowing to switch the atoms in the clause bodies when a specific applicability condition is satisfied. The applicability condition is very simple to verify, yet very common in practice. We also discuss how to verify such condition by exploiting mode information.
|Title of host publication||Logic Programming Synthesis and Transformation (9th International Workshop, LOPSTR'99, Venezia, Italy, September 22-24, 1999, Selected Papers)|
|Publication status||Published - 2000|
|Name||Lecture Notes in Computer Science|