Abstract
Streams are infinite sequences over a given data type. A stream specification is a set of equations intended to define a stream. We propose a transformation from such a stream specification to a TRS in such a way that termination of the resulting TRS implies that the stream specification admits a unique solution. As a consequence, proving such well-definedness of several interesting stream specifications can be done fully automatically using present powerful tools for proving TRS termination.
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.
References
Allouche, J.-P., Shallit, J.: Automatic Sequences: Theory, Applications, Generalizations. Cambridge University Press, Cambridge (2003)
Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. Theoretical Computer Science 236, 133–178 (2000)
Endrullis, J., Grabmayer, C., Hendriks, D.: Data-oblivious stream productivity. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS, vol. 5330, pp. 79–96. Springer, Heidelberg (2008), webinterface tool: http://fspc282.few.vu.nl/productivity/
Giesl, J., et al.: Automated program verification environment (AProVE), http://aprove.informatik.rwth-aachen.de/
Giesl, J., Thiemann, R., Schneider-Kamp, P.: The dependency pair framework: Combining techniques for automated termination proofs. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS, vol. 3452, pp. 301–331. Springer, Heidelberg (2005)
Goguen, J., Lin, K., Rosu, G.: Circular coinductive rewriting. In: Proceedings, 15th International Conference on Automated Software Engineering (ASE 2000), Grenoble, France, September 11-15, 2000, Institute of Electrical and Electronics Engineers Computer Society (2000), webinterface tool CIRC: http://fsl.cs.uiuc.edu/index.php/Special:CircOnline
Korp, M., Sternagel, C., Zankl, H., Middeldorp, A.: Tyrolean termination tool 2. In: Treinen, R. (ed.) RTA 2009. LNCS, vol. 5595, pp. 295–304. Springer, Heidelberg (2009), Tool available at: http://colo6-c703.uibk.ac.at/ttt2/
Lucanu, D., Rosu, G.: CIRC: A circular coinductive prover. In: Mossakowski, T., Montanari, U., Haveraaen, M. (eds.) CALCO 2007. LNCS, vol. 4624, pp. 372–378. Springer, Heidelberg (2007)
Marche, C., Zantema, H.: The termination competition. In: Baader, F. (ed.) RTA 2007. LNCS, vol. 4533, pp. 303–313. Springer, Heidelberg (2007)
Roşu, G.: Equality of streams is a \(\Pi_2^0\)-complete problem. In: Proceedings of the 11th ACM SIGPLAN International Conference on Functional Programming (ICFP 2006). ACM Press, New York (2006)
Rutten, J.J.M.M.: A coinductive calculus of streams. Mathematical Structures in Computer Science 15, 93–147 (2005)
Simonsen, J.G.: The \(\Pi^0_2\)-completeness of most of the properties of rewriting systems you care about (and productivity). In: Treinen, R. (ed.) RTA 2009. LNCS, vol. 5595, pp. 335–349. Springer, Heidelberg (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Zantema, H. (2009). Well-Definedness of Streams by Termination. In: Treinen, R. (eds) Rewriting Techniques and Applications. RTA 2009. Lecture Notes in Computer Science, vol 5595. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02348-4_12
Download citation
DOI: https://doi.org/10.1007/978-3-642-02348-4_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-02347-7
Online ISBN: 978-3-642-02348-4
eBook Packages: Computer ScienceComputer Science (R0)