Abstract
As typed logic programming becomes more mainstream, system building tools like partial deduction systems will need to be mapped from untyped languages to typed ones. It is important, however, when mapping techniques across that the new techniques should exploit the type system as much as possible. In this paper, we show how norms, which play a crucial role in termination analysis, can be generated from the prescribed types of a logic program. Interestingly, the types highlight restrictions of earlier norms and suggest how these norms can be extended to obtain some very general and powerful notions of norm which can be used to measure any term in an almost arbitrary way. We see our work on norm derivation as a contribution to the termination analysis of typed logic programs which, in particular, forms an essential part of offline partial deduction systems.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
K.R. Apt and D. Pedreschi. Studies in pure Prolog: Termination. In Proceedings Esprit symposium on computational logic, pages 150–176, Brussels, November 1990. Springer-Verlag.
F. Benoy and A. King. Inferring argument size relations with CLP(\(\mathcal{R}\)). In LOP-STR'96. Springer-Verlag, 1996.
M. Bezem. Characterizing termination of logic programs with level mappings. In Ewing L. Lusk and Ross A. Overbeek, editors, Proceedings of the North American Conference on Logic Programming, pages 69–80, Cleveland, Ohio, USA, 1989.
A. Bossi, N. Cocco, and M. Fabris. Typed norms. In ESOP'92, pages 73–92, 1992.
A. Bossi, N. Cocco, and M. Fabris. Norms on terms and their use in proving universal termination of a logic program. Theoretical Computer Science, 124:297–328, 1994.
S. Decorte, D. de Schreye, and M. Fabris. Automatic inference of norms: A missing link in automatic termination analysis. In ILPS'93, pages 420–436, 1993.
S. Decorte, D. de Schreye, and M. Fabris. Exploiting the power of typed norms in automatic inference of interargument relations. Technical report, Dept. computer science, K.U.Leuven, 1994.
J. Gallagher and A. de Waal. Fast and precise regular approximations of logic programs. In ICLP'94, pages 599–613, 1994.
C. Gurr. A Self-Applicable Partial Evaluator for the Logic Programming Language Gödel. PhD thesis, University of Bristol, January 1994.
C. Gurr. Personal communication on the literature on termination analyses. September 1995.
P. M. Hill and J. W. Lloyd. The Gödel Programming Language. MIT Press, 1994.
G. Janssens and M. Bruynooghe. Deriving descriptions of possible values of program variables by means of abstract interpretation. J. Logic Programming, 13:205–258, 1992.
L. Plümer. Termination Proofs for Logic Programs. Springer-Verlag, 1990.
P. Van Hentenryck, A. Cortesi, and B. Le Charlier. Type Analysis of Prolog Using Type Graphs. In PLDI'94, pages 337–348. ACM Press, 1994.
P. Van Roy. A Prolog Compiler for the PLM. Master's thesis, Computer Science Division, University of California, Berkeley, 1984.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Martin, J.C., King, A., Soper, P. (1997). Typed norms for typed logic programs. In: Gallagher, J. (eds) Logic Program Synthesis and Transformation. LOPSTR 1996. Lecture Notes in Computer Science, vol 1207. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-62718-9_13
Download citation
DOI: https://doi.org/10.1007/3-540-62718-9_13
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-62718-0
Online ISBN: 978-3-540-68494-7
eBook Packages: Springer Book Archive