Peano's Axioms Part II: Orderability and Code

So, lets get started with this Peano arithmetic stuff. For those who do not know what Peano's axioms are, heres a brief explaination.

Peano's Axioms define a formal system for deriving arithmetic operations and procedures over the set of "Natural" numbers. Peanos Axiom's are most often stated as follows, though variants do exist.

1) 0 is a natural number. (Base Case)
2) If x is a natural number, S x is a natural number (Successor)
3) There is no number S x = 0 (0 is the successor of no number)
4a) 0 is only equal to 0.
4b) Two natural numbers Sx and Sy are equal iff x and y are equal.
4c) If x,y are natural numbers, then either (x == y /\ y == x) or (x /= y /\ y /= x)
5) If you have a subset K, and 0 is in K. Then if some Proposition P holds for 0, and Sx for all x in K, then K contains the naturals. (Induction, from Wikipedia)

(see Peano's Axioms Wikipedia Entry)

The goal of this post is to define Equality, Orderability, and basic arithmetic over the Naturals. We'll also see how the standard Peano numbers. Lets talk about Orderability, for a second.

Equality is provided for by the axioms, but what is orderability? When we think about something being ordered, we can think about a "total" ordering, or a "partial" ordering. A Total Ordering is one that satisfies the following conditions.

For some Binary relation R(x,y), (notated xRy),
1) R is antisymmetric:
(xRy /\ yRx) iff (x==y), where == is equality.
2) R is transitive:
if (aRb /\ bRc) then (aRc)
3) and R is total:
(xRy \/ yRx)

a partial order only lacks in the third axiom. What does all this mean though? Well, axiom 1 gives us an important link to equality. We can actually use this fact to either define Equality from Orderability, or vice versa. Also, Axiom 1 gives us the ability to make the MRD for the Ord class very succint, only requiring (<=) at the very least. In Haskell, the Ord class is a subclass of Eq, so we need to define equality first in Haskell. This is not a problem, as we can always use Axiom 1 to define an equality function retroactively. That is, define (<=) as a function external to the type class, over the naturals. Then define (==) as ((x<=y)&&(y<=x)). We can then instance the both classes together. Axiom 2 is pretty self explainatory, it allows us to infer an ordering of two elements from two separate orderings. One neat thing this does, that not many people point out, is this is the axiom that allows for the concept of sorting. Since effectively, when we sort, we want to chain orderings together so we can have a list with elements of the type with the property of: k_1 <= k_2 &&amp;amp; k_2 <= k_3 && ... && k_(n-1) <= k_n => k_1 <= k_n that is, element 1 is less than element 2, and so on, such that the first element of the list is ordered with the last. It's relatively trivial to realize, so much so that most people don't even bother to mention it, but it certainly is interesting to see. Axiom 3 is the defining feature of total orderings, it's similar to the law of the excluded middle. We can see how certain relations are non-total, take for instance the relation (<). That is, the relation x < sx ="=" sy ="=">
> {-# OPTIONS -fglasgow-exts #-}
> module Peano (Nat(..), one, p,
>    iton, ntoi, natToInteger,
>    integerToNat) where

=============================================
Defining Arithmetic based on Peano's Axioms
=============================================

===============================================================================
First, we'll define Nat, the set of natural numbers w/ 0,

This covers Axiom 1,2, and 3.

> data Nat = Z | S Nat
>   deriving Show

This encodes the concept of Natural Numbers, we aren't going to use Haskell's
deriving capabilities for Eq, but Show thats fine, it'd just be
tedious.


Handy bits.

> one :: Nat
> one = (S Z)



===============================================================================
Now lets build up Eq, the Equality of two numbers, this covers Axioms
2,3,4,5,7, and 8


> instance Eq Nat where

every number is equal to itself, we only need to define it for Zero, the rest
will come w/ recursion for free.

>   Z == Z = True

No number's successor equals zero, and the inverse is also true, zero is the
successor of no number

>   S x == Z = False -- no successor to zero
>   Z == S x = False -- zero is no number's successor

Two numbers are equal iff there successors are equal, here, we state it
backwards,

>   S x == S y = (x == y)

And that, my friends, it Eq for Nat

===============================================================================

Now, lets define orderability, these two things will give us some extra power
when pushing Nat into Num.

> instance Ord Nat where
>   compare Z Z = EQ
>   compare (S x) Z = GT
>   compare Z (S x) = LT
>   compare (S x) (S y) = compare x y

Easy as pie, follows from Axioms 1,2 and 8.
===============================================================================

Now, we can push this bad boy into Num, which will give us all your basic
arithmetic functions

First, lets write (p), the magic predecessor function

> p :: Nat -> Nat
> p Z = Z -- A kludge, we're at the limit of the system here.
>    -- We'll come back to this when we start playing with ZZ
>    -- (the integers)
> p (S x) = x

=======================================

Heres (+) in terms of repeated incrementing.

> addNat :: Nat -> Nat -> Nat

First, we know that Z + Z = Z, but that will follow from the following
definitions

> addNat x Z = x
> addNat Z y = y
> addNat (S x) (S y)
>   | (S x) <= (S y) = addNat x (S (S y)) > | otherwise = addNat y (S (S x))

=======================================

Heres (*)

> mulNat :: Nat -> Nat -> Nat

Simple, here are our rules
y' = y
Z * Sx = Sx * Z = Z
SZ * Sx = Sx * SZ = x
Sx * y = (x) * (y+y')


> mulNat _ Z = Z
> mulNat Z _ = Z
> mulNat a b
>   | a <= b = mulNat' a b b > | otherwise = mulNat' b a a
>   where
>    mulNat' x@(S a) y orig
>     | x == one = y
>     | otherwise = mulNat' a (addNat orig y) orig


=======================================

We're gonna stop and do integerToNat and natToInteger just quick.

> natToInteger :: Integral a => Nat -> a
> natToInteger Z = 0
> natToInteger (S x) = 1 + (natToInteger x)

easy enough, heres integerToNat

> integerToNat :: Integral a => a -> Nat
> integerToNat 0 = Z
> integerToNat k = S (integerToNat (k-1))


pretty nice, huh? Lets add a couple of aliases.

> iton = integerToNat
> ntoi = natToInteger

=======================================

Now we just need (-), we'll talk about abs and signum in a second

> subNat :: Nat -> Nat -> Nat
> subNat x Z = x
> subNat Z x = Z
> subNat x y
>   | x <= y = Z > | otherwise = subNat (p x) (p y)

=======================================

Few, after all that, we just need to define signum. abs is pointless in Nat,
because all numbers are either positive or Z,

so signum is equally easy. since nothing is less than Z, then we know the
following

> sigNat :: Nat -> Nat
> sigNat Z = Z
> sigNat (S x) = one

and abs is then just id on Nats

> absNat :: Nat -> Nat
> absNat = id

===============================================================================

After all that, we can now create an instance of Num

> instance Num Nat where
>   (+) = addNat
>   (*) = mulNat
>   (-) = subNat
>   signum = sigNat
>   abs = absNat
>   negate x = Z -- we don't _technically_ need this, but its pretty obvious
>   fromInteger = integerToNat

Phew, that was fun. Next time- we'll play with Exp, Div and Mod, and maybe some
more fun stuff.

Quick note, pushing Peano into Num gives us (^) for free (sortof.), but we'll
define it next time anyway