Strategy Independent Reduction Lengths in Rewriting and Binary Arithmetic
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 multipli...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2012-04-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/1204.5545v1 |
| Summary: | 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. |
|---|---|
| ISSN: | 2075-2180 |