Abstract
Given a program P, an unfold/fold program transformation system derives a sequence of programs P = P 0, P 1, ..., P n , such that P i + 1 is derived from P i by application of either an unfolding or a folding step. Existing unfold/fold transformation systems for definite logic programs differ from one another mainly in the kind of folding transformations they permit at each step. Some allow folding using a single (possibly recursive) clause while others permit folding using multiple non-recursive clauses. However, none allow folding using multiple recursive clauses that are drawn from some previous program in the transformation sequence. In this paper we develop a parameterized framework for unfold/fold transformations by suitably abstracting and extending the proofs of existing transformation systems. Various existing unfold/fold transformation systems can be obtained by instantiating the parameters of the framework. This framework enables us to not only understand the relative strengths and limitations of these systems but also construct new transformation systems. Specifically we present a more general transformation system that permits folding using multiple recursive clauses that can be drawn from any previous program in the transformation sequence. This new transformation system is also obtained by instantiating our parameterized framework.
The work of Abhik Roychoudhury, C.R. Ramakrishnan and I.V. Ramakrishnan was partially supported by NSF grants CCR-9711386 and EIA-9705998. The work of K. Narayan Kumar was partially supported by NSF grant CDA-9805735.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Aravindan, C., Dung, P.M.: On the correctness of unfold/fold transformations of normal and extended logic programs. Journal of Logic Programming, 295–322 (1995)
Bossi, A., Cocco, N., Dulli, S.: A method of specializing logic programs. ACM TOPLAS, 253–302 (1990)
Boulanger, D., Bruynooghe, M.: Deriving unfold/fold transformations of logic programs using extended OLDT-based abstract interpretation. Journal of Symbolic Computation, 495–521 (1993)
Cui, B., Dong, Y., Du, X., Narayan Kumar, K., Ramakrishnan, C.R., Ramakr, I.V.: Logic programming and model checking. In: Palamidessi, C., Meinke, K., Glaser, H. (eds.) ALP 1998 and PLILP 1998. LNCS, vol. 1490, pp. 1–20. Springer, Heidelberg (1998)
Etalle, S., Gabrielli, M., Meo, M.C.: Unfold/fold transformations of CCP programs. In: Proceedings of CONCUR (1998)
Francesco, N.D., Santone, A.: A transformation system for concurrent processes. Acta Informatica 35(12), 1037–1073 (1998)
Gergatsoulis, M., Katzouraki, M.: Unfold/fold transformations for definite clause programs. In: Penjam, J. (ed.) PLILP 1994. LNCS, vol. 844, Springer, Heidelberg (1994)
Kanamori, T., Fujita, H.: Unfold/fold transformation of logic programs with counters. USA-Japan Seminar on Logics of Programs (1987)
Lloyd, J.W.: Foundations of Logic Programming, 2nd edn. Springer, Heidelberg (1993)
Maher, M.J.: Correctness of a logic program transformation system. Technical report, IBM T.J. Watson Research Center (1987)
Pettorossi, A., Proietti, M. (eds.): Transformation of logic programs. Handbook of Logic in Artificial Intelligence, vol. 5, pp. 697–787. Oxford University Press, Oxford (1998)
Pettorossi, A., Proietti, M., Renault, S.: Reducing nondeterminism while specializing logic programs. Proceedings of POPL, 414–427 (1997)
Roychoudhury, A., Narayan Kumar, K., Ramakrishnan, C.R., Ramakrishnan, I.V.: A generalized unfold/fold transformation system for definite logic programs. Technical Report 98/37, Dept. of Computer Science, SUNY Stony Brook (1998)
Roychoudhury, A., Narayan Kumar, K., Ramakrishnan, C.R., Ramakrishnan, I.V.: Proofs by program transformations. Accepted for LOPSTR (1999)
Roychoudhury, A., Narayan Kumar, K., Ramakrishnan, I.V.: Beyond TamakiSato style unfold/fold transformations for normal logic programs. Technical Report 99/21, Dept. of Computer Science, SUNY Stony Brook (1999)
Roychoudhury, A., Ramakrishnan, C.R., Ramakrishnan, I.V., Smolka, S.A.: Tabulation based Induction proofs with applications to Automated Verification. In: Workshop on Tabulation in Parsing and Deduction, pp. 83–88 (1998)
Sands, D.: Total correctness by local improvement in the transformation of functional programs. ACM TOPLAS 18(2), 175–234 (1996)
Seki, H.: Unfold/fold transformation of stratified programs. Theoretical Computer Science, 107–139 (1991)
Seki, H.: Unfold/fold transformation of general logic programs for well-founded semantics. Journal of Logic Programming, 5–23 (1993)
Tamaki, H., Sato, T.: Unfold/fold transformations of logic programs. In: Proceedings of International Conference on Logic Programming, pp. 127–138 (1984)
Tamaki, H., Sato, T.: A generalized correctness proof of the unfold/ fold logic program transformation. Technical report, Ibaraki University, Japan (1986)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Roychoudhury, A., Kumar, K.N., Ramakrishnan, C.R., Ramakrishnan, I.V. (1999). A Parameterized Unfold/Fold Transformation Framework for Definite Logic Programs. In: Nadathur, G. (eds) Principles and Practice of Declarative Programming. PPDP 1999. Lecture Notes in Computer Science, vol 1702. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10704567_24
Download citation
DOI: https://doi.org/10.1007/10704567_24
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66540-3
Online ISBN: 978-3-540-48164-5
eBook Packages: Springer Book Archive