nLab decimal numeral representation of the natural numbers

Idea

The decimal numeral representation of the natural numbers as strings of digits as familiar from school mathematics, with mathematical operations directly defined on the strings of digits.

 Definition

In type theory

Let $D$ be the type of decimal digits, inductively generated by the terms $0:D$, $1:D$, $2:D$, $3:D$, $4:D$, $5:D$, $6:D$, $7:D$, $8:D$, and $9:D$. The decimal numeral representation of the natural numbers $\mathrm{Dec}$ is defined as the higher inductive type generated by the function

$$(-):D \to \mathrm{Dec}$$

the binary operation

$$(-)(-):\mathrm{Dec} \times \mathrm{Dec} \to \mathrm{Dec}$$

the dependent function

$$p:\prod_{a:\mathrm{Dec}} \prod_{b:\mathrm{Dec}} \prod_{c:\mathrm{Dec}} (a b) c = a (b c)$$

and the dependent function

$$q:\prod_{a:\mathrm{Dec}} a = 0 a$$

In Coq-syntax the decimal digits and the decimal representation of the natural numbers are the (higher) inductive types defined by

Inductive DecDigits : Type :=
 | zero : DecDigits
 | one : DecDigits
 | two : DecDigits
 | three : DecDigits
 | four : DecDigits
 | five : DecDigits
 | six : DecDigits
 | seven : DecDigits
 | eight : DecDigits
 | nine : DecDigits

Inductive Dec : Type :=
 | digit : DecDigits -> Dec
 | cat : Dec -> Dec -> Dec
 | assoc : forall (a,b,c : DecDigits) cat cat a b c == cat a cat b c
 | lead-zero : forall (a : Dec) a == cat digit zero a

As a quotient set

Let

$$\mathbb{10} \coloneqq \mathbb{1} \uplus \mathbb{1} \uplus \mathbb{1} \uplus \mathbb{1} \uplus \mathbb{1} \uplus \mathbb{1} \uplus \mathbb{1} \uplus \mathbb{1} \uplus \mathbb{1} \uplus \mathbb{1}$$

be the disjoint union of 10 singletons, with an element $0 \in \mathbb{10}$ and let $\mathbb{10}^+$ be the free semigroup on $\mathbb{10}$. Then the set of decimal numeral representations of the natural numbers is the quotient set $\mathbb{10}^+/(a = 0 a)$.

 Properties

Zero and successor

The decimal numeral representation of the natural numbers is a natural numbers object in Set: We define $0:\mathrm{Dec}$ to be $0$, and we inductively define the successor function $s:\mathrm{Dec} \to \mathrm{Dec}$ as

$$s(a 0) \coloneqq a 1$$

$$s(a 1) \coloneqq a 2$$

$$s(a 2) \coloneqq a 3$$

$$s(a 3) \coloneqq a 4$$

$$s(a 4) \coloneqq a 5$$

$$s(a 5) \coloneqq a 6$$

$$s(a 6) \coloneqq a 7$$

$$s(a 7) \coloneqq a 8$$

$$s(a 8) \coloneqq a 9$$

$$s(a 9) \coloneqq s(a) 0$$

Inequalities

The denial inequality tight apartness relation $\neq$ called not equal to is inductively defined for decimal numeral representations of the natural numbers in the same way that it is inductively defined for natural numbers:

$$0 \neq 0 \coloneqq \mathbb{0}$$

$$0 \neq s(n) \coloneqq \mathbb{1}$$

$$s(m) \neq 0 \coloneqq \mathbb{1}$$

$$s(m) \neq s(n) \coloneqq m \neq n$$

The total order relation $\leq$ called less than or equal to is inductively defined for decimal numeral representations of the natural numbers in the same way that it is inductively defined for natural numbers:

$$0 \leq 0 \coloneqq \mathbb{1}$$

$$0 \leq s(n) \coloneqq \mathbb{1}$$

$$s(m) \leq 0 \coloneqq \mathbb{0}$$

$$s(m) \leq s(n) \coloneqq m \leq n$$

The opposite total order $\geq$ called greater than or equal to is inductively defined as

$$0 \geq 0 \coloneqq \mathbb{1}$$

$$0 \geq s(n) \coloneqq \mathbb{0}$$

$$s(m) \geq 0 \coloneqq \mathbb{1}$$

$$s(m) \geq s(n) \coloneqq m \geq n$$

The strict linear order relation $\lt$ called less than is inductively defined for decimal numeral representations of the natural numbers in the same way that it is inductively defined for natural numbers:

$$0 \lt 0 \coloneqq \mathbb{0}$$

$$0 \lt s(n) \coloneqq \mathbb{1}$$

$$s(m) \lt 0 \coloneqq \mathbb{0}$$

$$s(m) \lt s(n) \coloneqq m \lt n$$

The opposite strict linear order $\gt$ called greater than is inductively defined as

$$0 \gt 0 \coloneqq \mathbb{0}$$

$$0 \gt s(n) \coloneqq \mathbb{0}$$

$$s(m) \gt 0 \coloneqq \mathbb{1}$$

$$s(m) \gt s(n) \coloneqq m \gt n$$

Number of digits

Each decimal numeral representation has an associated number of digits, a function $\mathrm{numDigits}:\mathrm{Dec} \to \mathrm{Dec}$ inductively defined as

$$\mathrm{numDigits}(0) \coloneqq 0$$

$$\mathrm{numDigits}(1) \coloneqq 1$$

$$\mathrm{numDigits}(2) \coloneqq 1$$

$$\mathrm{numDigits}(3) \coloneqq 1$$

$$\mathrm{numDigits}(4) \coloneqq 1$$

$$\mathrm{numDigits}(5) \coloneqq 1$$

$$\mathrm{numDigits}(6) \coloneqq 1$$

$$\mathrm{numDigits}(7) \coloneqq 1$$

$$\mathrm{numDigits}(8) \coloneqq 1$$

$$\mathrm{numDigits}(9) \coloneqq 1$$

and for every decimal numeral representation $a \neq 0$,

$$\mathrm{numDigits}(a 0) \coloneqq s(\mathrm{numDigits}(a))$$

$$\mathrm{numDigits}(a 1) \coloneqq s(\mathrm{numDigits}(a))$$

$$\mathrm{numDigits}(a 2) \coloneqq s(\mathrm{numDigits}(a))$$

$$\mathrm{numDigits}(a 3) \coloneqq s(\mathrm{numDigits}(a))$$

$$\mathrm{numDigits}(a 4) \coloneqq s(\mathrm{numDigits}(a))$$

$$\mathrm{numDigits}(a 5) \coloneqq s(\mathrm{numDigits}(a))$$

$$\mathrm{numDigits}(a 6) \coloneqq s(\mathrm{numDigits}(a))$$

$$\mathrm{numDigits}(a 7) \coloneqq s(\mathrm{numDigits}(a))$$

$$\mathrm{numDigits}(a 8) \coloneqq s(\mathrm{numDigits}(a))$$

$$\mathrm{numDigits}(a 9) \coloneqq s(\mathrm{numDigits}(a))$$

We define the type of decimal numeral representations with $n$-digits as the fiber of $\mathrm{numDigits}$ at $n$:

$$representationsWithNumDigits(n) \coloneqq \sum_{a:\mathrm{Dec}} \mathrm{numDigits}(a) = n$$

Addition of single digits

Addition $(-)+(-):D \times D \to \mathrm{Dec}$ of two digits is inductively defined as

+	0	1	2	3	4	5	6	7	8	9
0	$0 + 0 \coloneqq 0$	$0 + 1 \coloneqq 1$	$0 + 2 \coloneqq 2$	$0 + 3 \coloneqq 3$	$0 + 4 \coloneqq 4$	$0 + 5 \coloneqq 5$	$0 + 6 \coloneqq 6$	$0 + 7 \coloneqq 7$	$0 + 8 \coloneqq 8$	$0 + 9 \coloneqq 9$
1	$1 + 0 \coloneqq 1$	$1 + 1 \coloneqq 2$	$1 + 2 \coloneqq 3$	$1 + 3 \coloneqq 4$	$1 + 4 \coloneqq 5$	$1 + 5 \coloneqq 6$	$1 + 6 \coloneqq 7$	$1 + 7 \coloneqq 8$	$1 + 8 \coloneqq 9$	$1 + 9 \coloneqq 10$
2	$2 + 0 \coloneqq 2$	$2 + 1 \coloneqq 3$	$2 + 2 \coloneqq 4$	$2 + 3 \coloneqq 5$	$2 + 4 \coloneqq 6$	$2 + 5 \coloneqq 7$	$2 + 6 \coloneqq 8$	$2 + 7 \coloneqq 9$	$2 + 8 \coloneqq 10$	$2 + 9 \coloneqq 11$
3	$3 + 0 \coloneqq 3$	$3 + 1 \coloneqq 4$	$3 + 2 \coloneqq 5$	$3 + 3 \coloneqq 6$	$3 + 4 \coloneqq 7$	$3 + 5 \coloneqq 8$	$3 + 6 \coloneqq 9$	$3 + 7 \coloneqq 10$	$3 + 8 \coloneqq 11$	$3 + 9 \coloneqq 12$
4	$4 + 0 \coloneqq 4$	$4 + 1 \coloneqq 5$	$4 + 2 \coloneqq 6$	$4 + 3 \coloneqq 7$	$4 + 4 \coloneqq 8$	$4 + 5 \coloneqq 9$	$4 + 6 \coloneqq 10$	$4 + 7 \coloneqq 11$	$4 + 8 \coloneqq 12$	$4 + 9 \coloneqq 13$
5	$5 + 0 \coloneqq 5$	$5 + 1 \coloneqq 6$	$5 + 2 \coloneqq 7$	$5 + 3 \coloneqq 8$	$5 + 4 \coloneqq 9$	$5 + 5 \coloneqq 10$	$5 + 6 \coloneqq 11$	$5 + 7 \coloneqq 12$	$5 + 8 \coloneqq 13$	$5 + 9 \coloneqq 14$
6	$6 + 0 \coloneqq 6$	$6 + 1 \coloneqq 7$	$6 + 2 \coloneqq 8$	$6 + 3 \coloneqq 9$	$6 + 4 \coloneqq 10$	$6 + 5 \coloneqq 11$	$6 + 6 \coloneqq 12$	$6 + 7 \coloneqq 13$	$6 + 8 \coloneqq 14$	$6 + 9 \coloneqq 15$
7	$7 + 0 \coloneqq 7$	$7 + 1 \coloneqq 8$	$7 + 2 \coloneqq 9$	$7 + 3 \coloneqq 10$	$7 + 4 \coloneqq 11$	$7 + 5 \coloneqq 12$	$7 + 6 \coloneqq 13$	$7 + 7 \coloneqq 14$	$7 + 8 \coloneqq 15$	$7 + 9 \coloneqq 16$
8	$8 + 0 \coloneqq 8$	$8 + 1 \coloneqq 9$	$8 + 2 \coloneqq 10$	$8 + 3 \coloneqq 11$	$8 + 4 \coloneqq 12$	$8 + 5 \coloneqq 13$	$8 + 6 \coloneqq 14$	$8 + 7 \coloneqq 15$	$8 + 8 \coloneqq 16$	$8 + 9 \coloneqq 17$
9	$9 + 0 \coloneqq 9$	$9 + 1 \coloneqq 10$	$9 + 2 \coloneqq 11$	$9 + 3 \coloneqq 12$	$9 + 4 \coloneqq 13$	$9 + 5 \coloneqq 14$	$9 + 6 \coloneqq 15$	$9 + 7 \coloneqq 16$	$9 + 8 \coloneqq 17$	$9 + 9 \coloneqq 18$

Arithmetic left shifts

There is a binary operation $(-) \ll (-):\mathrm{Dec} \times \mathrm{Dec} \to \mathrm{Dec}$ called the arithmetic left shift inductively defined as

$$a \ll 0 \coloneqq a$$

$$a \ll s(b) \coloneqq (a \ll b) 0$$

This binary operation is also called multiplication by a power of ten.

Arithmetic left shifts of digits is left distributive over addition: given $a:D$, $b:D$, and $c:\mathrm{Dec}$, $a \ll c + b \ll c = (a + b) \ll c$.

Digit decompositions

Given a decimal numeral representation $b$, there exists functions $\mathrm{digitsNotLast}:\mathrm{Dec} \to \mathrm{Dec}$ and $\mathrm{lastDigit}:\mathrm{Dec} \to D$ such that

$$b = \mathrm{digitsNotLast}(b) \mathrm{lastDigit}(b)$$

and

$$\mathrm{numDigits}(b) = s(\mathrm{digitsNotLast}(b))$$

Addition of general decimal representations

Given a decimal numeral representation $b$ such that $\mathrm{lastDigit}(b) = 0$, the sum of $b$ and a digit $d$ is defined as

$$b + d \coloneqq \mathrm{digitsNotLast}(b) d$$

Given two decimal numeral representations of the natural numbers $a_0 d_0$ and $a_1 d_1$ with $d_0$ and $d_1$ being digits and $a_0$ and $a_1$ being decimal numeral representations, addition is inductively defined as

$$a_0 d_0 + a_1 d_1 \coloneqq (a_0 + a_1) 0 + (d_0 + d_1)$$

The decimal numeral representation of the natural numbers is a commutative monoid object in Set:

Addition is left unital:

$$0 + a d = 0 + a 0 + d = a 0 + d = a d$$

Addition is right unital:

$$a d + 0 = a 0 + d + 0 = a 0 + d = a d$$

See also

• natural numbers

• natural numbers type

• inductive type

• higher inductive type

• infinite decimal representation of a unit interval