Strategy Independent Reduction Lengths in Rewriting and Binary Arithmetic

TL;DR

This paper introduces a criterion ensuring that all reduction strategies in rewriting systems reach normal form in the same number of steps, demonstrated on natural number addition and multiplication in unary and binary forms.

Contribution

It provides a new criterion for strategy-independent reduction lengths in rewriting systems, applicable to natural number operations.

Findings

All reduction strategies reach normal form in the same number of steps under this criterion.

The criterion applies to TRSs computing addition and multiplication in unary and binary notation.

Strategy independence simplifies analysis of rewriting systems.

Abstract

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.