Correctness of Logic Program Transformations Based on Existential Termination

Kung-Kiu Lau
Department of Computer Science, University of Manchester
Oxford Road, Manchester M13 9PL, United Kingdom
kung-kiu@cs.man.ac.uk

Mario Ornaghi
Dipartimento di Scienze dell'Informazione
Universita degli Studi di Milano
Via Comelico 39/41, Milano, Italy
ornaghi@dsi.unimi.it

Alberto Pettorossi
Department of Electronic Engineering, University of Roma Tor Vergata
Via della Ricerca Scientifica, 00133 Roma, Italy
adp@iasi.rm.cnr.it

Maurizio Proietti
IASI-CNR,
Viale Manzoni 30, 00185 Roma, Italy
proietti@iasi.rm.cnr.it

Abstract:
We study the relationships between the correctness of logic program
transformation and program termination. We consider definite programs
and we identify some `invariants' of the program transformation
process. The validity of these invariants ensures the preservation of
the success set semantics, provided that the existential termination
of the initial program implies the existential termination of the final program.
We also identify invariants for the preservation of the finite failure
set semantics.

We consider four very general transformation rules: definition introduction,
definition elimination, iff-replacement, and finite failure. Many
versions of the transformation rules proposed in the literature,
including unfolding, folding, and goal replacement, are instances of
the iff-replacement rule.

By using our proposed invariants which are based on Clark completion,
we prove, for our transformation rules, various results concerning the
preservation of both the success set and finite failure set semantics.
By exploiting some powerful properties of the Clark completion, we are
able to derive simple proofs of these  preservation results. These
proofs are much simpler than those done by induction on the
construction of the SLD-trees, like the ones proposed in the
literature for related results.