Abstract
We present TEA, a tool that is able to detect termination of functions written in a non-strict high-level functional programming language like Haskell. Since almost every compiler for lazy functional languages transforms programs into a functional core language, we use such a core language as the source language for the analysis. TEA is able to detect two kinds of termination: nf-termination and lazy termination. Intuitively, nf-termination of f means that given arguments a i in normal form, the normal order evaluation of the expression f a 1 ... a n terminates with a normal form. If an expression evaluates to an infinite normal form, we will call it lazy terminating.
In order to prove nf-termination of an expression, TEA tries to generate a preclosed tableau using abstract reduction and path analysis. The preclosed tableau issues a set of ordering constraints, which have to be satisfied by some Noetherian ordering. A subsystem is called to generate this Noetherian ordering, and to verify that the set of ordering constraint is satisfied. In the case of success, this proves termination of the expression at the root of the tableau. Lazy termination is recognized using a specialized check on a preclosed tableau.
TEA performs the analysis automatically in reasonable time with a success rate of about 90 % for the functions of a real program script written in Haskell.
Preview
Unable to display preview. Download preview PDF.
References
T. Arts and J. Giesl. Automatically proving termination where simplification orderings fail. In Michel Bidoit & Max Dauchet, editor, Proceedings of the 7th International Joint Conference on Theory and Practice of Software Development (TAPSOFT '97), number 1214 in Lecture Notes in Computer Science, pages 261–272, Lille, Rance, 1997. Springer-Verlag.
S. Abramsky and C. L. Hankin, editors. Abstract Interpretation of Declarative Languages. Ellis Horwood, 1987.
P.H. Andersen and C.K. Holst. Termination analysis for ofline partial evaluation of a higher order functional language. In Static Analysis, third international symposium, volume 1145 of Lecture Notes in Computer Science, pages 67–82. Springer-Verlag, 1996.
R. S. Boyer and J S. Moore. A Computational Logic. Academic Press, 1979.
Geoffrey Burn. Lazy Functional Languages: Abstract Interpretation and Compilation. Pitman, London, 1991.
Patrick Cousot and Radhia Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, pages 252–252. ACM Press, 1977.
N. Dershowitz. Termination of rewriting. Journal of Symbolic Computation, 3(1):69–116, 1987.
J. Giesl. Automatisierung von Terminierungsbeweisen für rekursiv definierte Algorithmen. PhD thesis, Technische Hochschule Darmstadt, 1995.
J. Giesl. Termination analysis for functional programs using term orderings. In Alan Mycroft, editor, Static Analysis Symposium '95, number 984 in Lecture Notes in Computer Science, pages 154–171. Springer, 1995.
K. Hammond, L. Augustsson, B. Boutel, W. Burton, J. Fairbairn, J. Fasel, A. Gordon, M. Guzmán, J. Hughes, P. Hudak, T. Johnsson, M. Jones, D. Kieburtz, R. Nikhil, W. Partain, J. Peterson, S. Peyton Jones, and P Wadler. Report on the programming language Haskell 1.3. Technical report, Department of Computer Science, University of Glasgow, 1996.
Mark P. Jones. The implementation of the Gofer functional programming system. Research Report YALEU/DCS/RR-1030, Yale University, Department of Computer Science, May 1994.
S. Kahrs. Towards a domain theory for termination proofs. In Proceedings of the 6th International Conference on Rewriting Techniques and Applications, volume 914 of Lecture Notes in Computer Science, pages 241–255. Springer-Verlag, 1995.
Hubert Kick. Terminierungsanalyse für den Sprachkern einer nicht-strikten funktionalen Programmiersprache unter Verwendung eines Tableaukalküls für abstrakte Reduktion. Master's thesis, Johann Wolfgang Goethe-Universität, Frankfurt, 1997.
Eric Nöcker. Strictness analysis using abstract reduction. In Functional Programming Languages and Computer Architecture, pages 255–265. ACM Press, 1993.
S. E. Panitz. Generierung statischer Programminformation zur Kompilierung verzögert ausgewerteter funktionaler Programmiersprachen. (Dissertation), Universität Frankfurt, 1997. preliminary version, in German.
Marko Schütz. Striktheits-Analyse mittels abstrakter Reduktion für den Sprachkern einer nicht-strikten funktionalen Programmiersprache. Master's thesis, Johann Wolfgang Goethe-Universität, Frankfurt, 1994.
Kirsten Lackner Solberg, Hanne Riis Nielson, and Flemming Nielson. Strictness and totality analysis. In Baudouin Le Charlier, editor, Static Analysis, number 864 in Lecture Notes in Computer Science, pages 408–422. Springer, 1994.
M. Schmidt-Schauß, S.E. Panitz, and M. Schütz. Strictness analysis by abstract reduction using a tableau calculus. In Alan Mycroft, editor, Static Analysis Symposium '95, number 983 in Lecture Notes in Computer Science, pages 348–365. Springer, 1995.
J. Steinbach. Automatic termination proofs with transformation orderings. In Proceedings of the 6th International Conference on Rewriting Techniques and Applications, volume 914 of Lecture Notes in Computer Science, pages 11–25. Springer-Verlag, 1995.
Chr. Walther. Automatisierung von Terminierungsbeweisen. Künstliche Intelligenz. Vieweg, Braunschweig, 1991.
Chr. Walther. On proving the termination of algorithms by machine. Artificial Intelligence, 71:101–157, 1994.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Panitz, S.E., Schmidt-Schauß, M. (1997). TEA: Automatically proving termination of programs in a non-strict higher-order functional language. In: Van Hentenryck, P. (eds) Static Analysis. SAS 1997. Lecture Notes in Computer Science, vol 1302. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0032752
Download citation
DOI: https://doi.org/10.1007/BFb0032752
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63468-3
Online ISBN: 978-3-540-69576-9
eBook Packages: Springer Book Archive