A Folding Rule for Eliminating Existential Variables from Constraint Logic Programs

• Autorzy: Senni V. , Pettorossi A. , Proietti M.
• Języki publikacji: EN

Abstrakty

EN

The existential variables of a clause in a constraint logic program are the variables which occur in the body of the clause and not in its head. The elimination of these variables is a transformation technique which is often used for improving program efficiency and verifying program properties. We consider a folding transformation rule which ensures the elimination of existential variables and we propose an algorithm for applying this rule in the case where the constraints are linear inequations over rational or real numbers. The algorithm combines techniques for matching terms modulo equational theories and techniques for solving systems of linear inequations. Through some examples we show that an implementation of our folding algorithm has a good performance in practice.

Słowa kluczowe

EN

program transformation; folding rule; variable elimination; constraint logic programming (CLP)

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2009
• Tom: Vol. 96, nr 3
• Strony: 373--393
• Opis fizyczny: Bibliogr. 22 poz., tab.

Twórcy

autor

Senni V.

autor

Pettorossi A.

autor

Proietti M.

• DISP, University of Rome "Tor Vergata", Via del Politecnico 1, 00133 Rome, Italy,

Bibliografia

• [1] Baader, F., Snyder, W.: Unification Theory, in: Handbook of Automated Reasoning (A. Robinson, A. Voronkov, Eds.), vol. I, Elsevier Science, 2001, 445-532.
• [2] Benanav, D., Kapur, D., Narendran, P.: Complexity ofmatching problems, Journal of Symbolic Computation, 3(1-2), 1987, 203-216.
• [3] Bensaou, N., Guessarian, I.: Transforming Constraint Logic Programs, Theoretical Computer Science, 206, 1998, 81-125.
• [4] Bürckert, H.-J.: Some Relationships between Unification, Restricted Unification, andMatching, Proceedings of the 8th International Conference on Automated Deduction, 230, Springer-Verlag, London, UK, 1986.
• [5] Burstall, R.M., Darlington, J.: A Transformation System for Developing Recursive Programs, Journal of the ACM, 24(1), January 1977, 44-67.
• [6] Eker, S. M.: Improving the efficiency of AC matching and unification, RR-2104, INRIA Lorraine & CRIN, Villers-les-Nancy, France, 1993.
• [7] Etalle, S., Gabbrielli, M.: Transformations of CLP Modules, Theoretical Computer Science, 166, 1996, 101-146.
• [8] Fioravanti, F., Pettorossi, A., Proietti, M.: Transformation Rules for Locally Stratified Constraint Logic Programs, Program Development in Computational Logic (K.-K. Lau, M. Bruynooghe, Eds.), Lecture Notes in Computer Science 3049, Springer, 2004.
• [9] Jaffar, J., Maher, M.: Constraint Logic Programming: A Survey, Journal of Logic Programming, 19/20, 1994, 503-581.
• [10] Lloyd, J. W.: Foundations of Logic Programming, Springer-Verlag, Berlin, 1987, Second Edition.
• [11] Maher, M. J.: A Transformation System for Deductive Database Modules with Perfect Model Semantics, Theoretical Computer Science, 110, 1993, 377-403.
• [12] The MAP Transformation System, 1995-2008, Available from http://www.iasi.cnr.it/∼proietti/system.html.
• [13] Pettorossi, A., Proietti, M., Senni, V.: Proving Properties of Constraint Logic Programs by Eliminating Existential Variables, in: Proceedings of the 22nd International Conference on Logic Programming, ICLP'06 (S. Etalle, M. Truszczyński, Eds.), Lecture Notes in Computer Science 4079, Springer, 2006, 179-195.
• [14] Proietti, M., Pettorossi, A.: Unfolding-Definition-Folding, in this Order, for Avoiding Unnecessary Variables in Logic Programs, Theoretical Computer Science, 142(1), 1995, 89-124.
• [15] Ringeissen, C.: Matching in a Class of Combined Non-disjoint Theories, Proceedings of the 19th International Conference on Automated Deduction, CADE-19 (F. Baader, Ed.), Lecture Notes in Computer Science 2741, Springer, 2003.
• [16] Schrijver, A.: Theory of Linear and Integer Programming, John Wiley & Sons, 1986.
• [17] Senni, V., Pettorossi, A., Proietti, M.: A Folding Algorithm for Eliminating Existential Variables from Constraint Logic Programs, in: Proceedings of the 24th International Conference on Logic Programming, ICLP'08 (M. Garcia de la Banda, E. Pontelli, Eds.), Lecture Notes in Computer Science 5366, Springer, 2008, 284-300.
• [18] V. Senni, A. Pettorossi, and M. Proietti. A folding rule for eliminating existential variables from constraint logic programs. Technical Report 08-03, IASI-CNR, Rome, Italy, 2008. Available from: http://www.iasi.cnr.it/~proietti/reports.html.
• [19] H. Seki. Unfold/fold transformation of stratified programs. Theoretical Computer Science, 86:107-139, 1991.
• [20] Tamaki, H., Sato, T.: Unfold/Fold Transformation of Logic Programs, Proceedings of the Second International Conference on Logic Programming, ICLP'84 (S.-°A. Tärnlund, Ed.), Uppsala University, Uppsala, Sweden, 1984.
• [21] Terese: Term Rewriting Systems, Cambridge University Press, 2003.
• [22] Weispfenning, V.: The complexity of linear problems in fields, Journal of Symbolic Computation, 5(1-2), 1988, 3-27.