arXiv:1406.3280v4 [cs.LO] 18 Jul 2016

Three Datatype Defining Rewrite Systems for Datatypes of
Integers each extending a Datatype of Naturals∗
Jan A. Bergstra and Alban Ponse
Informatics Institute,
section Theory of Computer Science,
University of Amsterdam
https://staff.fnwi.uva.nl/j.a.bergstra/

https://staff.fnwi.uva.nl/a.ponse/

Abstract
Integer arithmetic is specified according to three views: unary, binary, and decimal notation. The binary and decimal view have as their characteristic that each normal form
resembles common number notation, that is, either a digit, or a string of digits without leading zero, or the negated versions of the latter. The unary view comprises a specification of
integer arithmetic based on 0, successor function S, and predecessor function, with negative
normal forms −S i (0). Integer arithmetic in binary and decimal notation is based on (postfix)
digit append functions. For each view we define a ground-confluent and terminating datatype
defining rewrite system (DDRS), and in each case the resulting datatype is a canonical term
algebra that extends a corresponding canonical term algebra for natural numbers.
Then, for each view, we consider an alternative DDRS based on tree constructors that
yield comparable normal forms, which for that binary and decimal view admits expressions
that are algorithmically more involved. These DDRSes are incorporated because they are
closer to existing literature. For these DDRSes we also provide ground-completeness results.
Finally, we define a DDRS for the ring of Integers (comprising fifteen rewrite rules) and
prove its ground-completeness.
Keywords and phrases: Equational specification, Initial algebra, Datatype defining rewrite
system, Abstract datatype

Contents
1 Introduction

2

1.1

Digits and rewrite rules in equational form . . . . . . . . . . . . . . . . . . . . . . .

3

1.2

A signature for integers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

4

∗ Version

4: All DDRSes defined in Section 2 are proven ground-complete (Appendix A). In Section 3, the
DDRS for Zut in Table 11 now contains only sixteen equations and is proven ground-complete; the DDRS for Zbt
in Table 13 has one more equation ([bt22]) and is proven ground-complete; the DDRSes for Ndt (Table 14) and Zdt
(Table 16) are those that are proven ground-complete in [13]. In Appendix C, corrected versions of the DDRSes
for Nu′ and Zu′ are proven ground-complete.

2 Three DDRSes for datatypes of Integers, each extending a datatype of Naturals
5
2.1

Unary view . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

5

2.2

Binary view . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

7

2.3

Decimal view . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

9

3 Alternative views with digit tree constructors

11

3.1

Unary view with digit tree constructor . . . . . . . . . . . . . . . . . . . . . . . . . 11

3.2

Binary view with digit tree constructor . . . . . . . . . . . . . . . . . . . . . . . . . 13

3.3

Decimal view with digit tree constructor . . . . . . . . . . . . . . . . . . . . . . . . 15

4 Concluding remarks

16

References

20

A Ground-completeness proofs: DDRSes with digit append constructors

22

A.1 Unary view: the DDRS for Zubd

. . . . . . . . . . . . . . . . . . . . . . . . . . . . 22

A.2 Binary view: the DDRS for Zbud . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24
A.3 Decimal view: the DDRS for Zdub

. . . . . . . . . . . . . . . . . . . . . . . . . . . 26

B Ground-completeness proofs: DDRSes with digit tree constructors

28

B.1 Unary view: the DDRS for Zut . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
B.2 Binary view: the DDRS for Zbt . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
C Another unary view: unary append

1

31

Introduction

We specify integer arithmetic according to three different “views”: unary, binary, and decimal
notation. This work is based on the specifications for natural numbers from [1] and we follow the
same strategy to develop these different views. Each of the specifications we provide is a so-called
DDRS (datatype defining rewrite system) and consists of a number of equations that define a term
rewriting system when interpreting the equations from left-to-right. A DDRS must be groundcomplete, that is, strongly terminating and ground-confluent; for some general information on
term rewriting systems see e.g. [16].
This paper constitutes a further stage in the development of a family of arithmetical datatypes
with corresponding specifications. The resulting specifications (DDRSes) incorporate different
views on the same abstract datatype (ADT), where an ADT may be understood as the isomorphism class of its instantiations which are concrete datatypes. The datatypes considered in [1] are
so-called canonical term algebras which means that carriers are non-empty sets of closed terms
which are closed under taking subterms.
The unary view provides a term rewriting system where terms in unary notation serve as
normal forms. The unary view also provides a semantic specification of binary notation, of
2

0′ = 1
1′ = 2

3′ = 4
4′ = 5

6′ = 7
7′ = 8

2′ = 3

5′ = 6

8′ = 9

Table 1: Enumeration and successor notation of digits of type Z
decimal notation, and of hexadecimal notation. These three positional notations were modified
in [1] with respect to conventional notations in such a way that syntactic confusion between these
notations cannot arise. In this paper, the hexadecimal view is left out as that seems to be an
unusual viewpoint for integer arithmetic.
It seems to be the case that for the unary view the specification of the integers (see Table 3)
is entirely adequate, whereas all subsequent specifications for binary view and decimal view may
provide no more than a formalization of a topic which must be somehow understood before taking
notice of that same formalization. It remains to be seen to what extent the first DDRS for the
unary case may serve exactly that expository purpose.
The strategy of this work is somewhat complicated: on the one hand we look for specifications
that may genuinely be considered introductory, that is, descriptions that can be used to construct
the datatype at hand for the first time in the mind of a person. On the other hand awareness of
the datatype in focus may be needed to produce an assessment of the degree of success achieved
in the direction of the first objective.
In the remainder of this section we discuss some preliminaries. In Section 2 we provide for
each view two DDRSes, one for natural number arithmetic, and one for integer arithmetic. In
Section 3 we consider for each view alternative DDRSes based on tree constructors that yield
comparable normal forms and are closer to existing literature. In Section 4 we finish the paper
with some concluding remarks, and we define a DDRS for arithmetic in the “language of rings”
that is of some theoretical interest (it is used in [4]), while its relatively small ground-confluence
proof paves the way to the more elaborated ground-confluence proofs for the DDRSes defined
in Sections 2 and 3 that are recorded in Appendix A and Appendix B, respectively. Finally, in
Appendix C we discuss two very simple DDRSes, the first one of which establishes an alternative
model for natural number arithmetic in unary view and the second one its generalization to
integer arithmetic.

1.1

Digits and rewrite rules in equational form

Digits are elements of the set D = {0, 1, 2, 3, 4, 5, 6, 7, 8, 9}, ordered in the common way:
0 < 1 < 2 < 3 < 4 < 5 < 6 < 7 < 8 < 9.
For the digits 0, 1, . . . , 8 we denote with i′ the successor digit of i in the given enumeration. In
Table 1 the successor notation on digits is specified as a transformation of syntax, and we adopt
this notation throughout the paper.
We will list rewrite rules in the form of equations t = r to be interpreted from left-to-right,
and we will add tags of the form
[Nn] t = r
for reference, with “N” some name and “n” a natural number (in ordinary, decimal notation).
3

Furthermore, for k, ℓ ∈ D and k < ℓ, the notation
[Nn.i ]ℓi=k t = r
represents the following ℓ − k + 1 equations:
[Nn.k] t[k/i] = r[k/i], . . . , [Nn.ℓ] t[ℓ/i] = r[ℓ/i],
thus with i instantiated from k to ℓ. Occasionally, we will use this notation with two “digit
counters”, as in
[Nn.i.j ]ℓi,j=k t = r,
for a concise representation of the following (ℓ − k + 1)2 equations:
[Nn.k.k] t[k/i][k/j] = r[k/i][k/j], . . . , [Nn.k.ℓ] t[k/i][ℓ/j] = r[k/i][ℓ/j],
...,
[Nn.ℓ.k] t[ℓ/i][k/j] = r[ℓ/i][k/j], . . . ,

1.2

[Nn.ℓ.ℓ] t[ℓ/i][ℓ/j] = r[ℓ/i][ℓ/j].

A signature for integers

The signature ΣZ has the following elements:
1. A sort Z,
2. For digits the ten constants 0, 1, 2, 3, 4, 5, 6, 7, 8, 9,
3. Three one-place functions S, P, − : Z → Z, “successor”, “predecessor”, and “minus”, respectively,
4. Addition and multiplication (infix) +, · : Z × Z → Z,
5. Two one-place functions (postfix) : b 0, : b 1 : Z → Z, “binary append zero” and “binary
append one”, these functions will be used for binary notation,
6. Ten one-place functions (postfix)
: d 0, : d 1, : d 2, : d 3, : d 4, : d 5, : d 6, : d 7, : d 8, : d 9 : Z → Z,
“decimal append zero”, . . . ,“decimal append nine”, to be used for decimal notation.
We shall use the following abbreviations, where i is a digit: S i (t) stands for i applications of the
′
successor function S to t, thus S 0 (t) = t and S i (t) = S(S i (t)), and P i (t) stands for i applications
of the predecessor function P to t.
The “append <digit name>” functions defined in items 5 and 6 can be viewed as instantiations
of more general two-place “append” functions, but that would require the introduction of sorts for
bits (binary digits) and for decimal digits. However, we prefer to keep the signature single-sorted
and that is why we instantiate such “digit append” functions per digit to unary functions and
why we use postfix notation for applications of these functions. E.g.,
(9 : d 7) : d 5 and ((1 : b 0) : b 0) : b 1
represent the decimal number 975, and the binary number 1001, respectively. For the unary view
the normal forms are the classical successor terms, that is
0, S(0), S(S(0)), . . .
4

[S1]
[S2]
[S3]
[S4]

x+0 = x
x + S(y) = S(x + y)
x·0 = 0

[S5.i ]8i=0
[S6.i ]1i=0

i′ = S(i)
x : b i = (x · S(1)) + i

[S7.i ]9i=0

x : d i = (x · S(9)) + i

x · S(y) = (x · y) + x
Table 2: A DDRS for Nubd , natural numbers in unary view

and all minus instances −(t) of each such nonzero normal form t, e.g. −(S(S(0))), if no confusion
can arise, we abbreviate −(t) to −t, as in −x.
For the binary view and for the decimal view, we provide one DDRS for each. Normal forms are
all appropriate digits, all applications of the respective append functions to a nonzero normal form,
and all minus instances −t of each such normal form t that differs from 0. Thus −(((1 : b 0) : b 0) : b 1)
is an example of a normal form in binary view, and −((9 : d 7) : d 5) is one in decimal view.

2

Three DDRSes for datatypes of Integers, each extending
a datatype of Naturals

We provide for each of the unary, binary and decimal view two DDRSes, one for natural number
arithmetic and one for integer arithmetic. For the binary and decimal view we consider specifications that also employ the successor and predecessor functions. These specifications are far more
lengthy and involved, but as DDRSes their quality improves because normal forms are smaller
and are reached in fewer rewriting steps.

2.1

Unary view

Table 2 provides a DDRS for the natural numbers and defines the canonical term algebra Nubd ,
the datatype based on unary view in which binary and decimal view are derived representations.
Minus and predecessor are absent in this datatype. Successor terms, that is expressions involving
zero and successor only, serve as normal forms for the datatype Nubd . This DDRS contains the
well-known equations [S1] − [S4] and the twenty-one equations [S5.i ]8i=0 − [S7.i ]9i=0 , and defines
the rewrite rules that serve the rewriting of binary and decimal notation.
In Table 3 a DDRS is provided for the Zubd of integer numbers with successor, predecessor,
addition, and multiplication, which are defined by equations [u1] − [u14]. We notice that we
do not need equations for rewriting (−x) · y because multiplication is defined by recursion on
its right-argument, and that is why equation [u11] is sufficient, and why addition is defined by
recursion on both its arguments and also requires [u9] and [u10]. Like before, the twenty-one
equations [u15.i ]8i=0 − [u17.i ]9i=0 serve the rewriting of binary and decimal notation.
In Table 4 one finds a listing of equations that are true in the datatype Zubd that is specified
by the DDRS in Table 3. This ensures that these equations are semantic consequences of the
equations for commutative rings. We give a detailed proof of the ground-completeness of this
DDRS for Zubd in Appendix A.1, which also implies ground-completeness of the DDRS for Nubd
defined in Table 2.

5

[u1]
[u2]
[u3]
[u4]

x+0 = x
x + S(y) = S(x + y)

[u5]
[u6]

−0 = 0
S(−(S(x))) = −x

[u7]

x·0 = 0
x · S(y) = (x · y) + x

−(−x) = x

[u8]
[u9]

0+x= x
S(x) + y = S(x + y)

[u10]
[u11]

(−x) + (−y) = −(x + y)
x · (−y) = −(x · y)

[u12]

P (0) = −S(0)

[u13]
[u14]

P (S(x)) = x
P (−x) = −S(x)

[u15.i ]8i=0
[u16.i ]1i=0
[u17.i ]9i=0

i′ = S(i)
x : b i = (x · S(1)) + i
x : d i = (x · S(9)) + i

Table 3: A DDRS for Zubd , integer numbers in unary view

x + (y + z) = (x + y) + z

(1)

x+y =y+x
x+0=x

(2)
(3)

x + (−x) = 0
(x · y) · z = x · (y · z)

(4)
(5)

x·y =y·x
1·x=x

(6)
(7)

x · (y + z) = (x · y) + (x · z)

(8)

S(x) = x + 1
P (x) = x + (−1)

(9)
(10)

x : b i = (x + x) + i

for i ∈ {0, 1}

(11)

x : d i = (10 · x) + i

for i ∈ {0, 1, 2, 3, 4, 5, 6, 7, 8, 9},
0 = 0, i′ = i + 1, 10 = 9 + 1

(12)

Table 4: Equations valid in Zubd , where (1) − (8) axiomatize commutative rings

6

[b1.i ]1i=0

0 :b i = i

[b2]
[b3]

S(0) = 1
S(1) = 1 : b 0

[b4]
[b5]

S(x : b 0) = x : b 1
S(x : b 1) = S(x) : b 0

[b6]

x+0=x

[b7]
[b8]

0+x=x
x + 1 = S(x)

[b9]

1 + x = S(x)

[b10.i.j ]1i,j=0

[b11]
[b12]

x·0=0
x·1=x

[b13.i ]1i=0 x · (y : b i) = ((x · y) : b 0) + (x · i)
[b14.i ]8i=1
[b15.i ]9i=0

i′ = S(i)
x : d i = (x · S(9)) + i

(x : b i) + (y : b j) = S j ((x + y) : b i)
Table 5: A DDRS for Nbud , natural numbers in binary view

So, binary and decimal notation are defined by expanding terms into successor terms. This
expansion involves a combinatorial explosion in size and renders the specification in Tables 2 and 3
irrelevant as term rewriting systems from which an efficient implementation can be generated.

2.2

Binary view

In Table 5 we define a DDRS for a binary view of natural numbers that employs the successor
function as an auxiliary function. Leading zeros except for the zero itself are removed by [b1.i ]1i=0 ,
and successor terms are rewritten according to [b2] − [b5]. This DDRS contains fifteen (parametric) equations (that is, sixteen equations for the specification of addition and multiplication, and
eighteen that serve the rewriting from decimal notation to binary notation via successor terms1 ).
In the binary view natural numbers are identified with normal forms in binary notation. The
specification has a canonical term algebra Nbud which is isomorphic to the canonical term algebra
Nubd of the specification in Table 2. In [14], Kluiving and van Woerkom prove that this DDRS
is complete.
In Table 6 minus and predecessor are introduced and the transition from a signature for natural
numbers to a signature for integers is made; the rules in this table extend those of Table 5 and
define the canonical term algebra Zbud that is isomorphic to the canonical term algebra Zubd of
the specification in Table 3. The DDRS thus defined contains thirty-three (parametric) equations
(thus, 34+24 eq’s in total). We attempt to provide some intuition for equations [b26] and [b27]:
(−x) : b i
should be equal to (−x : b 0) + i, so (−x) : b 0 = −(x : b 0), and (−x) : b 1 is determined by
[b20]

−(P (x : b 0)) = −(P (x) : b 1).
1 Note

that there is no equation [b14.0] that is, 1 = S(0), because 1 is a normal form in binary view.

7

[b1.i ]1i=0

0 :b i = i

[b2]
[b3]

S(0) = 1
S(1) = 1 : b 0

[b4]
[b5]

S(x : b 0) = x : b 1
S(x : b 1) = S(x) : b 0

[b6]

x+0=x

[b7]
[b8]

0+x=x
x + 1 = S(x)

[b9]

1 + x = S(x)

[b16]
[b17]
[b18]

[b10.i.j ]1i,j=0 (x : b i) + (y : b j) = S j ((x + y) : b i)
[b11]
[b12]
[b13.i ]1i=0

x·0=0
x·1=x
x · (y : b i) = ((x · y) : b 0) + (x · i)
i′ = S(i)

[b14.i ]8i=1
[b15.i ]9i=0

−0 = 0
−(−x) = x

x : d i = (x · S(9)) + i

P (0) = −1

[b19]
[b20]

P (1) = 0
P (x : b 0) = P (x) : b 1

[b21]
[b22]

P (x : b 1) = x : b 0
P (−x) = −S(x)

[b23]
[b24]

S(−1) = 0
S(−(x : b 0)) = −(P (x) : b 1)

[b25]

S(−(x : b 1)) = −(x : b 0)

[b26]

(−x) : b 0 = −(x : b 0)

[b27]

(−x) : b 1 = −(P (x) : b 1)

[b28]

x + (−1) = P (x)

[b29]

(−1) + x = P (x)

[b30.i.j ]1i,j=0

(x : b i) + (−(y : b j)) = P j ((x + (−y)) : b i)

[b31.i.j ]1i,j=0

(−(y : b j)) + (x : b i) = P j ((x + (−y)) : b i)

[b32]

(−x) + (−y) = −(x + y)

[b33]

x · (−y) = −(x · y)

Table 6: A DDRS for Zbud that specifies integer numbers in binary view
Equations [b24] and [b25] can be explained in a similar way:
S(−(x : b 0)) should be equal to
S(−(x : b 1)) should be equal to

− (P (x : b 0)) = −(P (x) : b 1),
− (P (x : b 1)) = −(x : b 0).

Normal forms for Zbud are 0, 1, all applications of : b 0 and : b 1 to a nonzero normal form, and
all minus instances −t of each such normal form t that differs from 0.
We note that the equations in Table 6 are semantic consequences of the axioms for commutative
rings (equations (1)−(8) in Table 4). This DDRS is proven strongly terminating in [14]. However,
its non-confluence is also proven in [14], using the following rewrite steps:
P (−(−x))
[b17] ✑✑

✑
✑
✰

◗ [b22]
◗
◗
s
◗

P (x)

−S(−x)

(13)

In Appendix A.2 we prove that this DDRS for Zbud is ground-confluent, and thus ground-complete.
8

[d1.i ]9i=0

0 :d i = i

[d2.i ]8i=0
[d3]

S(i) = i′
S(9) = 1 : d 0

[d4.i ]8i=0
[d5]

S(x : d i) = x : d i′
S(x : d 9) = S(x) : d 0

[d6]

x+0=x

[d7]

0+x=x

[d8.i ]9i=1
[d9.i ]9i=1
[d10.i.j ]9i,j=0

x + i = S i (x)

[d11]
[d12.i ]8i=0
[d13.i ]9i=0
[d14.i ]1i=0

x·0 = 0
x · i′ = (x · i) + x
x · (y : d i) = ((x · y) : d 0) + (x · i)
x : b i = (x + x) + i

i + x = S i (x)
(x : d i) + (y : d j) = S j ((x + y) : d i)
Table 7: A DDRS for Ndub , natural numbers in decimal view

2.3

Decimal view

In Table 7 we define a DDRS for a decimal view of natural numbers that defines the canonical
term algebra Ndub , the datatype in which unary and binary view are derived representations.
This DDRS consists of fourteen (parametric) equations (172 eq’s in total). The datatype Ndub
is isomorphic to the canonical term algebra Nubd of the specification in Table 2. Leading zeros
except for the zero itself are removed by [d1.i ]9i=0 , and successor terms are rewritten according
to [d2.i ]8i=0 − [d5]. Rewriting from binary notation is part of this DDRS, and the last equation
scheme [d14.i ]1i=0 serves that purpose. In [14], this DDRS for Ndub is proven complete.
Before we extend the DDRS in Table 7 to the integers, we define in Table 8 a variant of
successor notation for digits that we call “10 minus subtraction” with notation i⋆ , and that for
decimal digits i ∈ {1, ..., 9} characterizes the equation
i⋆ = 10 − i.
In Table 9, minus and predecessor are added and the transition to integers is made. In rule
scheme [d26.i ]9i=1 we employ the notation i⋆ . The DDRS thus defined is named Zdub and is
isomorphic to the canonical term algebra Zubd of the specification in Table 3; it contains thirtytwo (parametric) equations (so, 172 + 272 eq’s in total).
The (twenty) equations captured by [d23] − [d26.i ]9i=1 can be explained in a similar fashion
as was done in the previous section for [b24] − [b27]: for example,
(−5) : d 3

1⋆ = 9

4⋆ = 6

7⋆ = 3

2⋆ = 8

5⋆ = 5

8⋆ = 2

⋆

3 =7

⋆

6 =4

9⋆ = 1

Table 8: “10 minus” subtraction notation for decimal digits
9

should be equal to −(5 : d 0) + 3 = −(4 : d 7), and this follows immediately from the appropriate
equation in [d26.i ]9i=1 .
The equations of the DDRS specified by Tables 7 and 9 are semantic consequences of the
equations for commutative rings (equations (1) − (8) in Table 4). In [14], this DDRS for Zdub is
proven strongly terminating, and non-confluent by essentially the same counter-example as was
used for the DDRS for Zbud (see (13)):
P (−(−x))
[d16] ✑✑

◗ [d21]
◗
◗
s
◗

✑
✑
✰

P (x)

−S(−x)

In Appendix A.3 we prove that this DDRS for Zdub is ground-confluent, and thus ground-complete.

[d1.i ]9i=0

0 :d i = i

[d15]

−0 = 0

[d2.i ]8i=0
[d3]

S(i) = i′
S(9) = 1 : d 0

[d16]

−(−x) = x

[d4.i ]8i=0
[d5]

S(x : d i) = x : d i′
S(x : d 9) = S(x) : d 0

[d6]

x+0=x

[d7]

0+x=x

[d8.i ]9i=1
[d9.i ]9i=1
[d10.i.j ]9i,j=0

x + i = S i (x)
(x : d i) + (y : d j) = S j ((x + y) : d i)
x·0=0
′

x · i = (x · i) + x
x · (y : d i) = ((x · y) : d 0) + (x · i)

[d14.i ]1i=0

x : b i = (x + x) + i

P (0) = −1
P (i′ ) = i
P (x : d 0) = P (x) : d 9

[d20.i ]8i=0
[d21]

P (x : d i′ ) = x : d i
P (−x) = −S(x)

[d22.i ]8i=0
[d23]

i + x = S i (x)

[d11]
[d12.i ]8i=0
[d13.i ]9i=0

[d17]
[d18.i ]8i=0
[d19]

S(−i′ ) = −i
S(−(x : d 0)) = −(P (x) : d 9)

[d24.i ]8i=0 S(−(x : d i′ )) = −(x : d i)
[d25]

(−x) : d 0 = −(x : d 0)

[d26.i ]9i=1

(−x) : d i = −(P (x) : d i⋆ )

[d27.i ]9i=1

x + (−i) = P i (x)

[d28.i ]9i=1

(−i) + x = P i (x)

[d29.i.j ]9i,j=0 (x : d i) + (−(y : d j)) = P j ((x + (−y)) : d i)
[d30.i.j ]9i,j=0 (−(y : d j)) + (x : d i) = P j ((x + (−y)) : d i)
[d31]
[d32]

(−x) + (−y) = −(x + y)
x · (−y) = −(x · y)

Table 9: A DDRS for Zdub that specifies integers in decimal view, employing i⋆ from Table 8

10

3

Alternative views with digit tree constructors

Having defined DDRSes that employ (postfix) digit append functions in Section 2, we now consider
the more general digit tree constructor functions. For the binary view, this approach is followed
by Bouma and Walters in [8]; for a view based on any radix (number base), this approach is
further continued in Walters [17] and Walters and Zantema [18], where the constructor is
called juxtaposition because it goes with the absence of a function symbol in order to be close to
ordinary decimal and binary notation.
We extend the signature ΣZ defined in Section 1.2 with the following three functions (infix):
û

,

b̂

,

d̂

: Z × Z → Z,

called “unary digit tree constructor function”, “binary digit tree constructor function”, and “decimal digit tree constructor function”, and to be used for unary, binary notation and decimal
notation, respectively. The latter two constructors serve to represent positional notation and
satisfy the semantic equations Jx b̂ yK = 2 · JxK + JyK and Jx d̂ yK = 10 · JxK + JyK.
For integer numbers in decimal view or binary view, normal forms are the relevant digits, all
applications of the respective constructor with left argument a nonzero normal form and right
argument a digit, and all minus instances −t of each such nonzero normal form t, these satisfy
J−(t)K = −(JtK). E.g.,
(9 d̂ 7) d̂ 5 and ((1 b̂ 0) b̂ 0) b̂ 1
represent the decimal number 975 and the binary number 1001, respectively, and the normal form
that represents the additional inverse of the latter is −(((1 b̂ 0) b̂ 0) b̂ 1). A minor complication
with decimal and binary digit tree constructors is that we now have to consider rewritings such
as
2 d̂ (1 d̂ 5) = (2 + 1) d̂ 5 = 3 d̂ 5 (= 35),
which perhaps are somewhat non-intuitive. For integers in unary view, thus with unary digit tree
constructor, this complication is absent (see Section 3.1).
We keep the presentation of the resulting DDRSes (those defining the binary and decimal view
are based on [17, 18]) minimal in the sense that equations for conversion from the one view to the
other are left out. Of course, it is easy to define such equations. Also, equations for conversion to
and from the datatypes defined in Section 2 are omitted, although such equations are also easy
to define.

3.1

Unary view with digit tree constructor

For naturals in this particular unary view, normal forms are 0 and expressions t û 0 with t a
normal form (thus, with association of û to the left). Of course, the phenomenon of “removing
leading zeros” does not exist in this particular unary view. The resulting datatype Nut is defined
in Table 10.
In the unary view, û is an associative operator, as is clear from rule [ut1] (in contrast to digit
tree constructors for the binary and decimal case). Moreover, the commutative variants t û r
and r û t rewrite to the same normal form. The latter property also follows from the following

11

[ut1]

x û (y

[ut2]
[ut3]

x+0=x
x + (y û 0) = (x + y) û 0

û

z) = (x û y) û z

[ut4]
[ut5]

x·0=0
x · (y û 0) = (x · y) + x

Table 10: A DDRS for Nut , natural numbers in unary view with unary digit tree constructor
semantics for closed terms:
J0K = 0,
Jx û yK = JxK + JyK + 1,
Jx + yK = JxK + JyK,
Jx · yK = JxK · JyK.
Observe that
x + (y

û

z) = (x + y) û z

and x · (y

û

z) = (x · (y + z)) + x

are valid equations in Nut .
The extension to integer numbers can be done in a similar fashion as in the previous section,
thus obtaining normal forms of the form −(t) with t a nonzero normal form in Nut . However, also
terms of the form x û (−y) and variations thereof have to be considered. We define this extension
in Table 11 below and call the resulting datatype Zut .
Adding the interpretation rule J−xK = −JxK and exploiting the commutativity of û in Jx û yK,
it can be easily checked that [ut6] − [ut16] (as equations) are sound. In Appendix B.1 we prove
that this DDRS is ground-complete, which also implies ground-completeness of the DDRS for
Nut defined in Table 10: strong termination is preserved and all its equations are valid.

[ut1]

x û (y

[ut2]
[ut3]

x+0=x
x + (y û 0) = (x + y) û 0

[ut4]
[ut5]

û

z) = (x û y) û z

x·0=0
x · (y

û

0) = (x · y) + x

[ut6]
[ut7]

−0 = 0
−(−x) = x

[ut8]

0 û (−(x û 0)) = −x

[ut9]
[ut10]

(x û 0) û (−(y û 0)) = x û (−y)
(−(x û 0)) û 0 = −x

[ut11]
[ut12]

(−(x û 0)) û (y û 0) = (−x) û y
(−(x û 0)) û (−(y û 0)) = −((x + y) û 0)

[ut13]

0+x=x

[ut14]
[ut15]

(x û 0) + (−(y û 0)) = x + (−y)
(−x) + (−y) = −(x + y)

[ut16]

x · (−y) = −(x · y)

Table 11: A DDRS for Zut that specifies integer numbers in unary view with unary digit tree
constructor

12

[bi1]
[bi2]

0 b̂ x = x
x b̂ (y b̂ z) = (x + y) b̂ z

[bi3]

0+x=x

[bi4]
[bi5]

1+0=1
1 + 1 = 1 b̂ 0

[bi6]
[bi7]

1 + (x b̂ y) = x b̂ (1 + y)
(x b̂ y) + z = x b̂ (y + z)

[bi8]
[bi9]

x·0=0
x·1=x

[bi10]

x · (y

b̂

z) = (x · y) b̂ (x · z)

Table 12: A DDRS for Nbt , natural numbers in binary view with binary digit tree constructor

3.2

Binary view with digit tree constructor

For naturals in binary view with the binary digit tree constructor, the associated datatype Nbt is
defined in Table 12. According to [18] (with a reference to [8]), the rewriting system defined by
[bi1] − [bi7] is strongly terminating and ground-confluent, and thus ground-complete.
In [18] a rewriting system for integer arithmetic is provided with next to juxtaposition and
minus also addition, subtraction and multiplication, and proven ground-confluent and terminating
with respect to any radix (number base). In Table 13 we present a variant of this rewriting system
without subtraction for the binary digit tree constructor, and define the datatype Zbt .

[bt1]
[bt2]

0 b̂ x = x
x b̂ (y

b̂

z) = (x + y) b̂ z

[bt3]

0+x=x

[bt4]

x+0=x

[bt13]

−0 = 0

[bt14]

−(−x) = x

[bt15]

1 b̂ (−1) = 1

[bt16]

(x b̂ 0) b̂ (−1) = (x b̂ (−1)) b̂ 1

[bt5]
[bt6]

1 + 1 = 1 b̂ 0
x + (y b̂ z) = y b̂ (x + z)

[bt17]
[bt18]

(x b̂ 1) b̂ (−1) = (x b̂ 0) b̂ 1
x b̂ (−(y b̂ z)) = −((y + (−x)) b̂ z)

[bt7]

(x b̂ y) + z = x b̂ (y + z)

[bt19]

(−x) b̂ y = −(x b̂ (−y))
1 + (−1) = 0

[bt8]

x·0 =0

[bt20]

[bt9]
[bt10]

0·x =0
1·1 =1

[bt21]
[bt22]

[bt11]
[bt12]

x · (y b̂ z) = (x · y) b̂ (x · z)
(x b̂ y) · z = (x · z) b̂ (y · z)

[bt23]
[bt24]

(−1) + 1 = 0
(−1) + (−1) = −(1 b̂ 0)
x + (−(y b̂ z)) = −(y b̂ (z + (−x)))
(−(x b̂ y)) + z = −(x b̂ (y + (−z)))

[bt25]

x · (−y) = −(x · y)

[bt26]

(−x) · y = −(x · y)

Table 13: A DDRS for Zbt , integer numbers in binary view with binary digit tree constructor

13

In [14] it is proven that the associated term rewriting system is strongly terminating. Confluence is disproven in [14] by the following counter-example:
x b̂ (y

b̂

(z

[bt2] ✑✑

(x + y) b̂ (z

b̂

w))

◗ [bt2]
◗
◗
s
◗

✑
✰
✑
w)
b̂

x b̂ ((y + z) b̂ w)

[bt2]

[bt2]

❄
((x + y) + z) b̂ w

❄
(x + (y + z)) b̂ w

(14)

However, ground-confluence for this DDRS is proven in Appendix B.2, by which it is groundcomplete. As a consequence, equations [bt1] − [bt12] define an alternative DDRS for Nbt that is
also ground-complete: strong termination is preserved and all equations are valid.

14

[dt1]
[dt2]

0 d̂ x = x
x d̂ (y d̂ z) = (x + y) d̂ z

[dt3.i ]8i=0

S(i) = i′

[dt4]
[dt5.i ]8i=0

S(9) = 1 d̂ 0
S(x d̂ i) = x d̂ i′

[dt6]

S(x d̂ 9) = S(x) d̂ 0

x + i = S i (x)

[dt7.i ]9i=0
[dt8.i ]9i=0

x + (y

[dt9]
[dt10.i ]9i=1
[dt11.i ]9i=0

d̂

i) = S i (y

d̂

x)

x·0=0
Pi
x·i =
x
x · (y d̂ i) = ((x · y) d̂ 0) + (x · i)

Table 14: A DDRS for Ndt , natural numbers with decimal digit tree constructor in decimal view
(using the notation i′ from Table 1)

3.3

Decimal view with digit tree constructor

For naturals in decimal view with the decimal digit tree constructor, we make use of successor
terms, in order to avoid (non-parametric) equations such as
1 + 1 = 2, . . . , 9 + 8 = 1 d̂ 7,
...,

9 + 9 = 1 d̂ 8,

1 · 1 = 1, . . . ,

9 · 9 = 8 d̂ 1.

8 · 9 = 7 d̂ 2,

The associated datatype Ndt is defined in Table 14. Following van der Kamp [13], we use in
equations [dt10.i ]9i=1 for i ∈ {1, 2, ..., 9} the notation
Pi

x

for i − 1 repeated applications of + with association to the right, thus
P1
Pi+1
Pi
x = x and for i = 1, ..., 8,
x=x+
x.
The extension to integers is given by the equations in Table 16 that define the datatype Zdt .
In contrast to the approaches in [17, 18] with juxtaposition, we now make use of both successor
terms and predecessor terms, and the DDRS presented here is composed from rewrite rules for
successor and predecessor, rewrite rules defined in [17, 18], and combinations thereof. For a
smooth, parametric representation we also use the predecessor notation i′′ for digits larger than
0 defined in Table 15. In [13] it is shown that the associated rewriting system for Zdt is strongly
terminating and ground-confluent, and thus ground-complete. This implies that the DDRS in
Table 14 for Ndt is also ground-complete: strong termination is preserved and all its equations
are valid. Finally we note that both these DDRSes are not confluent (cf. counter-example (14)).

1′′ = 0
2′′ = 1

4′′ = 3
5′′ = 4

7′′ = 6
8′′ = 7

3′′ = 2

6′′ = 5

9′′ = 8

Table 15: Predecessor notation for decimal digits
15

[dt1]
[dt2]

0 d̂ x = x
x d̂ (y d̂ z) = (x + y) d̂ z

[dt12]
[dt13]

−0 = 0
−(−x) = x

[dt3.i ]8i=0

S(i) = i′

[dt4]
[dt5.i ]8i=0

S(9) = 1 d̂ 0
S(x d̂ i) = x d̂ i′

[dt15.i ]8i=0
[dt16]

P (i′ ) = i
P (x d̂ 0) = P (x) d̂ 9

[dt6]

S(x d̂ 9) = S(x) d̂ 0

[dt17.i ]8i=0

P (x d̂ i′ ) = x d̂ i

[dt7.i ]9i=0

[dt10.i ]9i=1
[dt11.i ]9i=0

[dt18]

x + i = S i (x)

[dt8.i ]9i=0 x + (y
[dt9]

[dt14]

d̂

i) = S i (y

d̂

x)

x·0 =0
Pi
x·i =
x
x · (y d̂ i) = ((x · y) d̂ 0) + (x · i)

P (0) = −1

P (−x) = −S(x)

[dt19.i ]8i=0
[dt20]

S(−i′ ) = −i
S(−(x d̂ 0)) = −(P (x) d̂ 9)

[dt21.i ]8i=0

S(−(x d̂ i′ )) = −(x d̂ i)

[dt22]

(−x) d̂ y = −(x d̂ (−y))

[dt23.i.j ]9i,j=1

i d̂ (−j) = i′′

d̂

j⋆

[dt24.i.j ]9i,j=1 (x d̂ i) d̂ (−j) = (x d̂ i′′ ) d̂ j ⋆
[dt25]
[dt26.i ]9i=1
[dt27]
[dt28]

x d̂ (−(y

d̂

z)) = −((y + (−x)) d̂ z)

x + (−i) = P i (x)
x + (−(y

d̂

z)) = −(y

d̂

(z + (−x)))

x · (−y) = −(x · y)

Table 16: A DDRS for Zdt , integer numbers with decimal digit tree constructor in decimal view
(using i′ from Table 1, i⋆ from Table 8, and i′′ from Table 15)

4

Concluding remarks

This paper is about the design (by means of trial and error) of datatype defining rewrite systems
(DDRSes) rather than about the precise analysis of the various rewriting systems per se. What
matters in addition to readability and conciseness of each DDRS is at this stage a proof — or
at least a reasonable confidence — that each of these rewriting systems is strongly terminating
and ground-confluent (and thus ground-complete), and furthermore that the (intended) normal
forms are natural and convincing, while the rewriting systems are comprehensible.
When specifying a datatype of integers as an extension of the naturals, the unary view leads
to satisfactory results, but with high inefficiency. For the binary view and the decimal view based
on the unary append functions and discussed in Section 2, such extensions are provided, but
the resulting rewriting systems are at first sight significantly less concise and comprehensible.
Recently, strong termination has been proven by Kluiving and van Woerkom [14] with help
of the AProVE tool [12], and ground-confluence is proven in this paper. Some further remarks:
1. The three DDRSes (datatype defining rewrite systems) for integers given in Section 2 each
produce an extension datatype for a datatype for the natural numbers. An initial algebra
specification of the datatype of integers is obtained from any of the DDRSes given in [1] by
16

• taking the reduct to the signature involving unary, binary, and decimal notation only,
• removing rewrite rules involving operators for hexadecimal notation,
• expanding the signature with a unary additive inverse and a unary predecessor function,
• adding rewrite rules (in equational form) that allow for the unique normalization of
closed terms involving the minus sign,
while making sure that these rewrite rules (viewed as equations) are semantic consequences
of the equations for commutative rings.
2. Syntax for hexadecimal notation has been omitted because that usually plays no role when
dealing with integers. It is an elementary exercise to incorporate hexadecimal notation.
3. The DDRSes for the binary view and the decimal view are hardly intelligible unless one
knows that the objective is to construct a commutative ring. A decimal normal form is
defined as either a digit, or an application of a decimal append function : d i to a nonzero
normal form (for all digits i). This implies the absence of (superfluous) leading zeros,
and the (ground) normal forms thus obtained correspond bijectively to the non-negative
integers (that is, N). Incorporating all minus instances −(t) of each nonzero normal form t
yields the class of normal forms. The “semantics” of these normal forms in the language of
commutative rings is standard:
J0K = 0,
Ji′ K = JiK + 1 for all digits 0 ≤ i < 9 and i′ defined as in Table 1,
Jx : d iK = (10 · JxK) + JiK for all digits i, and 10 = J9K + 1,
J−(x)K = −(JxK).
A binary normal form has similar semantics: Jx : b iK = (2 · JxK) + JiK for digits 0, 1, and
2 = 1 + 1.
4. Understanding the concept of a commutative ring can be expected only from a person who
has already acquired an understanding of the structure of integers and who accepts the
concept of generalization of a structure to a class of structures sharing some but not all of
its properties.
In other words, the understanding that a DDRS for the integers is provided in the binary
view and in the decimal view can only be communicated to an audience under the assumption that a reliable mental picture of the integers already exists in the minds of members
of the audience. This mental picture, however, can in principle be communicated by taking notice of the DDRS for the unary view first. This conceptual (near) circularity may
be nevertheless be considered a significant weakness of the approach of defining (and even
introducing) the integers as an extension of naturals by means of rewriting.
Although full confluence of the DDRSes defined in Section 2 for the binary and decimal view has
been disproven by Kluiving and van Woerkom [14] (with help of the confluence tool CSI [20]),
we prove in Appendix A that all DDRSes defined in this section are ground-confluent, and thus
ground-complete.
In Section 3 we discussed some alternatives for the above-mentioned DDRSes based on papers
of Bouma and Walters [8], Walters [17], and Walters and Zantema [18] in which digit
tree constructors are used. In [17], Walters presents a TRS (term rewriting system) based
17

Name
rule count
rule schemes
extra operators

Ndub

Zdub

Ndt

Zdt

DA(10)

JP(10)

172

444

62

277

135

438

14

32

11

28

10

30

S(x),
x : b 0, x : b 1

S(x), P (x),
x : b 0, x : b 1

S(x)

S(x),
P (x)

x−y

Table 17: Rule count for decimal representation, where DA(10) and JP(10) both originate
from [18] instantiated for base 10.
on juxtaposition as a tree constructor for integer arithmetic with addition and subtraction that
is ground-complete and parametric over any radix. In [18], Walters and Zantema extend
this TRS with multiplication and prove ground-completeness, using semantic labelling for their
termination proof, and judge this TRS — named JP — to have good efficiency and readability
(in comparison with some alternatives discussed in that paper).
With the tool AProVE [12], Kluiving and van Woerkom [14] proved strong termination of
TRSes for arithmetic over N and over Z that employ the binary tree constructors. In Appendix B
we prove that the resulting DDRSes (Tables 12 and 13) are ground-complete. Kluiving and
van Woerkom also proposed in [14] a TRS for arithmetic over the natural numbers employing
decimal tree constructors (based on a DDRS proposed in version 2 of this paper) and proved
strong termination with the tool AProVE. However, its natural extension to a TRS for integer
arithmetic could not be proven terminating, probably due to its size. This led to further research
by van der Kamp [13], who adapted both these TRSes and proved ground-completeness. The
resulting DDRSes are those in Tables 14 and 16.
Of course, many normal forms in decimal notation have names that confirm their base, for
example “six hundred eighty-nine” haei or “six hundred and eighty-nine” hbei. A decimal notation as 689 is so common that one usually does not question whether it represents (6 : d 8) : d 9
or (6 d̂ 8) d̂ 9 or some other formally defined notation. Nevertheless, as we have seen, different
algorithmic approaches to for example addition may apply, although one would preferably not
hamper an (initial) arithmetical method with notation such as x d̂ (y d̂ z) and rewrite rules such
as x d̂ (y d̂ z) → (x + y) d̂ z, and for this reason we have a preference for the DDRSes defined in
Section 2. It should be noted that hand-written ground-confluence proofs of the size recorded
in Appendix A and B are of course error-prone and should be automated. Following [13], we
summarize in Table 17 the rule counts of the term rewriting systems for decimal representation
of natural and integer arithmetic considered in this paper and those considered in [18] (the TRS
named DA is discussed below), and observe no significant differences in these counts.
We briefly mention two other, comparable approaches to arithmetic that are also based on
some form of digit append constructors for representing numbers. First, in [18] Walters and
Zantema introduce a TRS which they named DA (for “digit application”) with addition and
multiplication on natural numbers. The authors prove strong termination by recursive path
ordering and confluence, and also judge this TRS to have good efficiency and readability. Secondly,
in [10], Contejean, Marché and Rabehasaina introduce integer arithmetic based on balanced
ternary numbers, that is, numbers that can be represented by a digit append function : t with
digits -1,0,1 and semantics JiK = i and Jx : t iK = 3 · JxK + i (see, e.g., Knuth [15]) and provide a
TRS that is confluent and terminating modulo associativity and commutativity of addition and
multiplication.
18

[r1]
[r2]
[r3]
[r4]

−0 = 0
−(−x) = x

[r12]
[r13]

1 + (−1) = 0
(x + 1) + (−1) = x

[r7]

x + (−(y + 1)) = (x + (−y)) + (−1)

[r8]
[r9]
[r10]
[r11]

[r14]

x + (y + z) = (x + y) + z
x+0=x

[r5]
[r6]

x·0 = 0
x·1 = x

[r15]

x · (−y) = (−x) · y
x · (y + z) = (x · y) + (x · z)

0+x=x
(−1) + 1 = 0
(−(x + 1)) + 1 = −x
(−x) + (−y) = −(x + y)
Table 18: A DDRS for Zr , integer numbers in the language of rings

Based on either a DDRS for the natural numbers or a DDRS for the integers one may develop
a DDRS for rational numbers in various ways. It is plausible to consider the meadow of rational
numbers of [7] or the non-involutive meadow of rational numbers (see [2]) or the common meadow
of rational numbers (see [3]) as abstract algebraic structures for rationals in which unary, binary,
and decimal notation are to be incorporated in ways possibly based on the specifications presented
above. Furthermore, one does well to consider the work discussed in [10] on a term rewriting
system for rational numbers, in which arithmetic for rational numbers is specified (this is the
main result in [10], for which the above-mentioned work on integer arithmetic is a preliminary):
the authors specify rational numbers by means of a TRS that is complete modulo associativity
and commutativity of addition and multiplication, taking advantage of Stein’s algorithm for
computing gcd’s of non-negative integers without any division2 (see, e.g., [15]).
A survey of equational algebraic specifications for abstract datatypes is provided in [19]. In [6]
one finds the general result that computable abstract datatypes can be specified by means of
specifications which are confluent and strongly terminating term rewriting systems. Some general
results on algebraic specifications can be found in [9, 5, 11]. More recent applications of equational
specifications can be found in [7].
We conclude the paper with the introduction of a simple DDRS in Table 18 that specifies the
integers in the signature Σr = {0, 1, −( ), +, ·} of rings and we name this datatype Zr . Observe
that the minus variant of equation [r7], that is,
(−x) + (y + 1) = ((−x) + y) + 1
is an instance of equation [r3]. Also, observe that the equations in Table 18 are semantic consequences of the axioms for commutative rings (equations (1) − (8) in Table 4). In [14], Kluiving
and van Woerkom report that the term rewriting system defined by this DDRS is strongly
terminating,3 and below we prove that it is also ground-confluent, and thus ground-complete.
2 Apart from halving even numbers, which is easy in binary notation, but can otherwise be specified with a shift
operation.
3 Alternatively, the following weight function |t| on closed terms can be used to prove strong termination:
|0| = |1| = 2, | − x| = 2|x| + 1, |x + y| = |x| + 3|y|, and |x · y| = |x| · |y|2 .

19

Define the set N of closed terms over Σr as follows:
N = {0} ∪ N + ∪ N − ,
N + = {1} ∪ {t + 1 | t ∈ N + },
N − = {−t | t ∈ N + }.
It immediately follows that if t ∈ N , then t is a normal form (no rewrite step applies). Furthermore, two distinct elements in N have distinct values in Z. In order to prove ground-confluence
of the associated TRS it suffices to show that for each closed term over Σr , either t ∈ N or t has
a rewrite step, so that each normal form is in N .
We prove this by structural induction on t. The base cases t ∈ {0, 1} are trivial. For the
induction step we have to consider three cases:
1. Case t = −r. Assume that r ∈ N and apply case distinction on r:
• if r = 0, then t → 0 by equation [r1],
• if r ∈ N + , then t ∈ N ,
• if r ∈ N − , then t has a rewrite step by equation [r2].
2. Case t = u + r. Assume that u, r ∈ N and apply case distinction on r:
• if r
• if r
–
–
–
–
• if r
• if r
–
–
–
–
• if r

= 0, then t → u by equation [r4],
= 1, then apply case distinction on u:
if u = 0, then t → 1 by equation [r8],
if u ∈ N + , then t ∈ N ,
if u = −1, then t → 0 by equation [r9],
if u = −(u′ + 1), then t has a rewrite step by equation [r10],
= r′ + 1, then t → (u + r′ ) + 1 by equation [r3],
= −1 then t = u + (−1) and apply case distinction on u:
if u = 0, then t has a rewrite step by equation [r8],
if u = 1, then t has a rewrite step by equation [r5],
if u = u′ + 1, then t has a rewrite step by equation [r6],
if u ∈ N − , then t has a rewrite step by equation [r11],
= −(r′ + 1), then t → (u + (−r′ )) + (−1) by equation [r7].

3. Case t = u · r. Assume that u, r ∈ N , then t has a rewrite step according to one of the
equations [r12] − [r15].
This concludes our proof.
In [14] it is observed that this DDRS for Zr is not confluent: (−(−x)) + (−y) → x + (−y) and
(−(−x)) + (−y) → −((−x) + y) by [r2], [r11]. Attempts to use Knuth-Bendix completion yielded
no solution and the authors write that “Too many rules needed to be added and changed to solve
the confluence issues. The system itself does not seem to be designed with confluence in mind”.
Acknowledgement. We thank Boas Kluiving and Wijnand van Woerkom for adapting some
of the DDRSes defined in version 2 of this paper and proving various results: completeness of the
DDRSes for Nbud and Ndub ; strong termination and non-confluence of those for Zbud , Zdub , and
Zr ; and reporting on all this in [14]. We thank Luca van der Kamp for his further research on
DDRSes for Ndt and Zdt , and coming up with those defined in [13] and discussed in Section 3.3.
20

References
[1] Bergstra, J.A. (2014). Four datatype defining rewrite systems for an abstract datatype of
natural numbers. Electronic report TCS1407v2, University of Amsterdam, Informatics Institute, section Theory of Computer Science (August 2014). Available at
https://ivi.fnwi.uva.nl/tcs/pub/tcsreports/TCS1407v2.pdf.
[2] Bergstra, J.A. and Middelburg, C.A. (2015). Division by zero in non-involutive meadows.
Journal of Applied Logic, 13(1):1–12 (doi.org/10.1016/j.jal.2014.10.001). Preprint
available at arXiv/1406.2092v2 [math.RA] (2014, 9 June).
[3] Bergstra, J.A. and Ponse, A. (2015). Division by zero in common meadows. In R. de Nicola
and R. Hennicker (Eds.): Software, Services, and Systems, Lecture Notes in Computer Science, Vol. 8950, Springer, pp. 46–61. Preprint available at arXiv/1406.6878v2 [math.RA]
(2014, 22 December).
[4] Bergstra, J.A. and Ponse, A. (2016). Fracpairs and fractions over a reduced commutative
ring. Indagationes Mathematicae, 27:727–748 (doi.org/10.1016/j.indag.2016.01.007).
Preprint available at arXiv/1411.4410v2 [math.RA] (2016, 22 Jan).
[5] Bergstra, J.A. and Tucker, J.V. (1987). Algebraic specifications of computable and semicomputable data types. Theoretical Computer Science, 50(2):137–181.
[6] Bergstra, J.A. and Tucker, J.V. (1995). Equational specifications, complete term rewriting
systems, and computable and semicomputable algebras. Journal of the ACM, 42(6):1194–
1230.
[7] Bergstra, J.A. and Tucker, J.V. (2007). The rational numbers as an abstract data type.
Journal of the ACM, 54(2), Article 7.
[8] Bouma, L.G. and Walters, H.R. (1989). Implementing algebraic specifications. In J.A. Bergstra, J. Heering, and P. Klint (Eds.): Algebraic Specification (Chapter 5), Addison-Wesley,
pp. 199–282.
[9] Broy, M., Wirsing, M., and Pair, C. (1984). A systematic study of models of abstract data
types. Theoretical Computer Science, 33(2):139–174.
[10] Contejean, E., Marché, C., and Rabehasaina, L. (1997). Rewrite systems for natural, integral, and rational arithmetic. In H. Comon (Ed.): Rewriting Techniques and Applications
(Proceedings 8th International Conference, RTA’97), Lecture Notes in Computer Science,
Vol. 1232, Springer, pp. 98–112.
[11] Gaudel, M.-C. and James, P.R. (1998). Testing algebraic data types and processes: a unifying
theory. Formal Aspects of Computing, 10(5-6):436–451.
[12] Giesl, J., Schneider-Kamp, P., and Thiemann, R. (2006). AProVE 1.2: Automatic termination proofs in the dependency pair framework. In U. Furbach and N. Shankar (Eds.): IJCAR
2006, Lecture Notes in Computer Science, Vol. 4130, Springer, pp. 281–286.
[13] Kamp, L.R. van der (2016). A term rewrite system for decimal integer arithmetic. BSc. thesis
Computer Science, University of Amsterdam (June 2016). Available at
https://esc.fnwi.uva.nl/thesis/centraal/files/f576933574.pdf.

21

[14] Kluiving, B. and Woerkom, W. van (2016). Number representations and term rewriting. Honours project BSc Computer Science and BSc Artificial Intelligence, University of Amsterdam
(January 31, 2016). Available at arXiv:1607.04500v1 [cs.LO], 15 Jul 2016.
[15] Knuth, D.E. (1997). The Art of Computer Programming, Volume 2 (3rd Edition): Seminumerical Algorithms. Addison-Wesley.
[16] Terese. Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science, Vol. 55,
Cambridge University Press, 2003.
[17] Walters, H.R. (1994). A complete term rewriting system for decimal integer arithmetic.
Report CS-R9435, CWI. Available at http://oai.cwi.nl/oai/asset/5140/5140D.pdf.
[18] Walters, H.R. and Zantema, H. (1995). Rewrite systems for integer arithmetic. In J. Hsiang
(Ed.): Rewriting Techniques and Applications (Proceedings 6th International Conference,
RTA’95), Lecture Notes in Computer Science, Vol. 914, Springer, pp. 324–338. Preprint
available at http://oai.cwi.nl/oai/asset/4930/4930D.pdf.
[19] Wirsing, M. (1991). Algebraic Specification. In: Handbook of Theoretical Computer Science,
Vol. B, MIT Press, pp. 675–788.
[20] Zankl, H., Felgenhauer, B., and Middeldorp, A. (2011). CSI - A confluence tool. In N. Bjørner
and V. Sofronie-Stokkermans (Eds.): CADE 2011, Lecture Notes in Computer Science,
Vol. 6803, Springer, pp. 499–505.

A

Ground-completeness proofs: DDRSes with digit append constructors

In this appendix we prove ground-completeness for the DDRSes for Zubd , Zbud , and Zdub , respectively. In all ground-confluence proofs we adopt the approach used in that of the DDRS for the
ring of Integers (see page 20).

A.1

Unary view: the DDRS for Zubd

First we show that the term rewriting system defined by the DDRS for Zubd in Table 3 is strongly
terminating. Define the following weight function |t| on closed terms over ΣZ :
|0| = 2,

|i′ | = |i| + 3 for i = 0, . . . , 8,

|S(x)| = |x| + 2,

|x : b i| = 5 · |x|7 + 1 for i = 0, 1,

|P (x)| = |x| + 5,
| − x| = |x| + 2,

|x : d i| = 29 · |x|31 + 1 for i = 0, 1, . . . , 9.

|x + y| = |x| · |y|,
|x · y| = |x||y| .
Then |t| > 1 for all closed terms over ΣZ , and it easily follows that each rewrite step on a closed
term reduces its weight. (Of course, the defining equations in the right column are superfluous:
each closed term that matches one of its left-hand sides has a unique rewrite step to one that
matches a left-hand side in the left column.)
22

Also, this rewriting systen is ground-confluent. Define the set N as follows:
N = {0} ∪ N + ∪ N − ,
N + = {S(0)} ∪ {S(t) | t ∈ N + },
N − = {−t | t ∈ N + }.
It immediately follows that if t ∈ N , then t is a normal form (no rewrite rule applies), and that
two distinct elements in N have distinct values in Z. Also, as stated in Section 2.2, the equations
in Table 3 are semantic consequences of the axioms for commutative rings (equations (1) − (8) in
Table 4). In order to prove ground-confluence we have to show that for each closed term t over
ΣZ , either t ∈ N or t has a rewrite step, so that each normal form is in N . We prove this by
structural induction on t.
The base cases are simple: if t = 0, then t ∈ N , and if t = i′ for some i ∈ {0, 1, 2, 3, 4, 5, 6, 7, 8},
then t → S(i) by equation [u15.i ]8i=0 .
For the induction step we distinguish seven cases:
1. Case t = S(r). Assume that r ∈ N and apply case distinction on r:
• if r = 0, then t ∈ N ,
• if r = S(r′ ) (thus r′ ∈ N + ), then t ∈ N ,
• if r = −S(r′ ), then t → −r′ by equation [u6].
2. Case t = P (r). Assume that r ∈ N and apply case distinction on r:
• if r = 0, then t → −S(0) by equation [u12],
• if r = S(r′ ), then t → r′ by equation [u13],
• if r = −S(r′ ), then t → −S(S(r′ )) by equation [u14].
3. Case t = −r. Assume that r ∈ N and apply case distinction on r:
• if r = 0, then t → 0 by equation [u5],
• if r = S(r′ ), then t ∈ N ,
• if r = −S(r′ ), then t → S(r′ ) by equation [u7].
4. Case t = r : b i. Now t has a rewrite step by equation [u16.i ]1i=0 .
5. Case t = r : d i. Now t has a rewrite step by equation [u17.i ]9i=0 .
6. Case t = u + r. Assume that u, r ∈ N and apply case distinction on r:
• if r = 0, then t → u by equation [u1],
• if r = S(r′ ), then t → S(u + r′ ) by equation [u2],
• if r = −S(r′ ), then apply case distinction on u:
– if u = 0, then t → r by equation [u8],
– if u = S(u′ ), then t → S(u′ + r) by equation [u9],
– if u = −S(u′ ), then t → −(S(u′ ) + S(r′ )) by equation [u10].
7. Case t = u · r. Assume that u, r ∈ N and apply case distinction on r:
• if r = 0, then t → 0 by equation [u3],
• if r = S(r′ ), then t → (u · r′ ) + u by equation [u4],
• if r = −S(r′ ), then t → −(u · r) by equation [u11].
This concludes our proof.
23

A.2

Binary view: the DDRS for Zbud

We prove that the term rewriting system defined by the DDRS for Zbud in Table 6 is groundcomplete. This rewriting system is proven strongly terminating in [14], so it remains to be proven
that it is ground-confluent and again we adopt the approach used in the proof on page 20.
Define the set N of closed terms over ΣZ as follows:
N = {0} ∪ N + ∪ N − ,
N + = {1} ∪ {t : b 0, t : b 1 | t ∈ N + },
N − = {−t | t ∈ N + }.
It immediately follows that if t ∈ N , then t is a normal form (no rewrite rule applies), and that
two distinct elements in N have distinct values in Z. Also, as stated in Section 2.2, the equations
in Tables 5 and 6 are semantic consequences of the axioms for commutative rings (equations
(1) − (8) in Table 4). In order to prove ground-confluence of this rewriting system we have to
show that for each closed term t over ΣZ , either t ∈ N or t has a rewrite step, so that each normal
form is in N . We prove this by structural induction on t.
The base cases are simple: if t ∈ {0, 1} then t ∈ N , and if t = i′ for some i ∈ {1, 2, 3, 4, 5, 6, 7, 8},
then t → S(i) by equation [b14.i ]8i=1 .
For the induction step we distinguish eight cases:
1. Case t = S(r). Assume that r ∈ N and apply case distinction on r:
• if r = 0, then t → 1 by equation [b2],
• if r = 1, then t → 1 : b 0 by equation [b3],
• if r = r′ : b 0, then t → r′ : b 1 by equation [b4],
• if r = r′ : b 1, then t → S(r′ ) : b 0 by equation [b5],
• if r = −1, then t → 0 by equation [b23],
• if r = −(r′ : b 0), then t → −(P (r′ ) : b 1) by equation [b24],
• if r = −(r′ : b 1), then t → −(r′ : b 0) by equation [b25].
2. Case t = P (r). Assume that r ∈ N and apply case distinction on r:
• if r = 0, then t → −1 by equation [b18],
• if r = 1, then t → 0 by equation [b19],
• if r = r′ : b 0, then t → P (r′ ) : b 1 by equation [b20],
• if r = r′ : b 1, then t → r′ : b 0 by equation [b21],
• if r = −1, then t → −S(1) by equation [b22],
• if r = −(r′ : b i), then t → −S(r′ : b i) by equation [b22].
3. Case t = −r. Assume that r ∈ N and apply case distinction on r:
• if r = 0, then t → 0 by equation [b16],
• if r = 1, then t ∈ N ,
• if r = r′ : b i, then t ∈ N ,
• if r = −1, then t → 1 by equation [b17],
24

• if r = −(r′ : b i), then t → r′ : b i by equation [b17].
4. Case t = r : b 0. Assume that r ∈ N and apply case distinction on r:
• if r = 0, then t → 0 by the first equation of [b1.i ]1i=0 ,
• if r = 1 or r = r′ : b i, then t ∈ N ,
• if r = −1 or r = −(r′ : b i), then t has a rewrite step by equation [b26].
5. Case t = r : b 1. Assume that r ∈ N and apply case distinction on r:
• if r = 0, then t → j by the second equation of [b1.i ]1i=0 ,
• if r = 1 or r = r′ : b i, then t ∈ N ,
• if r = −1 or r = −(r′ : b i), then t has a rewrite step by equation [b27].
6. Case t = r : d i. Now t has a rewrite step by equation [b15.i ]9i=0 .
7. Case t = u + r. Assume that u, r ∈ N and apply case distinction on r:
• if r = 0, then t → u by equation [b6],
• if r = 1, then t → S(u) by equation [b8],
• if r = r′ : b i, apply case distinction on u:
–
–
–
–
–

if
if
if
if
if

u = 0, then t → r by equation [b7],
u = 1, then t → S(r) by equation [b9],
u = u′ : b j, then t has a rewrite step according to one of [b10.i.j ]1i,j=0 ,
u = −1, then t → P (r) by equation [b29],
u = −(u′ : b j), then t has a rewrite step according to one of [b31.i.j ]1i,j=0 ,

• if r = −1, then t → P (u) by equation [b28],
• if r = −(r′ : b i), apply case distinction on u:
–
–
–
–
–

if
if
if
if
if

u = 0, then t → r by equation [b7],
u = 1, then t → S(r) by equation [b9],
u = u′ : b j, then t has a rewrite step according to one of [b30.i.j ]1i,j=0 ,
u = −1, then t → P (r) by equation [b29],
u = −(u′ : b j), then t has a rewrite step by equation [b32].

8. Case t = u · r. Assume that u, r ∈ N and apply case distinction on r:
• if r = 0, then t → 0 by equation [b11],
• if r = 1, then t → u by equation [b12],
• if r = r′ : b i, then t has a rewrite step according to one of [b13.i ]1i=0 ,
• if r = −1 or r = −(r′ : b i), then t has a rewrite step by equation [b33].
This concludes our proof.

25

A.3

Decimal view: the DDRS for Zdub

We prove that the term rewriting system defined by the DDRS for Zbud in Table 9 (using i⋆ as
defined in Table 8) is ground-complete. This rewriting system is proven strongly terminating
in [14], so it remains to be proven that it is ground-confluent.
Recall we write D for the set of all digits. Define the set N of closed terms over ΣZ as follows:
N = {0} ∪ N + ∪ N − ,
N + = D \ {0} ∪ {t : b i | t ∈ N + , i ∈ D},
N − = {−t | t ∈ N + }.
It immediately follows that if t ∈ N , then t is a normal form (no rewrite rule applies), and that
two distinct elements in N have distinct values in Z. Also, as stated in Section 2.3, the equations
in Tables 7 and 9 are semantic consequences of the axioms for commutative rings (equations
(1) − (8) in Table 4). In order to prove ground-confluence of this rewriting system we have to
show that for each closed term t over ΣZ , either t ∈ N or t has a rewrite step, so that each normal
form is in N . We prove this by structural induction on t.
The base cases are trivial: if t ∈ D, then t ∈ N .
For the induction step we distinguish eight cases:
1. Case t = S(r). Assume that r ∈ N and apply case distinction on r:
• if r = i for i ∈ {0, 1, . . . , 8}, then t → i′ by equation [d2.i ]8i=0 ,
• if r = 9, then t → 1 : d 0 by equation [d3],
• if r = r′ : d i for i ∈ {0, 1, . . . , 8}, then t → r′ : d i′ by equation [d4.i ]8i=0 ,
• if r = r′ : d 9, then t → S(r′ ) : d 0 by equation [d5],
• if r = −i′ for i ∈ {0, 1, . . . , 8}, then t → −i by equation [d22.i ]8i=0 ,
• if r = −(r′ : d 0), then t → −(P (r′ ) : d 9) by equation [d23],
• if r = −(r′ : d i′ ) for i ∈ {0, 1, . . . , 8}, then t → −(r′ : d i) by equation [d24.i ]8i=0 .
2. Case t = P (r). Assume that r ∈ N and apply case distinction on r:
• if r = 0, then t → −1 by equation [d17],
• if r = i′ for i ∈ {0, 1, . . . , 8}, then t → i by equation [d18.i ]8i=0 ,
• if r = r′ : d 0, then t → P (r′ ) : d 9 by equation [d19],
• if r = r′ : d i′ for i ∈ {0, 1, . . . , 8}, then t → r′ : d i by equation [d20.i ]8i=0 ,
• if r = −i′ for i ∈ {0, 1, . . . , 8}, then t → −S(i′ ) by equation [d21],
• if r = −(r′ : d i), then t → −S(r′ : d i) by equation [d21].
3. Case t = −r. Assume that r ∈ N and apply case distinction on r:
• if r = 0, then t → 0 by equation [d15],
• if r = i′ for i ∈ {0, 1, . . . , 8}, then t ∈ N ,
• if r = r′ : d i, then t ∈ N ,
• if r = −i′ for i ∈ {0, 1, . . . , 8}, then t → i′ by equation [d16],
• if r = −(r′ : d i), then t → r′ : d i by equation [d16].
26

4. Case t = r : d 0. Assume that r ∈ N and apply case distinction on r:
• if r = 0, then t → 0 by the first equation of [d1.i ]9i=0 ,
• if r = i′ for i ∈ {0, 1, . . . , 8}, then t ∈ N ,
• if r = r′ : d i, then t ∈ N ,
• if r ∈ N − , then t → −(r : d 0) by equation [d25].
5. Case t = r : d j for j ∈ {1, 2, . . . , 9}. Assume that r ∈ N and apply case distinction on r:
• if r = 0, then t → j by the appropriate equation of [d1.i ]9i=0 ,
• if r = i′ for i ∈ {0, 1, . . . , 8}, then t ∈ N ,
• if r = r′ : d i, then t ∈ N ,
• if r ∈ N − , then t → −(P (r) : d j ⋆ ) by one of the equations of [d26.i ]9i=1 .
6. Case t = r : b i. Now t has a rewrite step by equation [d14.i ]1i=0 .
7. Case t = u + r. Assume that u, r ∈ N and apply case distinction on r:
• if r = 0, then t → u by equation [d6],
• if r = i for i ∈ {1, 2, . . . , 9}, then t → S i (u) by equation [d8.i ]9i=1 ,
• if r = r′ : d i, apply case distinction on u:
– if u = 0, then t → r by equation [d7],
– if u = j for j ∈ {1, 2, . . . , 9}, then t → S j (r) by equation [d9.i ]9i=1 ,
– if u = u′ : d j, then t has a rewrite step according to one of [d10.i.j ]9i,j=0 ,
– if u = −j for j ∈ {1, 2, . . . , 9}, then t → P j (r) by one of [d28.i ]9i=1 ,
– if u = −(u′ : d j), then t has a rewrite step according to one of [d30.i.j ]9i,j=0 ,
• if r = −i for i ∈ {1, 2, . . . , 9}, then t → P i (u) by one of the equations of [d27.i ]9i=1 ,
• if r = −(r′ : d i), apply case distinction on u:
– if u = 0, then t → r by equation [d7],
– if u = j for j ∈ {1, 2, . . . , 9}, then t → S j (r) by one of [d9.i ]9i=1 ,
– if u = u′ : d j, then t has a rewrite step according to one of [d29.i.j ]9i,j=0 ,
– if u = −j for j ∈ {1, 2, . . . , 9}, then t → P j (r) by equation [d28.i ]9i=1 ,
– if u = −(u′ : d j), then t has a rewrite step by equation [d31].
8. Case t = u · r. Assume that u, r ∈ N and apply case distinction on r:
• if r = 0, then t → 0 by equation [d11],
• if r = i′ for i ∈ {0, 1, . . . , 8}, then t → (u · i) + u by equation [d12.i ]8i=0 ,
• if r = r′ : b i for i ∈ {0, 1, . . . , 9}, then t → ((u · r′ ) : d 0) + (u · i) by equation [d13.i ]9i=0 ,
• if r ∈ N − , then t has a rewrite step by equation [d32].
This concludes our proof.

27

B

Ground-completeness proofs: DDRSes with digit tree
constructors

In Appendix B.1 we prove ground-completeness of the DDRS for Zut , and in Appendix B.2 we
prove ground-completeness of the DDRS for Zbt .

B.1

Unary view: the DDRS for Zut

First we show that the term rewriting system defined by the DDRS for Zut in Table 11 is strongly
terminating.
Define the signature Σut = {0, −( ),
terms over Σut :

û

, +, ·} and the following weight function |t| on closed

|0| = 1,
| − x| = |x| + 1,
|x û y| = |x| + 2|y|,
|x + y| = |x| + 2|y|,
|x · y| = 2 · |x| · |y|.
Then |t| ≥ 1 for all closed terms over Σut , and it easily follows that each rewrite step on a closed
term reduces its weight.
Also, this rewriting system is ground-confluent. Define the set N as follows:
N = {0} ∪ N + ∪ N − ,
N + = {0 û 0} ∪ {t û 0 | t ∈ N + },
N − = {−t | t ∈ N + }.
It immediately follows that if t ∈ N , then t is a normal form (no rewrite rule applies), and that
two distinct elements in N have distinct values in Z. Also, as stated in Section 3.1, the equations
in Table 11 are semantic consequences of the axioms for commutative rings (equations (1) − (8)
in Table 4). In order to prove ground-confluence of the DDRS for Zut we have to show that for
each closed term t over Σut , either t ∈ N or t has a rewrite step, so that each normal form is in
N . We prove this by structural induction on t.
The base case is trivial: if t = 0, then t ∈ N .
For the induction step we distinguish four cases:
1. Case t = −r. Assume that r ∈ N and apply case distinction on r:
• if r = 0, then t → 0 by equation [ut6],
• if r = r′

û

• if r = −(r
2. Case t = v

û

0, then t ∈ N ,
′

û

0), then t → r′

û

0 by equation [ut7].

r. Assume that v, r ∈ N and apply case distinction on r:

• if r = 0, then apply case distinction on v:
– if v = 0, then t ∈ N ,

28

–
–
• if r
–
–
–
• if r
–
–
–

if v = v ′ û 0, then t ∈ N ,
if v = −(v ′ û 0), then t → −v ′ by equation [ut10].
= r′ û 0, then apply case distinction on v:
if v = 0, then t → (0 û r′ ) û 0 by equation [ut1],
if v = v ′ û 0, then t → (v û r′ ) û 0 by equation [ut1],
if v = −(v ′ û 0), then t → (−v ′ ) û r′ by equation [ut11].
= −(r′ û 0), then apply case distinction on v:
if v = 0, then t → −r′ by equation [ut8],
if v = v ′ û 0, then t → v ′ û (−r′ ) by equation [ut9],
if v = −(v ′ û 0), then t → ((v ′ + r′ ) û 0) by equation [ut12].

3. Case t = v + r. Assume that v, r ∈ N and apply case distinction on r:
• if r = 0, then t → v by equation [ut2],
• if r = r′ û 0, then t → (v + r′ ) û 0 by equation [ut3],
• if r = −(r′ û 0), then apply case distinction on v:
– if v = 0, then t → r′ by equation [ut13],
– if v = v ′ û 0, then t → v ′ + (−r′ ) by equation [ut14],
– if v = −(v ′ û 0), then t → −((v ′ û 0) + (r′ û 0)) by equation [ut15].
4. Case t = v · r. Assume that v, r ∈ N and apply case distinction on r:
• if r = 0, then t → 0 by equation [ut4],
• if r = r′ û 0, then t → (v · r′ ) + v by equation [ut5],
• if r = −(r′ û 0), then t → −(v · r) by equation [ut16].
This concludes our proof.

B.2

Binary view: the DDRS for Zbt

We prove that the term rewriting system defined by the DDRS for Zbt in Table 13 is groundcomplete. This rewriting system is proven strongly terminating in [14], so it remains to be proven
that this DDRS is ground-confluent, and we adopt the approach used in the proof on page 20.
Define the signature Σbt = {0, 1, −( ),
follows:

b̂

, +, ·}, and the set N of closed terms over Σbt as

N = {0} ∪ N + ∪ N − ,
N + = {1} ∪ {t b̂ 0, t b̂ 1 | t ∈ N + },
N − = {−t | t ∈ N + }.
It immediately follows that if t ∈ N , then t is a normal form (no rewrite rule applies), and that
two distinct elements in N have distinct values in Z. Observe that the equations in Table 13 are
semantic consequences of the axioms for commutative rings (equations (1) − (8) in Table 4). In
order to prove ground-confluence of this rewriting system we have to show that for each closed
term t over Σbt , either t ∈ N or t has a rewrite step, so that each normal form is in N . We prove
this by structural induction on t.
The base cases are simple: if t ∈ {0, 1}, then t ∈ N .
For the induction step we distinguish four cases:
29

1. Case t = −r. Assume that r ∈ N and apply case distinction on r:
• if r = 0, then t → 0 by equation [bt13],
• if r = 1, then t ∈ N ,
• if r = r′

b̂

i, then t ∈ N ,

• if r = −1, then t → 1 by equation [bt14],
• if r = −(r′

b̂

i), then t → r′

b̂

i by equation [bt14].

2. Case t = r b̂ u. Assume that r, u ∈ N and apply case distinction on r:
• if r = 0, then t → u by equation [bt1],
• if r = 1 apply case distinction on u:
–
–
–
–
–

if
if
if
if
if

u = 0, then t ∈ N ,
u = 1, then t ∈ N ,
u = u′ b̂ i, then t → (1 + u′ ) b̂ i by equation [bt2],
u = −1, then t → 1 by equation [bt15],
u = −(u′ b̂ j), then t → −((u′ + (−1)) b̂ j) by equation [bt18],

• if r = r′
–
–
–
–
–

if
if
if
if
if

b̂

i, then apply case distinction on u:

u ∈ {0, 1}, then t ∈ N ,
u = u′ b̂ j, then t → (r + u′ ) b̂ j by equation [bt2],
u = −1 and i = 0, then t → (r′ b̂ (−1)) b̂ 1 by equation [bt16],
u = −1 and i = 1, then t → (r′ b̂ 0) b̂ 1 by equation [bt17],
u = −(u′ b̂ j), then t → −((u′ + (−r)) b̂ j) by equation [bt18],

• if r = −1, then apply case distinction on u:
– if u ∈ {0, 1, −1}, then t → −(1 b̂ (−u)) by equation [bt19],
– if u = u′ b̂ j, then t → ((−1) + u′ ) b̂ j by equation [bt2],
– if u = −(u′ b̂ j), then t → −((u′ + (−(−1))) b̂ j) by equation [bt18],
• if r = −(r′

b̂

i), then t has a rewrite step by equation [bt19].

3. Case t = u + r. Assume that u, r ∈ N and apply case distinction on r:
• if r = 0, then t → u by equation [bt4],
• if r = 1, then apply case distinction on u:
–
–
–
–
–

if
if
if
if
if

u = 0, then t → 1 by equation [bt3],
u = 1, then t → (1 b̂ 0) by equation [bt5]
u = u′ b̂ j then t → u′ b̂ (j + 1) by equation [bt7],
u = −1, then t → 0 by equation [bt21],
u = −(u′ b̂ j) then t → −(u′ b̂ (j + (−1))) by equation [bt24],

• if r = r′

b̂

i, then t → r′

b̂

(u + j) by [bt6],

• if r = −1, then apply case distinction on u:
–
–
–
–

if
if
if
if

u = 0, then t → r by equation [bt3],
u = 1, then t → 0 by equation [bt20]
u = u′ b̂ j then t → u′ b̂ (j + (−1)) by equation [bt7],
u = −1, then t → −(1 b̂ 0) by equation [bt22],
30

– if u = −(u′ b̂ j) then t → −(u′ b̂ (j + (−r)) by equation [bt24],
• if r = −(r′

b̂

i), then t → −(r′

b̂

(i + (−u))) by equation [bt23].

4. Case t = u · r. Assume that u, r ∈ N and apply case distinction on r:
• if r = 0, then t → 0 by equation [bt8],
• if r = 1, then apply case distinction on u:
–
–
–
–

if
if
if
if

u = 0, then t → 0 by equation[bt9],
u = 1, then t → 1 by equation[bt10],
u = u′ b̂ j, then t → (u′ · r) b̂ (j · r) by equation[bt12],
u ∈ N − , then t has a rewrite step by equation [bt26],

• if r = r′

b̂

i, then t → (u · r′ ) b̂ (u · i) by equation [bt11],

• if r ∈ N − , then t has a rewrite step by equation [bt25].
This concludes our proof.

C

Another unary view: unary append

We briefly consider a simple alternative notation for the unary view that is related to tallying
and establishes a unary numeral system based on unary digit append. However, using only one
digit requires this digit to be 0 for the representation of zero, while the semantics of the “unary
digit append” function : u 0 requires the appended digit 0 to have value 1, that is
Jt : u 0K = JtK + 1.
Note that this mismatch does not occur in our numeral system for unary view with digit tree
constructor in Section 3.1, because in that case application of the constructor function û does
not refer to 0 as a value.
In order to solve this mismatch, we introduce the one-place function (postfix)
: u 1 : Z → Z,

the unary append,

and define the datatypes Nu′ and Zu′ based on the constant 0 and unary append. Consider the
signature Σu′ = {0, −( ), : u 1, +, ·}. In Table 19 we define a DDRS for the datatype Nu′ over
Σu′ . Of course, the phenomenon of “removing leading zeros” does not exist in this particular
unary view. Normal forms are 0 for zero, and applications of the unary append function that
define all successor values: each natural number n is represented by n applications of the unary
append to 0 and can be seen as representing a sequence of 1’s of length n having 0 as a single
prefix, e.g.
(0 : u 1) : u 1
is the normal form that represents 2.
The transition to integer numbers is straightforward. All minus instances −t of nonzero normal
forms t define the negative normal forms, e.g.
−((0 : u 1) : u 1)
is the normal form that represents −2. A DDRS that defines the extension of Nu′ to integer
numbers Zu′ is given in Table 20.
31

[u′ 1]
[u′ 2]

x+0 = x
x + (y : u 1) = (x : u 1) + y

[u′ 3]
[u′ 4]

x·0=0
x · (y : u 1) = (x · y) + x

Table 19: A DDRS for Nu′ , natural numbers in unary view with zero append
Define the following weight function |t| on closed terms over Σu′ :
|0| = 1,
| − x| = |x| + 1,
|x : u 1| = |x| + 2,
|x + y| = |x| + 2|y|,
|x · y| = 2 · |x| · |y|.
Then |t| > 0 for each closed term t and it easily follows that each rewrite step on a closed term
reduces its weight. Hence, both these DDRSes for Nu′ and Zu′ define a strongly terminating
rewriting system.
We now prove that both these DDRSes are ground-confluent. We prove this for the latter,
which implies ground-confluence of the former. Define the set N as follows:
N = {0} ∪ N + ∪ N − ,
N + = {0 : u 1} ∪ {t : u 1 | t ∈ N + },
N − = {−t | t ∈ N + }.
It immediately follows that if t ∈ N , then t is a normal form (no rewrite rule applies), and that
two distinct elements in N have distinct values in Z. Also, the equations in Table 20 are semantic
consequences of the axioms for commutative rings (equations (1) − (8) in Table 4). In order to
prove ground-confluence we have to show that for each closed term t over Σu′ , either t ∈ N or t
has a rewrite step, so that each normal form is in N . We prove this by structural induction on t.
The base case is simple: if t = 0, then t ∈ N .
For the induction step we have to distinguish four cases:

[u′ 1]
[u′ 2]

x+0 = x
x + (y : u 1) = (x : u 1) + y

[u′ 3]
[u′ 4]

x·0 = 0
x · (y : u 1) = (x · y) + x

[u′ 5]
[u′ 6]

−0 = 0
(−(x : u 1)) : u 1 = −x

[u′ 7]

−(−x) = x

[u′ 8]

0+x=x

′

[u 9]
[u′ 10]
[u′ 11]

(x : u 1) + (−(y : u 1)) = x + (−y)
(−x) + (−y) = −(x + y)
x · (−y) = −(x · y)

Table 20: A DDRS for Zu′ that specifies integer numbers in unary view with zero append

32

1. Case t = −r. Assume that r ∈ N and apply case distinction on r:
• if r = 0, then t → 0 by equation [u′ 5],
• if r = r′ : u 1, then t ∈ N ,
• if r = −(r′ : u 1), then t → r′ : u 1 by equation [u′ 7].
2. Case t = r : u 1. Assume that r ∈ N and apply case distinction on r:
• if r = 0, then t ∈ N ,
• if r = r′ : u 1, then t ∈ N ,
• if r = −(r′ : u 1), then t → −r′ by equation [u′ 6].
3. Case t = u + r. Assume that u, r ∈ N and apply case distinction on r:
• if r = 0, then t → u by equation [u′ 1],
• if r = r′ : u 1, then t → (u : u 1) + r′ by equation [u′ 2],
• if r = −(r′ : u 1), then apply case distinction on u:
– if u = 0, then t → r by equation [u′ 8],
– if u = u′ : u 1, then t → u′ + −(r′ ) by equation [u′ 9],
– if u = −(u′ : u 1), then t → −((u′ : u 1) + (r′ : u 1)) by equation [u′ 10].
4. Case t = u · r. Assume that u, r ∈ N and apply case distinction on r:
• if r = 0, then t → 0 by equation [u′ 3],
• if r = r′ : u 1, then t → (u · r′ ) + u by equation [u′ 4],
• if r = −(r′ : u 1), then t → −(u · (r′ : u 1)) by equation [u′ 11].
This concludes our proof.
Finally, we observe that writing S( ) for the unary append function : u 1 yields alternative
specifications of equal size for the datatypes Nubd and Zubd defined in Section 2.1 (Tables 2
and 3) when disregarding their equations for predecessor4 and for binary and decimal notation.
Tagging the resulting equations with [u′′ n], we observe that addition on the naturals is defined
by the two equations
[u′′ 1]
′′

[u 2]

x+0=x
x + S(y) = S(x) + y

where [u′′ 2] (as a rewrite rule) is not standard, while the extra equations used to define addition
on the integers,
[u′′ 8]
[u′′ 9]

0+x=x
S(x) + (−S(y)) = x + (−y)

[u′′ 10]

(−x) + (−y) = −(x + y)

are quite natural (only [u′′ 9] differs from [u9] in Table 3). The remaining six equations for Zu′ in
this notation define multiplication and minus, and exactly match those defined for Zubd .
4 Observe

that Zubd could have been specified without the predecessor P (x) and its three defining equations.

33

