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. © 2008 Springer-Verlag.
Cite
CITATION STYLE
Zantema, H. (2008). Normalization of infinite terms. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5117 LNCS, pp. 441–455). https://doi.org/10.1007/978-3-540-70590-1_30
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
