Strategy Independent Reduction Lengths in Rewriting and Binary Arithmetic

Hans Zantema
(University of Technology Eindhoven)

In this paper we give a criterion by which one can conclude that every reduction of a basic term to normal form has the same length. As a consequence, the number of steps to reach the normal form is independent of the chosen strategy. In particular this holds for TRSs computing addition and multiplication of natural numbers, both in unary and binary notation.

In Santiago Escobar: Proceedings 10th International Workshop on Reduction Strategies in Rewriting and Programming (WRS 2011), Novi Sad, Serbia, 29 May 2011 , Electronic Proceedings in Theoretical Computer Science 82, pp. 69–76.
Published: 24th April 2012.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: