nLab decimal numeral representation of the natural numbers

Contents

Context

Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logicset theory (internal logic of)category theorytype theory
propositionsetobjecttype
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels

semantics

Deduction and Induction

Arithmetic

Contents

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 DD be the type of decimal digits, inductively generated by the terms 0:D0:D, 1:D1:D, 2:D2:D, 3:D3:D, 4:D4:D, 5:D5:D, 6:D6:D, 7:D7:D, 8:D8:D, and 9:D9:D. The decimal numeral representation of the natural numbers Dec\mathrm{Dec} is defined as the higher inductive type generated by the function

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

the binary operation

()():Dec×DecDec(-)(-):\mathrm{Dec} \times \mathrm{Dec} \to \mathrm{Dec}

the dependent function

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

and the dependent function

q: a:Deca=0aq:\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𝟙𝟘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 𝟙𝟘 +/(a=0a)\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:Dec0:\mathrm{Dec} to be 00, and we inductively define the successor function s:DecDecs:\mathrm{Dec} \to \mathrm{Dec} as

s(a0)a1s(a 0) \coloneqq a 1
s(a1)a2s(a 1) \coloneqq a 2
s(a2)a3s(a 2) \coloneqq a 3
s(a3)a4s(a 3) \coloneqq a 4
s(a4)a5s(a 4) \coloneqq a 5
s(a5)a6s(a 5) \coloneqq a 6
s(a6)a7s(a 6) \coloneqq a 7
s(a7)a8s(a 7) \coloneqq a 8
s(a8)a9s(a 8) \coloneqq a 9
s(a9)s(a)0s(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:

00𝟘0 \neq 0 \coloneqq \mathbb{0}
0s(n)𝟙0 \neq s(n) \coloneqq \mathbb{1}
s(m)0𝟙s(m) \neq 0 \coloneqq \mathbb{1}
s(m)s(n)mns(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:

00𝟙0 \leq 0 \coloneqq \mathbb{1}
0s(n)𝟙0 \leq s(n) \coloneqq \mathbb{1}
s(m)0𝟘s(m) \leq 0 \coloneqq \mathbb{0}
s(m)s(n)mns(m) \leq s(n) \coloneqq m \leq n

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

00𝟙0 \geq 0 \coloneqq \mathbb{1}
0s(n)𝟘0 \geq s(n) \coloneqq \mathbb{0}
s(m)0𝟙s(m) \geq 0 \coloneqq \mathbb{1}
s(m)s(n)mns(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<0𝟘0 \lt 0 \coloneqq \mathbb{0}
0<s(n)𝟙0 \lt s(n) \coloneqq \mathbb{1}
s(m)<0𝟘s(m) \lt 0 \coloneqq \mathbb{0}
s(m)<s(n)m<ns(m) \lt s(n) \coloneqq m \lt n

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

0>0𝟘0 \gt 0 \coloneqq \mathbb{0}
0>s(n)𝟘0 \gt s(n) \coloneqq \mathbb{0}
s(m)>0𝟙s(m) \gt 0 \coloneqq \mathbb{1}
s(m)>s(n)m>ns(m) \gt s(n) \coloneqq m \gt n

Number of digits

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

numDigits(0)0\mathrm{numDigits}(0) \coloneqq 0
numDigits(1)1\mathrm{numDigits}(1) \coloneqq 1
numDigits(2)1\mathrm{numDigits}(2) \coloneqq 1
numDigits(3)1\mathrm{numDigits}(3) \coloneqq 1
numDigits(4)1\mathrm{numDigits}(4) \coloneqq 1
numDigits(5)1\mathrm{numDigits}(5) \coloneqq 1
numDigits(6)1\mathrm{numDigits}(6) \coloneqq 1
numDigits(7)1\mathrm{numDigits}(7) \coloneqq 1
numDigits(8)1\mathrm{numDigits}(8) \coloneqq 1
numDigits(9)1\mathrm{numDigits}(9) \coloneqq 1

and for every decimal numeral representation a0a \neq 0,

numDigits(a0)s(numDigits(a))\mathrm{numDigits}(a 0) \coloneqq s(\mathrm{numDigits}(a))
numDigits(a1)s(numDigits(a))\mathrm{numDigits}(a 1) \coloneqq s(\mathrm{numDigits}(a))
numDigits(a2)s(numDigits(a))\mathrm{numDigits}(a 2) \coloneqq s(\mathrm{numDigits}(a))
numDigits(a3)s(numDigits(a))\mathrm{numDigits}(a 3) \coloneqq s(\mathrm{numDigits}(a))
numDigits(a4)s(numDigits(a))\mathrm{numDigits}(a 4) \coloneqq s(\mathrm{numDigits}(a))
numDigits(a5)s(numDigits(a))\mathrm{numDigits}(a 5) \coloneqq s(\mathrm{numDigits}(a))
numDigits(a6)s(numDigits(a))\mathrm{numDigits}(a 6) \coloneqq s(\mathrm{numDigits}(a))
numDigits(a7)s(numDigits(a))\mathrm{numDigits}(a 7) \coloneqq s(\mathrm{numDigits}(a))
numDigits(a8)s(numDigits(a))\mathrm{numDigits}(a 8) \coloneqq s(\mathrm{numDigits}(a))
numDigits(a9)s(numDigits(a))\mathrm{numDigits}(a 9) \coloneqq s(\mathrm{numDigits}(a))

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

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

Addition of single digits

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

+0123456789
00+000 + 0 \coloneqq 00+110 + 1 \coloneqq 10+220 + 2 \coloneqq 20+330 + 3 \coloneqq 30+440 + 4 \coloneqq 40+550 + 5 \coloneqq 50+660 + 6 \coloneqq 60+770 + 7 \coloneqq 70+880 + 8 \coloneqq 80+990 + 9 \coloneqq 9
11+011 + 0 \coloneqq 11+121 + 1 \coloneqq 21+231 + 2 \coloneqq 31+341 + 3 \coloneqq 41+451 + 4 \coloneqq 51+561 + 5 \coloneqq 61+671 + 6 \coloneqq 71+781 + 7 \coloneqq 81+891 + 8 \coloneqq 91+9101 + 9 \coloneqq 10
22+022 + 0 \coloneqq 22+132 + 1 \coloneqq 32+242 + 2 \coloneqq 42+352 + 3 \coloneqq 52+462 + 4 \coloneqq 62+572 + 5 \coloneqq 72+682 + 6 \coloneqq 82+792 + 7 \coloneqq 92+8102 + 8 \coloneqq 102+9112 + 9 \coloneqq 11
33+033 + 0 \coloneqq 33+143 + 1 \coloneqq 43+253 + 2 \coloneqq 53+363 + 3 \coloneqq 63+473 + 4 \coloneqq 73+583 + 5 \coloneqq 83+693 + 6 \coloneqq 93+7103 + 7 \coloneqq 103+8113 + 8 \coloneqq 113+9123 + 9 \coloneqq 12
44+044 + 0 \coloneqq 44+154 + 1 \coloneqq 54+264 + 2 \coloneqq 64+374 + 3 \coloneqq 74+484 + 4 \coloneqq 84+594 + 5 \coloneqq 94+6104 + 6 \coloneqq 104+7114 + 7 \coloneqq 114+8124 + 8 \coloneqq 124+9134 + 9 \coloneqq 13
55+055 + 0 \coloneqq 55+165 + 1 \coloneqq 65+275 + 2 \coloneqq 75+385 + 3 \coloneqq 85+495 + 4 \coloneqq 95+5105 + 5 \coloneqq 105+6115 + 6 \coloneqq 115+7125 + 7 \coloneqq 125+8135 + 8 \coloneqq 135+9145 + 9 \coloneqq 14
66+066 + 0 \coloneqq 66+176 + 1 \coloneqq 76+286 + 2 \coloneqq 86+396 + 3 \coloneqq 96+4106 + 4 \coloneqq 106+5116 + 5 \coloneqq 116+6126 + 6 \coloneqq 126+7136 + 7 \coloneqq 136+8146 + 8 \coloneqq 146+9156 + 9 \coloneqq 15
77+077 + 0 \coloneqq 77+187 + 1 \coloneqq 87+297 + 2 \coloneqq 97+3107 + 3 \coloneqq 107+4117 + 4 \coloneqq 117+5127 + 5 \coloneqq 127+6137 + 6 \coloneqq 137+7147 + 7 \coloneqq 147+8157 + 8 \coloneqq 157+9167 + 9 \coloneqq 16
88+088 + 0 \coloneqq 88+198 + 1 \coloneqq 98+2108 + 2 \coloneqq 108+3118 + 3 \coloneqq 118+4128 + 4 \coloneqq 128+5138 + 5 \coloneqq 138+6148 + 6 \coloneqq 148+7158 + 7 \coloneqq 158+8168 + 8 \coloneqq 168+9178 + 9 \coloneqq 17
99+099 + 0 \coloneqq 99+1109 + 1 \coloneqq 109+2119 + 2 \coloneqq 119+3129 + 3 \coloneqq 129+4139 + 4 \coloneqq 139+5149 + 5 \coloneqq 149+6159 + 6 \coloneqq 159+7169 + 7 \coloneqq 169+8179 + 8 \coloneqq 179+9189 + 9 \coloneqq 18

Arithmetic left shifts

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

a0aa \ll 0 \coloneqq a
as(b)(ab)0a \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:Da:D, b:Db:D, and c:Decc:\mathrm{Dec}, ac+bc=(a+b)ca \ll c + b \ll c = (a + b) \ll c.

Digit decompositions

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

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

and

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

Addition of general decimal representations

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

b+ddigitsNotLast(b)db + d \coloneqq \mathrm{digitsNotLast}(b) d

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

a 0d 0+a 1d 1(a 0+a 1)0+(d 0+d 1)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+ad=0+a0+d=a0+d=ad0 + a d = 0 + a 0 + d = a 0 + d = a d

Addition is right unital:

ad+0=a0+d+0=a0+d=ada d + 0 = a 0 + d + 0 = a 0 + d = a d

See also

Last revised on June 10, 2022 at 00:14:57. See the history of this page for a list of all contributions to it.