Abstract
We investigate the property SN ∞ being the natural concept related to termination when considering term rewriting applied to infinite terms. It turns out that this property can be fully characterized by a variant of monotone algebras equipped with a metric. A fruitful special case is obtained when the algebra is finite and the required metric properties are obtained for free. It turns out that the matrix method can be applied to find proofs of SN ∞ based on these observations. In this way SN ∞ can be proved fully automatically for some interesting examples related to combinatory logic.
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
Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. Theoretical Computer Science 236, 133–178 (2000)
Endrullis, J., Waldmann, J., Zantema, H.: Matrix interpretations for proving termination of term rewriting. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 574–588. Springer, Heidelberg (2006)
Endrullis, J., Waldmann, J., Zantema, H.: Matrix interpretations for proving termination of term rewriting. Journal of Automated Reasoning (to appear, 2008)
Giesl, J., et al.: Automated program verification environment (AProVE), http://aprove.informatik.rwth-aachen.de/
Kennaway, J.R.: On transfinite abstract reduction systems. Computer Science Reports CS-R9205. CWI Amsterdam (1992)
Kennaway, R., de Vries, F.-J.: Infinitary rewriting. In: Term Rewriting Systems, by Terese, pp. 668–711. Cambridge University Press, Cambridge (2003)
Kennaway, R., Klop, J.W., Sleep, M.R., de Vries, F.-J.: Transfinite reductions in orthogonal term rewriting systems. Information and Computation 119(1), 18–38 (1995)
Kennaway, R., Severi, P., Sleep, R., de Vries, F.-J.: Infinitary rewriting: From syntax to semantics. In: Middeldorp, A., van Oostrom, V., van Raamsdonk, F., de Vrijer, R. (eds.) Processes, Terms and Cycles: Steps on the Road to Infinity: Essays Dedicated to Jan Willem Klop on the Occasion of His 60th Birthday. LNCS, vol. 3838, pp. 148–172. Springer, Heidelberg (2005)
Ketema, J.: On normalisation of infinitary combinatory reduction systems. In: Voronkov, A. (ed.) Proceedings of the 19th Conference on Rewriting Techniques and Applications (RTA). LNCS. Springer, Heidelberg (2008)
Klop, J.W., de Vrijer, R.C.: Infinitary normalization. In: We Will Show Them! Essays in Honour of Dov Gabbay, vol. 2, pp. 169–192. College Publications (2005)
Zantema, H.: Termination of term rewriting: Interpretation and type elimination. Journal of Symbolic Computation 17, 23–50 (1994)
Zantema, H.: Termination. In: Term Rewriting Systems, by Terese, pp. 181–259. Cambridge University Press, Cambridge (2003)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Zantema, H. (2008). Normalization of Infinite Terms. In: Voronkov, A. (eds) Rewriting Techniques and Applications. RTA 2008. Lecture Notes in Computer Science, vol 5117. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-70590-1_30
Download citation
DOI: https://doi.org/10.1007/978-3-540-70590-1_30
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-70588-8
Online ISBN: 978-3-540-70590-1
eBook Packages: Computer ScienceComputer Science (R0)