Peano-Integers.tex

\documentclass{article}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage[a4paper,top=1in]{geometry}
\usepackage{multicol}
\usepackage{titling}

\newcommand{\N}{\mathbb{N}}
\newcommand{\Z}{\mathbb{Z}}

\newcommand{\ttneg}{\mathtt{neg}}
\newcommand{\ttabs}{\mathtt{abs}}
\newcommand{\ttadd}{\mathtt{add}}
\newcommand{\ttsub}{\mathtt{sub}}
\newcommand{\ttmul}{\mathtt{mul}}
\newcommand{\ttdiv}{\mathtt{div}}
\newcommand{\ttrem}{\mathtt{rem}}

\title{Peano Arithmetic for all integers\\[4pt]
\large An extension of Peano's axioms for negative numbers}

\preauthor{}
\author{}
\postauthor{\vspace{-12pt}}
\date{2021}

\begin{document}
\maketitle

Peano's axioms have been used to formalize a notion of natural numbers to start counting from 0 up to positive infinity. The axioms introduce their own data type, defined inductively as follows:
\begin{enumerate}
\item The set of natural numbers is called $\mathbb{N}$.
\item The first element of the set is 0.
\item Any other element of the set can be constructed by using $S(\cdot)$ on another element already within the set. (Here $S$ stands for successor, meaning that $S$ would provide the `next' number of the input given.)
\end{enumerate}

For simplicity and brevity the more exhaustive properties have been omitted with just the essence kept. Although the properties listed does not directly provide symbols for the more common use of natural numbers, one can easily identify $S(0)$ as 1, $S(S(0))$ as 2, and so. (One can also use $S(1)$ as 2 if 1 is defined as a symbolic shortcut for $S(0)$.)
And so, the set can be listed as a roster as follows:
\[\mathbb{N} = \left\{0, S(0), S(S(0)), S(S(S(0))), \dots\right\}\]

Addition and multiplication have then been defined on this number system, as follows:
\begin{align}
n + 0 &= n \\
m + S(b) &= S(m + b)
\end{align}
(Notice that the operations are identified between two numbers $m$ and $n$, where if one needs to deconstruct the numbers we use the following convention $m = S(a)$ and $n = S(b)$.)

While counting forwards by adding one is simple, (i.e., given any number $n$ that one has, $S$ can be called to construct the next number $S(n)$) counting backwards can be achieved with a function $P$ (for predecessor) as follows:
\begin{align}
&{} P : \N \to \N \\
&{} P(S(a)) = a
\end{align}
Notice that notation does not directly allow one to find the predecessor of a number $m$, instead it has to be identified as the successor of some other number $a$ and then the function $S$ `unwrapped'.

However, the implementation of the predecessor function creates a problem: the number 0 is not the successor of any other number in the set, and it's predecessor has to be defined differently. Either we identify $P(0) = 0$ as a valid statement, or we say that $P(0)$ is undefined within $\N$, and so not allowing $P$ to be closed within the natural numbers.

\subsection*{Starting with integers}

Moreover, notice that subtraction cannot be closed within our set either, or any implementation of the natural numbers.

To get around these problems, we extend Peano's axioms to create a set for all integers.
\begin{enumerate}
\item The set of integers is called $\Z$.
\item 0 is in the set of integers.
\item The function $S(\cdot)$ can be used on any element already within the set to produce another element.
\item The function $P(\cdot)$ can be used on any element already within the set to produce another element.
\end{enumerate}
Notice that we've included $P(\cdot)$ within the axioms to allow us negative numbers. This is because we've promoted $P(\cdot)$ from being a function to being a data constructor, a construct that we can use to create new pieces of data under a given data type (in this case, $\Z$). Notice that $S(\cdot)$ wasn't a function either, instead being a data constructor. We have to define them as such because there's no sensible codomain where $S(\cdot)$ and $P(\cdot)$ can map to, and the result of $S(\cdot)$ taking 0 is simply denoted as $S(0)$.

What is also implied by the axioms is that $S(\cdot)$ and $P(\cdot)$ work like inverses. That is, if $S$ and $P$ are called successively on some integer $n$, the would `cancel' each other out to produce the first argument. That is, $S(P(n)) = P(S(n)) = n$.\footnote{Notice that this would have not been possible under the natural numbers, since the predecessor of 0 would either have been undefined resulting in the whole stack blowing up, or a do-nothing operation in which case $S$ would have incorrectly produced $S(0)$ (or 1) for $S(P(0))$.}

The intuition behind this can be identified with the number line. With axiom 2, we can be placed in the center of the line at 0, and if we call $S$ on ourselves (and imagine ourselves to be a number), we can take one step to the right. And similarly, we can call $P$ on ourselves to go one step to the left. And since we don't have to stop at 0, we can call $P$ there to take one step to the left, landing us at $-1$ and into the world of negative numbers. The set can thus be illustrated in roster form as (only writing down the integers from $-3$ to 3 inclusive):
\[\mathbb{Z} = \left\{\dots, P(P(P(0))), P(P(0)), P(0), 0, S(0), S(S(0)), S(S(S(0))), \dots\right\}\]

\fbox{
\parbox{0.9\textwidth}{
\textbf{\large A note about canonical forms}

Since $P$ can be used to cancel out $S$ and vice versa, it makes sense to identify all numbers as a chain of calls to $P$ or $S$ until the stack ends in 0 with there being no calls to $S$ after one to $P$ or vice versa. This also allows us to quickly determine whether a number is negative or positive by simply peeking at the top constructor of the stack and seeing whether it is $P$ (negative) or $S$ (positive). However, the axioms stated do give us the freedom to chain the calls whimsically and still get a number out of it. For example, $S(S(S(S(S(P(S(P(S(P(S(P(P(P(S(0)))))))))))))))$ is just as valid an integer, and is in fact equivalent to $S(S(S(0)))$, or 3. However, trying to reason about these complicated stacks become very hard, and we therefore identify a canonical/normal form for a number. We say 0 is in canonical form, and any piece of data that only has $P$ or $S$ in its data construction/call stack is in canonical form. Any other piece of data (that mixes $P$ and $S$ in its stack) is not in canonical form. And the following function has been provided to reduce a number to its canonical form:
\begin{align*}
&{} \mathtt{simplify} : \Z \to \Z \\
&{} \mathtt{simplify} : S(P(a)) \mapsto \mathtt{simplify}(a) \\
&{} \mathtt{simplify} : P(S(a)) \mapsto \mathtt{simplify}(a) \\
&{} \mathtt{simplify} : P(a) \mapsto P(\mathtt{simplify}(a)) \\
&{} \mathtt{simplify} : S(a) \mapsto S(\mathtt{simplify}(a))
\end{align*}
Notice that the number of interest here was an integer $n$, although that was nowhere to be found. Instead, we decomposed $n$ as one of the four forms $S(P(a))$, $P(S(a))$, $P(a)$, or $S(a)$. And since a formula was impossible to provide for $\mathtt{simplify}(n) = f(n)$, we used pattern matching on the constructors instead.

Side note to a side note: although this function simplifies the construction stack, it does return the same number, and if someone were cavalier about the stacks they were working with they could simply define $\mathtt{simplify} = \operatorname{id}_{\Z}$ and call it a day.
}
}

The function provided in the box has a form that will appear a lot throughout this write-up. Since it's often impossible to work abstractly over an integer, we have to take a look at the constructors it has and work on deconstructing it. (For the natural numbers $P$ was another such function that worked by unwrapping/deconstructing constructors.)

Another such example can be found with the new predecessor and successor functions we have to define. Since we can take a step to the left by calling $P$ or removing an $S$, we can formalize the notions as follows:
\begin{multicols}{2}
\begin{align*}
&{} \mathtt{pred} : \Z \to \Z \\
&{} \mathtt{pred} : S(a) \mapsto a & (n = S(a))\\
&{} \mathtt{pred} : n \mapsto P(n)
\end{align*}

\begin{align*}
&{} \mathtt{succ} : \Z \to \Z \\
&{} \mathtt{succ} : P(a) \mapsto a & (n = P(a))\\
&{} \mathtt{succ} : n \mapsto S(n)
\end{align*}
\end{multicols}
The usage of $\mathtt{pred}$ and $\mathtt{succ}$ simplifies our lives by letting the call stacks stay uncluttered, but they don't detect if a number is not in canonical form. And so, for the rest of this article, any functions we define will simply assume the numbers are in canonical form to simplify computations.

Another thing to note here is that the order in which the statements appear matter. After the domain and codomain definition, the first line checks whether the number $n$ has the form $P(a)$ or $S(a)$. If it doesn't, we go to the last line of the definition which cares about all other forms the numbers can take. The accompanying file \texttt{PeanoInts.hs} makes good use of this, which is provided by the pattern matching construct in Haskell. In Haskell a piece of input data can be matched against several patterns (where all pieces of data are generated by using constructors like the ones here) and the first matching constructor pattern is used. This allows the latter patterns to be simpler, since we can make particular assumptions as earlier patterns have been discarded.\footnote{The most obvious example of this is found when checking for 0 when we implement our division algorithm.}

\vspace{4pt}

\fbox{
\parbox{0.9\linewidth}{
\textbf{\large Cutting the monotony with two simple algorithms}

To get away from the dry talk of algorithms and functions, I bring you two new algorithms and functions. This time, the ideas are so simple that you can read passively while thinking about whether you filed your tax papers correctly.

The first function we take a look at is negation, identified by $\mathtt{neg}$ which negates a number. It works as follows:
\begin{align*}
&{} \ttneg : \Z \to \Z \\
&{} \ttneg(n) = \begin{cases}
0 & \text{if} ~ n = 0 \\
P(\ttneg(a)) & \text{if} ~ n ~ \text{has the form} ~ S(a) \\
S(\ttneg(a)) & \text{if} ~ n ~ \text{has the form} ~ P(a)
\end{cases}
\end{align*}
Also, I used the usual mathematical case-by-case description of a function to show what it may look like, but it involves more typing on my part and so I'm foregoing it for all other functions except the two here.

The second function is the absolute value operation, which simply flips all the $P$ in a stack to $S$.
\begin{align*}
&{} \ttabs : \Z \to \Z \\
&{} \ttabs(n) = \begin{cases}
S(\ttabs(a)) & \text{if} ~ n ~ \text{has the form} ~ P(a) \\
n & \text{otherwise}
\end{cases}
\end{align*}
}
}

\subsection*{Starting with the arithmetic}
Now that our numbers have been defined and we know how to navigate over them, let's start by abstracting away some of that navigation by defining the four basic arithmetic operations.

\subsubsection*{Addition}
The first one is addition, implemented by the $\ttadd$ function. The syntax equivalence is $\ttadd(a, b) = a + b$.\footnote{The definitions on the right are only to make commutativity explicit and can be safely ignored.}
\begin{align*}
&{} \ttadd : \Z \times \Z \to \Z \\
&{} \ttadd : (n, 0) \mapsto n &
&{} \ttadd : (0, n) \mapsto n \\
&{} \ttadd : (P(a), S(b)) \mapsto \ttadd(a, b) &
&{} \ttadd : (S(a), P(b)) \mapsto \ttadd(a, b) \\
&{} \ttadd : (P(a), P(b)) \mapsto \ttadd(a, P(P(b))) \\
&{} \ttadd : (S(a), S(b)) \mapsto \ttadd(a, S(S(b)))
\end{align*}
The first line refers to the use of 0 as the additive identity. The second line matches one number as negative and one number as positive.   We make the decompositions $m = a - 1$ and $n = b + 1$. This allows $m + n = a - 1 + b + 1 = a + b$. This also minimizes the depth of the stack and eventually it reduces down with either side being 0 and the whole computation being reduced to the additive identity. The $(m, n)$ both negative and $(m, n)$ both positive cases work the same way, where we remove one layer of $P$ or $S$ call from one integer to give to the other integer.

\subsubsection*{Subtraction}
TODO: write-up
\begin{align*}
&{} \ttsub : \Z \times \Z \to \Z \\
&{} \ttsub : (m, 0) \mapsto m \\
&{} \ttsub : (0, m) \mapsto \ttneg(n) \\
&{} \ttsub : (m, P(b)) \mapsto \ttadd(m, \ttneg(P(b))) \\
&{} \ttsub : (S(a), S(b)) \mapsto \ttsub(a, b) \\
&{} \ttsub : (P(a), S(b)) \mapsto P(P(\ttsub(a, b)))
\end{align*}

More simply,
\[ \ttsub : (m, n) \mapsto \ttadd(m, \ttneg(n)) \]

\subsubsection*{Multiplication}
TODO: write-up
\begin{align*}
&{} \ttmul : \Z \times \Z \to \Z \\
&{} \ttmul : (m, 0) \mapsto 0 &
&{} \ttmul : (0, n) \mapsto 0 \\
&{} \ttmul : (m, S(0)) \mapsto m &
&{} \ttmul : (S(0), n) \mapsto n \\
&{} \ttmul : (m=S(a), S(b)) \mapsto \ttadd(m, \ttmul(m, b)) \\
&{} \ttmul : (m=P(a), n=P(b)) \mapsto \ttmul(\ttneg(m), \ttneg(n)) \\
&{} \ttmul : (m=S(a), n=P(b)) \mapsto \ttneg(\ttmul(m, \ttneg(n))) \\
&{} \ttmul : (m=P(a), n=S(b)) \mapsto \ttmul(n, m)
\end{align*}

\subsection*{Division}
TODO: write-up
\begin{align*}
&{} \ttdiv : \Z \times \Z \to \Z \\
&{} \ttdiv : (m, 0) \mapsto \mathtt{undefined} \\
&{} \ttdiv : (0, n) \mapsto 0 \\
&{} \ttdiv : (m, S(0)) \mapsto m \\
&{} \ttdiv : (m=P(a), n=P(b)) \mapsto \ttdiv(\ttneg(m), \ttneg(n)) \\
&{} \ttdiv : (m=P(a), n=S(b)) \mapsto \ttneg(\ttdiv(\ttneg(m)), n) \\
&{} \ttdiv : (m=S(a), n=P(b)) \mapsto \ttneg(\ttdiv(m, \ttneg(n))) \\
&{} \ttdiv : (m, n) \mapsto \begin{cases}
0 & \text{if} ~ m < n \\
S(\ttdiv(\ttsub(m, n), n)) & \text{otherwise}
\end{cases}
\end{align*}

\subsection*{Bonus: Remainder}
TODO: write-up
\begin{align*}
&{} \ttrem : \Z \times \Z \to \Z \\
&{} \ttrem : (m, 0) \mapsto \mathtt{undefined} \\
&{} \ttrem : (0, n) \mapsto 0 \\
&{} \ttrem : (m, S(0)) \mapsto 0 \\
&{} \ttrem : (m=S(a), n=P(b)) \mapsto \ttrem(m, \ttneg(n)) \\
&{} \ttrem : (m=P(a), n=S(b)) \mapsto \ttneg(\ttrem(\ttneg(m), n)) \\
&{} \ttrem : (m=P(a), n=P(b)) \mapsto \ttneg(\ttrem(\ttneg(m), \ttneg(n))) \\
&{} \ttrem : (m, n) \mapsto \begin{cases}
m & \text{if} ~ m < n \\
\ttrem(\ttsub(m, n), n) & \text{otherwise}
\end{cases}
\end{align*}

Concisely,
\[ \ttrem(m, n) = \ttsub(m, \ttmul(n, \ttdiv(m, n))) \]

\subsection*{Double bonus: Sign/Signum function}
TODO: write-up
\begin{align*}
&{} \mathtt{sgn} : \Z \times \Z \to \Z \\
&{} \mathtt{sgn} : 0 \mapsto 0 \\
&{} \mathtt{sgn} : P(a) \mapsto P(1) \\
&{} \mathtt{sgn} : S(a) \mapsto S(1) \\
\end{align*}

\end{document}