Abstract
In this paper, we present a syntax-directed termination and reduction checker for higher-order logic programs. The reduction checker verifies parametric higher-order subterm orderings describing relations between input and output of well-moded predicates. These reduction constraints are exploited during termination checking to infer that a specified termination order holds. To reason about parametric higher-order subterm orderings, we introduce a deductive system as a logical foundation for proving termination. This allows the study of proof-theoretical properties, such as consistency, local soundness and completeness and decidability. We concentrate here on proving consistency of the presented inference system. The termination and reduction checker are implemented as part of the Twelf system and enable us to verify proofs by complete induction.
Acknowledgements
The author gratefully acknowledges numerous fruitful discussions with Frank Pfenning regarding the subject of this paper. His guidance and careful reading of this paper contributed greatly to its clarity and correctness.
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
Thomas Arts and Jürgen Giesl. Termination of term rewriting using dependency pairs. Theoretical Computer Science, 236:133–178, 2000.
John Hannan and Frank Pfenning. Compiler verification in LF. In Andre Scedrov, editor, Seventh Annual IEEE Symposium on Logic in Computer Science, pages 407–418, Santa Cruz, California, June 1992.
Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. Journal of the Association for Computing Machinery, 40(1):143–184, January 1993.
J.-P. Jouannaud and A. Rubio. The higher-order recursive path ordering. In G. Longo, editor, Proceedings of the 14th Annual Symposium on Logic in Computer Science (LICS’99), pages 402–411, Trento, Italy, July 1999. IEEE Computer Society Press.
Olav Lysne and Javier Piris. A termination ordering for higher order rewrite systems. In Jieh Hsiang, editor, Proceedings of the Sixth International Conference on Rewriting Techniques and Applications, pages 26–40, Kaiserslautern, Germany, April 1995. Springer-Verlag LNCS 914.
Frank Pfenning. Structural cut elimination. In D. Kozen, editor, Proceedings of the Tenth Annual Symposium on Logic in Computer Science, pages 156–166, San Diego, California, June 1995. IEEE Computer Society Press.
Frank Pfenning. Computation and Deduction. Cambridge University Press, 2000. In preparation. Draft from April 1997 available electronically.
Frank Pfenning and Carsten Schürmann. System description: Twelf — a metalogical framework for deductive systems. In H. Ganzinger, editor, Proceedings of the 16th International Conference on Automated Deduction (CADE-16), pages 202–206, Trento, Italy, July 1999. Springer-Verlag LNAI 1632.
Brigitte Pientka. Termination and reduction checking in the logical framework. Technical report cmu-cs-01-115, Carnegie Mellon University, 2001.
Lutz Plümer. Termination Proofs for Logic Programs. LNAI 446. Springer-Verlag, 1990.
Ekkehard Rohwedder and Frank Pfenning. Mode and termination checking for higher-order logic programs. In Hanne Riis Nielson, editor, Proceedings of the European Symposium on Programming, pages 296–310, Linköping, Sweden, April 1996. Springer-Verlag LNCS 1058.
J. van de Pol and H. Schwichtenberg. Strict functionals for termination proofs. In M. Dezani-Ciancaglini and G. Plotkin, editors, Proceedings of the International Conference on Typed Lambda Calculi and Applications, pages 350–364, Edinburgh, Scotland, April 1995. Springer-Verlag LNCS 902.
Femke van Raamsdonk. Higher-order rewriting. In Proceedings of the 10th International Conference on Rewriting Techniques and Applications (RTA’ 99), pages 220–239, Trento, Italy, July 1999. Springer-Verlag LNCS 1631.
Roberto Virga. Higher-Order Rewriting with Dependent Types. PhD thesis, Department of Mathematical Sciences, Carnegie Mellon University, 2000.
Christoph Walther. On proving the termination of algorithms by machine. Artificial Intelligence, 71(1), 1994.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Pientka, B. (2001). Termination and Reduction Checking for Higher-Order Logic Programs. In: Goré, R., Leitsch, A., Nipkow, T. (eds) Automated Reasoning. IJCAR 2001. Lecture Notes in Computer Science, vol 2083. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45744-5_32
Download citation
DOI: https://doi.org/10.1007/3-540-45744-5_32
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42254-9
Online ISBN: 978-3-540-45744-2
eBook Packages: Springer Book Archive