Termination analysis for functional programs using term orderings
- 1 January 1995
- book chapter
- conference paper
- Published by Springer Science and Business Media LLC in Lecture Notes in Computer Science
- p. 154-171
- https://doi.org/10.1007/3-540-60360-3_38
Abstract
To prove the termination of a functional program there has to be a well-founded ordering such that the arguments in each recursive call are smaller than the corresponding inputs. In this paper we present a procedure for automated termination proofs of functional programs. In contrast to previously presented methods a suited well-founded ordering does not have to be fixed in advance by the user, but can be synthesized automatically. For that purpose we use approaches developed in the area of term rewriting systems for the automated generation of suited well-founded term orderings. But unfortunately term orderings cannot be directly used for termination proofs of functional programs which call other algorithms in the arguments of their recursive calls. The reason is that while for the termination of term rewriting systems orderings between terms are needed, for functional programs we need orderings between objects of algebraic data types. Our method solves this problem and enables term orderings to be used for termination proofs of functional programs.Keywords
This publication has 19 references indexed in Scilit:
- Generating polynomial orderings for termination proofsLecture Notes in Computer Science, 1995
- Proving termination of (conditional) rewrite systemsActa Informatica, 1993
- Topics in terminationPublished by Springer Science and Business Media LLC ,1993
- Termination by completionApplicable Algebra in Engineering, Communication and Computing, 1990
- The OYSTER-CLAM systemPublished by Springer Science and Business Media LLC ,1990
- Termination of rewriting systems by polynomial interpretations and its implementationScience of Computer Programming, 1987
- Termination of rewritingJournal of Symbolic Computation, 1987
- The karlsruhe induction theorem proving systemPublished by Springer Science and Business Media LLC ,1986
- A procedure for automatically proving the termination of a set of rewrite rulesLecture Notes in Computer Science, 1985
- A note on simplification orderingsInformation Processing Letters, 1979