Abstract
This paper presents an automated method that deals with termination of constraint logic programs in two steps. First, from the text of a program, the method infers a set of potentially terminating classes using abstract interpretation and boolean mu-calculus. By “potentially”, we roughly mean that for each of these classes, one can find a static order over the literals of the clauses of the program to ensure termination. Then, given a terminating class among those computed at the first step, the second step consists of a “compilation” (or transformation) of the original program to another one by reordering literals. For this new program, the universal left-termination of any query of the considered class is guaranteed. The method has been implemented.
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
K.R. Apt and D. Pedreschi. Reasoning about termination of pure Prolog programs. In Information and Computation, 106:1, pages 109–157, 1993.
M. Codish and C. Taboch. A semantic basis for termination analysis of logic programs and its realization using symbolic norm constraints. Proc. of the 6th ICALP, LNCS 1298, 1997.
S. Colin, F. Mesnard, and A. Rauzy. Constraint logic programming and mu-calculus. ERCIM/COMPULOG Workshop on Constraints, 1997. URL: http://www.univ-reunion.fr/~gcc
P. Cousot and R. Cousot. Abstract interpretation and application to logic programs. Journal of Logic Programming, 13:103–179, 1992.
D. De Schreye and S. Decorte. Termination of logic programs: the never-ending story. Journal of Logic Programming, 12:1–66, 1994.
M. Gabbrielli and G. Levi. Modelling answer constraints in constraint logic programs. In MIT Press, Proc. of ICLP’91, pages 238–252, 1991.
J. Jaffar and M.J. Maher. Constraint logic programming: a survey. Journal of Logic Programming, 19:503–581, 1994.
N. Lindenstrauss and Y. Sagiv. Automatic termination analysis of logic programs. In MIT Press, Proc. of the 14th ICLP, pages 63–77, 1997.
F. Mesnard. Inferring left-terminating classes of queries for constraint logic programs by means of approximations. In MIT Press, Proc. of JICSLP’96, pages 7–21, 1996.
K. Sohn and A. Van Gelder. Termination detection in logic programs using argument sizes. In ACM Press, Proc. of PODS’91, pages 216–226, 1991.
C. Speirs, Z. Somogyi, and H. Søndergaard. Termination analysis for Mercury. Proc. of SAS’97, LNCS 1302, 1997.
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
Hoarau, S., Mesnard, F. (1999). Inferring and Compiling Termination for Constraint Logic Programs. In: Flener, P. (eds) Logic-Based Program Synthesis and Transformation. LOPSTR 1998. Lecture Notes in Computer Science, vol 1559. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48958-4_13
Download citation
DOI: https://doi.org/10.1007/3-540-48958-4_13
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65765-1
Online ISBN: 978-3-540-48958-0
eBook Packages: Springer Book Archive