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_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
> {-# OPTIONS -fglasgow-exts #-}
> module Peano (Nat(..), one, p,
>  &nbsp iton, ntoi, natToInteger,
>  &nbsp 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
> &nbsp 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

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.

> &nbsp Z == Z = True

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

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

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

> &nbsp 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
> &nbsp compare Z Z = EQ
> &nbsp compare (S x) Z = GT
> &nbsp compare Z (S x) = LT
> &nbsp 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.
>  &nbsp -- We'll come back to this when we start playing with ZZ
>  &nbsp -- (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

> addNat x Z = x
> addNat Z y = y
> addNat (S x) (S y)
> &nbsp | (S x) | 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
> &nbsp | a | otherwise = mulNat' b a a
> &nbsp where
>  &nbsp 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
> &nbsp | x | 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

> 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
> &nbsp (+) = addNat
> &nbsp (*) = mulNat
> &nbsp (-) = subNat
> &nbsp signum = sigNat
> &nbsp abs = absNat
> &nbsp negate x = Z -- we don't _technically_ need this, but its pretty obvious
> &nbsp 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

Published in: on July 12, 2007 at 3:05 am  Comments (4)  

The URI to TrackBack this entry is:

RSS feed for comments on this post.

4 CommentsLeave a comment

  1. Your induction axiom looks slightly wrong.

  2. it probably is, I was doing it from memory. I’ll dig up a better definition. I was writing the post while offline, so I didn’t have access to my online notes.

  3. Among other things, you have used 0 as your base case in the first few axioms, then switched to 1 for the induction axiom. (You quoted Wikpedia, and I think its definition uses the number theorists’ convention of excluding 0 from the naturals, as I understand Peano did. But CS/logic types in this day and age tend to include 0.)

  4. Oh crap, your absolutely correct, fritz, thanks for catching that. I did quote directly from wikipedia. I’ve never been able to remember the Induction axiom correctly off the top of my head. It’s one of those “I know what it is, just not how to say it.” Things. Should be fixed now.

    Thanks again

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: