Number representations and term rewriting

TL;DR

This paper investigates term rewriting systems for integer number representations, focusing on confluence and termination properties, and proposes modifications to improve their behavior.

Contribution

It analyzes existing systems for number representations, identifies issues with termination and confluence, and suggests minor adjustments to enhance their properties.

Findings

Some systems are not strongly terminating, but can be fixed with minor changes.

Most systems lack confluence, which is more challenging to achieve.

The study provides insights into automating proofs of confluence and termination.

Abstract

In this paper we examine a number of term rewriting system for integer number representations, building further upon the datatype defining systems described in [2]. In particular, we look at automated methods for proving confluence and termination in binary and decimal term rewriting systems for both append and tree constructor functions. We find that some of these term rewriting systems are not strongly terminating, which we resolve with minor changes to these systems. Moreover, most of the term rewriting systems discussed do not exhibit the confluence property, which seems more difficult to resolve.