We'll be playing different tunes in this blog. To begin, we'll cover the origins of Peano arithmetic, its applications in functional programming, and examples.
Yes, I did mix up piano and Peano when I first heard of Peano arithmetic. In my defense, I wasn't the only one. Before we jump right to Peano arithmetic applied in Haskell, lets cover the origins of Peano arithmetic.
The Godfather of Pianos. Sorry, Peano.
Peano axioms, also known as Peano's postulates were named after Italian mathematician Giuseppe Peano (I didn't see that one coming). Introduced in the 19th century by Peano, the Peano postulates provided a foundation for natural numbers. Natural numbers begin with 0 and its successors follow right after it.
Here's a basic picture of natural numbers:
Moshier, Contemporary Discrete Mathematics p. 13
What's so interesting about Peano axioms is its ability to "...enable an infinite set to be generated by a finite set of symbols and rules..."( Britanna, Peano axioms). However, Peano axioms were not simply accepted by the mathematical community when introduced. Like any scientist formulating a hypothesis, there had to be investigations before formalizing. Indeed, there have been a number of mathematical investigations over Peano arithmetic and propositions to further its definition. A few noteworthy mathematicians are the following, "...Hermann Grassmann, who showed in the 1860s that many facts in arithmetic could be derived from more basic facts about the successor operation and induction.[1] In 1881, Charles Sanders Peirce provided an axiomatization of natural-number arithmetic.[2] In 1888, Richard Dedekind proposed another axiomatization of natural-number arithmetic, and in 1889, Peano published a simplified version of them as a collection of axioms in his book, The principles of arithmetic presented by a new method (Latin: Arithmetices principia, nova methodo exposita)." (Wiki).
What's the significance of Peano arithmetic?
When I first applied Peano axioms for arithmetic in Haskell, I found that Haskell's type system is central to the language. Peano arithmetic is the gateway to defining the most basic of arithmetic concepts that are recursively defined. Here's a quick review of Peano:
Peano-Dedekind axiom postulates that (Chicago.edu)
0 is a natural number
0 is not a successor
s is a one-one function from the natural numbers to natural numbers(NN), i.e. for all NN a, s(a) is also a NN, moreover,
for all NN a and b, if s(a) = s(b) then a = b
every NN is either 0 or a successor i.e., for all a, a = 0 or there exists b such that a = s(b).
Now that we've touched on the history of the Peano axiom and what it entails, let us examine an example on Peano arithmetic in Haskell. However, remember from my first blog (Haskell's Got Style) when I said that discrete mathematics would come in handy? Yes, we're going to apply discrete mathematics to our example first before we implement it in Haskell. You'll finally see the symmetry that I've been babbling about and hopefully, in the process, you'll recognize discrete's importance.
Examples
Our example will cover the most basic arithmetic operation that you've known since grade school - addition.
Moshier, Contemporary Discrete Mathematics p. 20
Just like recursion, we have our base case: m + 0 = m. Our base case tells us that any natural number plus 0 would equal itself. In the second case, m + k_next , k_next(note, the _next is the curved arrow) is in successor notation. Generally, the successor operation (the curved arrow) takes the natural number k and send it to the one that succeeds it. For instance, 2 abbreviates to 0_next_next.
Here's a practical example of the addition algorithm in discrete mathematics:
0 * 2 = 0 * 0_next_next [2 abbreviates to 0_next_next ]
= 0 + (o *o_next) [ note that m * k_next = m + (m * k) ]
= 0 + (0 + (0 * 0) ) [ same reason]
= 0 + (0 + 0) [ m * 0 = 0 ]
= 0 + 0 [ m + 0 = m ]
= 0 [ same reason]
Now we'll code the addition algorithm in Haskell.
Data is a keyword in Haskell used to define a data type like a typedef in C or C++.
What this line does is to define the natural numbers (NN).
-- data type as being 0 or a successor to NN.
`data NN = O | S NN`
The statement below simply allows us to display our result in the console.
`deriving (Eq,Show)`
The function add takes in 2 arguments and outputs one result. As stated before, NN stands for a natural number.
`add :: NN -> NN -> NN`
Just like discrete, we have to define our base case m + 0, where any number n plus O is itself. Note that the 'O' used in our function add is not the number zero. Then in our second case, 'S' stands for successor. Analogous to discrete definition of addition, m + k_next = (m + k)_next, 'S' represents our successor. Again, we are using Peano numbers.
`add O n = n`
`add (S n) m = S (add n m)`
How would you test this in command line?
Write this as the input in the command line.
add (S O) (S (S O))
It should output the following:
S(S(S(O)))
Here's a short explanation of what just happened
We know that anything plus 'O' is itself.
Given: add(S O) (S(S O)),
add(S O) must equal S
Result: Thus the output will be: S(S(S(O)))
If we were to view this from a numeric system, add(S O) (S(S O)) would be viewed as 1 + 2
this is equal to S(S(S(O))) = 3
Another example that we can test with Peano numbers is the multiplication algorithm.
-- for the third line-->
Lets there be two natural numbers 5 and 3, we can use our add function from the previous example when approaching this problem. Recall that if we add 5 three times (5 + 5 + 5), it yields our solution 15.
mult :: NN -> NN -> NN
mult O n = O
mult (S n) m = add m (mult n m)
How would you test this in command line?
Write this as the input in the command line. In this case we're checking that 2 *3.
mult (S (S O)) (S (S ( S O)))
The output should return
S (S ( S ( S (S (S O ) ) ) ) )
This is equivalent to 6.
The above examples demonstrate the relation between discrete, functional programming, how functions can be used as arguments in another function, and the applications of the Peano axiom. But most importantly, we learned that Peano is not the same thing as piano.
Next week's blog:
Must Reads
Contemporary Discrete Mathematics by Andrew Moshier
References
Contemporary Discrete Mathematics by Andrew Moshier
Britannica: https://www.britannica.com/science/Peano-axioms
Alexander Kurz's Guide to Programming Languages (link below) : https://github.com/alexhkurz/programming-languages-2020/blob/master/lecture-by-lecture.md
Comments