Abstract
In this paper semi-linear norms, a class of functions to weight the terms occurring in a program, are defined and studied. All the functions in this class have the nice property of allowing a syntactical characterization of rigid terms, that is terms whose weight does not change under substitution. Based on these norms, a general proof method for termination of pure Prolog programs can be adapted to deal with a large class of programs in a simple way. The simplified method requires pre/post specifications well-behaved with respect to substitutions, quite a general case in practice, and ordering functions not increasing with respect to substitutions, which can be based on semi-linear norms, to be associated to program predicates. A few examples of this simplified proof method are given.
This work has been partially supported by "Progetto Finalizzato Sistemi Informatici e Calcolo Parallelo" of CNR under Grant n. 89.00026.69
Chapter PDF
Similar content being viewed by others
References
Apt K.R., Bol R.N., Klop J.W., On the safe termination of prolog programs, Proc. ICLP'89, MIT Press, (1989).
Apt K.R., Pedreschi D., Studies in Pure Prolog: Termination, Proc. Symp. on Computational Logic, LNCS (1990).
Baudinet M., Proving Termination Properties of Prolog Programs: A Semantic Approach, Proc. IEEE Symp. on Logic in Computer Science, pp. 336–347 (1988).
Bezem M., Characterizing Termination of Logic Programs, Proc. NACLP'89, pp. 69–80 (1989).
Berge C., Graphs and Hypergraphs, North-Holland Mathematical Library, North-Holland, 1973.
Bossi A., Cocco N., Verifying Correctness of Logic Programs, Proc. TAPSOFT'89, Vol. 2, Springer-Verlag, pp. 96–110 (1989).
Bossi A., Cocco N., Fabris M., Norms on Terms and Their Use in Proving Universal Termination of Logic Programs, C.N.R. Technical Report on Project "Sistemi Informatici e Calcolo Parallelo" (1991).
K.L. Clark, S. Tarnlund, A first order theory of data and programs, Proc. IFIP 77, pp. 939–944 (1977).
Deville Y., Logic Programming. Systematic Program Development, Int. Series in Logic Programming, Addison-Wesley, 1990.
Dijkstra E.W., A Discipline of Programming, Prentice-Hall, 1976.
Drabent W., Maluszynski J., Inductive Assertion Method for Logic Programs, Theoretical Computer Science, 59, pp. 133–155 (1988).
Fabris M., Sulla Terminazione dei Programmi Logici, tesi di laurea, Dip. di Matematica Pura e Applicata, Università di Padova (1990).
Floyd R.M., Assigning meaning to programs, Proc. AMS Symp. on Applied Mathematics, Amer. Math. Soc., pp. 19–31 (1967).
Frances N., Grumberg O., Katz S., Pnueli A., Proving Termination of Prolog Programs, Proc. Logics of Programs Conf., LNCS 193, pp. 89–105 (1985).
Gries D., The Science of Programming, Springer-Verlag, 1981.
Hoare C.A.R., An axiomatic approach to computer programming, Comm. ACM 12, pp. 576–580, 583 (1969).
Hogger C. J., Introduction to Logic Programming, Academic Press, 1984.
J. W. Lloyd, Foundations of Logic Programming, Springer-Verlag, second edition 1987.
Plümer L., Termination Proofs for Logic Programs based on Predicate Inequalities, Proc. ICLP'90, pp. 634–648 (1990).
Plümer L., Termination Proofs for Logic Programs, Lecture Notes in Artificial intelligence 446, Springer-Verlag, 1990.
Ullman J.D., Van Gelder A., Efficient Tests for Top-Down Termination of Logical Rules, JACM, Vol. 35, No. 2, pp. 345–373 (1988).
Vasak T., Potter J., Characterisation of Terminating Logic Programs, Int. Symp. on Logic Programming '86, IEEE, pp. 140–147 (1986).
Wang B., Shryamasunder R.K., Proving Termination of Logic Programs, Internal Report, CS Dept., Penn State University (1989).
Wang B., Shryamasunder R.K., Towards a Characterization of Termination of Logic Programs, Proc. II Int. Workshop on Programming Language Implementation and Logic Programming '90, LNCS 456, pp. 204–221 (1990).
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1991 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bossi, A., Cocco, N., Fabris, M. (1991). Proving termination of logic programs by exploiting term properties. In: Abramsky, S., Maibaum, T.S.E. (eds) TAPSOFT '91. TAPSOFT 1991. Lecture Notes in Computer Science, vol 494. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3540539816_66
Download citation
DOI: https://doi.org/10.1007/3540539816_66
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-53981-0
Online ISBN: 978-3-540-46499-0
eBook Packages: Springer Book Archive