We generalize the notion of proof term to the realm of transfinite reduction. Proof terms represent reductions in the first-order term format, thereby facilitating their formal analysis. Transfinite reductions can be faithfully represented as infinitary proof terms, unique up to infinitary associativity. We use proof terms to define equivalence of transfinite reductions on the basis of permutation equations. A proof of the compression property via proof terms is presented, which establishes permutation equivalence between the original and the compressed reductions. © 2014 Springer International Publishing Switzerland.
CITATION STYLE
Lombardi, C., Ríos, A., & De Vrijer, R. (2014). Proof terms for infinitary rewriting. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8560 LNCS, pp. 303–318). Springer Verlag. https://doi.org/10.1007/978-3-319-08918-8_21
Mendeley helps you to discover research relevant for your work.