Note A1: Peano Arithmetic

Today, we're going to jump into the deep end of the pool, Haskell wise. Don't be put off if you don't understand everything. Today's lecture is mostly literature, i.e., your task as a student is to read and expand your mind. I'll expect a bit of mimcry at first, real comprehension will come in time.

Our subject for today is the Peano-Dedekind axioms for arithmetic. Yes, we're going to redo third-grade math, but as it might be done by a graduate student studying mathematical logic. The underlying structure is the natural numbers, 0, 1, 2, ….

The Peano-Dedekind axioms posit the existence of a constant $0$ and function $s$ (the successor function) with the following properties:

We'll start with a data definition:

data NaturalNumber = Zero | S NaturalNumber deriving (Show)

This introduces a new type. Haskell's type system is a central part of the language, and our ability to introduce new types that exploit built-in facilities of the language is both useful and powerful. The type system partitions the universe of values and expressions into equivalence classes, and limits how the elements of these equivalence classes can be combined. Types are denoted by type definitions (as above) and type expressions (of which more later).

The definition above expresses the intent that natural numbers come in two distinct forms (it is helpful here to read | as ”or”): Zero, and S x where x is also a NaturalNumber. Thus, Zero, S Zero, S (S Zero) are values (and expressions) of type NaturalNumber, which we ordinarily know by the names zero, one, and two respectively. Note here that S is not just a function, it is a constructor, which can be thought of as a kind of labeled box that holds another value of type NaturalNumber. Haskell uses a simple, mandatory notational convention here: variables have names that begin with lower-case letters (including _), while constructors begin with an upper-case letter. The deriving (Show) instructs Haskell to print natural number values via constructor-based expressions.

Let's define a few names for common natural numbers:

-- common names for small natural numbers zero = Zero one = S zero two = S one three = S two four = S three five = S four six = S five seven = S six eight = S seven nine = S eight ten = S nine

There are several things to notice here. The first is a simple comment, which is introduced by a double hyphen, --. This, and any text that follows on the same line, is ignored by Haskell. This text is there to support our understanding. The next is the sequence of definitions, in which variables are bound to values denoted by expressions. Note that in Haskell, like many programming languages, we use = to indicate binding. This essentially creates equality by fiat, but it is distinct from the equality predicate, which we'll see next.

$ ghci NaturalNumbers.hs > three S (S (S Zero))

Equality and Ordering

First, we'll write code that makes the NaturalNumber type an instance of the Eq typeclass.

instance Eq NaturalNumber where Zero == Zero = True Zero == S y = False S x == Zero = False S x == S y = x == y

We can make a tiny code improvement here: note that the x and y on the left-hand side of the bindings in the 2nd and 3rd line of the definition are not used on the right hand side. This means that we don't actually need to name a variable:

instance Eq NaturalNumber where Zero == Zero = True Zero == S _ = False S _ == Zero = False S x == S y = x == y

In Haskell, types are organized into typeclasses. This is a very different meaning of “class” than you might have encountered in a language like Java. It's actually closer to Java's notion of an interface, but more powerful. The significance of a typeclass is that all types that belong to a given typeclass define certain common names. In the case of the Eq typeclass, instances must implement one or both of == (the equality predicate) or /= (the inequality predicate), and having done so, will have both defined for them. In this case, we're defining the equality predicate ==, based on the Peano-Dedekind axioms: Zero == Zero is a special case of reflexivity, Zero does not equal any successor, and two successors are equal if and only if their predecessors are equal (this follows from $s$ being one-to-one).

There's no essential difference between defining an ordinary function (one that is applied in prefix to zero or more argument/s), and defining an infix binary function like ==: we bind patterns to expressions to expressions in both cases. Indeed, from Haskell's point of view, infix binary functions are just syntactic sugar for ordinary (curried) binary functions. Having said that, the definition of equality is interesting, because it's recursive, i.e, we are defining == in terms of itself when we write S x == S y = x == y. Being able to define a function by recursion is powerful, but it's not free. Such a definition is going to drive a sequence of substitutions (as we saw in Lecture 1), a sequence that might or might not terminate. In this case, == will terminate on grounded elements of the natural numbers, because we defined it without recursion on base cases (Zero), and the recursive definition in constructed cases involved recursive calls of the function being defined on proper substructures of the argument. We will call recursions like this natural, or structural recursions, and the proof of termination follows from ordinary mathematical induction.

> ten == ten True > ten == nine False > ten /= nine True

Let's understand how this works on a small example:

two == one ==> S one == S zero ==> one == zero ==> S zero == Zero ==> False

How many of you noticed the weasel-word “grounded” up above?! This is actually important, and it gets to one of the ways that Haskell is not like other languages that you might have experienced. Let's talk about this particular case. Zero is grounded. This is a specific case of a general principle: all of the nullary constructors (i.e., constants) of an algebraic type are grounded. Also, if n is grounded, then S n is also grounded. Again, this is a specific case of a general principle: applying a k-ary constructor to k grounded values, results in grounded value. At this point, you're probably asking yourself, “Are there any ungrounded values?!” Yes. Consider

infinity = S infinity

What is infinity? Note infinity is defined recursively, but not naturally, because the right-hand side of the recursion mentions the left-hand side (rather than a proper substructure thereof). Therefore this is a potentially dangerous definition. Note that there's nothing special about Haskell in allowing you to make such a definition -- you can do something analogous in any general purpose programming language. The difference is that in Haskell, such definitions can be useful, which is to say, they can be used in terminating computations. Of course, you wouldn't want to simply evaluate infinity:

> infinity (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S ... ^-C Interrupted. >

But this works:

> infinity == one False >

Why?! Let's trace it...

infinity == one ==> S infinity == S zero ==> infinity == zero ==> S infinity == Zero ==> False

You're all invited to try this in Java. Get back to me when it finishes :-).

Whether the inclusion of objects like infinity in our NaturalNumber type seems like a good idea or not, it is an inevitability, and this is one of the ways that computational systems can fail to exactly correspond to mathematical systems. Objects like infinity are explicitly excluded from Peano-Dedekind Arithmetic by the induction axiom, which essentially says that all (Peano-Dedekind) natural numbers are grounded.

Adding infinity has other costs, e.g., computed equality is no longer reflexive, and this can be a trap in naïve reasoning about code.

infinity == infinity ==> S infinity == S infinity ==> infinity == infinity ...

This leads to a high-speed twiddling of the CPUs thumbs, but rather than termination with the result True. A general rule of thumb is that natural recursions are safe, i.e., they terminate, because all recursive calls are made to simpler arguments, and therefore a termination proof can be obtained by induction over the definition of the set of grounded values. The problem is that the grounded values of the domain aren't exhaustive.

*Exercise A1.1 Haskell contains an Ord typeclass, consisting of types with a natural trichotomous ordering. Provide an instance declaration that adds NaturalNumber to the Ord typeclass.

The documentation for the Ord typeclass can be found here, as well as on your system (assuming you've properly installed the Haskell Platform). The most satisfactory way to do this is by implementing the compare function, which takes two arguments, and returns LT, EQ, or GT, according as to whether the first argument is less than, equal to, or great than, the second argument, respectively.

To do this, complete the following definition

instance Ord NaturalNumber where compare Zero Zero = EQ ...

Once you've done this, you should be able to do simple comparisons, e.g.,

> ten >= nine True

Nonterminating computations are inevitable in any general-purpose programming language. The problem is not just infinity, which is in some sense a natural “limit point” in the natural numbers, but also definitions that twiddle their thumbs without creating new constructors, e.g.,

loop :: NaturalNumber loop = loop

Here, we provide a type ascription to loop because there's not enough information otherwise for the compiler to figure it out. This may seem like a silly example, but it's easy to achieve the same effect accidentally, and often difficult to sort out when you do. Oddly enough, loop can be used to define new natural numbers, and we can even compute with them:

> S loop == Zero False

but

> loop == loop ...

never terminates. It might seem to be a defect of Haskell that we can't weed out "unintentional" values of type NaturalNumber like the values of loop and infinity, but if so, it's a defect that all current and future programming languages must share, a consequence of the undecidability of the halting problem, one of the most fundamental theorems of computability theory, in essence a restatement of the Gödel's celebrated incompleteness theorem for Peano Arithmetic, which oddly enough is the subject of this lecture.

Addition and Multiplication

The principal operations of Peano-Dedekind arithmetic are addition and multiplication, which are recursively defined. This is most naturally accomplished by adding NaturalNumber to Haskell's Num typeclass. Doing this correctly requires implementing a number of functions, +, *, - (or negate), abs, signnum, and fromInteger. We'll get the definitions of + and * directly from the Peano-Dedekind axioms.

instance Num NaturalNumber where x + Zero = x x + S y = S (x + y) x * Zero = Zero x * S y = x + x * y

Haskell will permit us to provide partial implementations of typeclasses, although not without complaint. Even so, this is a useful way to proceed, because it allows us to test our code incrementally.

> two * three + one S (S (S (S (S (S (S Zero))))))

We'll next add an implementation of fromInteger, along with a simple helper function nat:

instance Num NaturalNumber where ... fromInteger n | n > 0 = S (fromInteger (n-1)) | n == 0 = Zero nat :: NaturalNumber -> NaturalNumber nat = id

The definition of fromInteger involves a programming new construct, guarded equations. The idea here is that we'll define a function by cases through a sequence of predicates (tests) and equations. The reduction of a term will evaluate each of the predicates in turn, until a predicate evaluates to True. Once this happens, the corresponding equation is used. The point to this definition is that it consciously avoids defining fromInteger on negative inputs, as this is meaningless in the context of the natural numbers.

The nat function is just the identity, but with a restricted type. We can use nat to force the interpretation of a literal like 1234 as a NaturalNumber via the fromInteger function.

The significance of these definitions is that they enable us to take advantage of Haskell's input processing. Consider a simple expression like:

2

What is the type of 2? The answer is that it can belong to any type that belongs to the Num typeclass, although it defaults to Integer (an “infinite-precision” integral type). By adding fromInteger, we make expressions like this meaningful:

two + 27

In effect, the two, which can only be a NaturalNumber, forces both + and 27 to be interpreted as a binary operator on NaturalNumber and a NaturalNumber respectively. The function nat does the same thing. Here we see both a type declaration (of which much more later), and a definition. Using nat enables us to force the interpretation of a numeric literal to be a NaturalNumber. Thus, we can write

> nat (2 * 3 + 4) ...

As we'll see later, this forces the expression 2 * 3 + 4 to have the type NaturalNumber, and this in turn will ultimately force 2, 3, and 4 to have type NaturalNumber too. ... S (S (S (S (S (S (S (S (S (S Zero)))))))))

We can write this with one fewer character via

> nat $ 2 * 3 + 4 S (S (S (S (S (S (S (S (S (S Zero)))))))))

Here, $ is a low precedence right associative infix operator for function application. It is a friend, a good friend, which can save us from the “lots of irritating single parentheses” that is sometimes used in a pejorative etymology of “Lisp.”

Exercise A1.2 Complete the definition of instance Num NaturalNumber by implementing -, abs and signnum in as meaningful a manner as possible. Note that for natural numbers, subtraction is truncated at Zero, i.e., evaluating one - ten should return Zero.

Exercise A1.3 It's easy to use pattern matching to write simple number theoretic functions using pattern matching like this:

even Zero = True even (S Zero) = False even (S (S n)) = even n

but it's much more convenient to take advantage of the machinery we've built up, and write it like this:

even n | n == 0 = True | n == 1 = False | otherwise = even (n-2)

and indeed, I tend to think of the first form as a translation of the second into the particular representation we used for NaturalNumber, whereas the later is "more generic," and because it doesn't make assumptions about representations, works perfectly well for other representations.

Write such representation-independent implementations of odd and remainder. Note that because even and odd are defined in the Haskell Prelude, it's necessary to begin the Haskell source file that includes your definitions with an import statement that explicitly hides them:

import Prelude hiding (even,odd)

Laziness

Thus far, we've been modeling Haskell's evaluation mechanism via term rewriting. This is not exactly correct, but it will do for now.

Now, my friend Robby, an exquisite Scheme programmer, would instinctively re-write the definition of + as follows:

x + Zero = x x + S y = S x + y

Remember here that application binds more tightly than infix operations, so this change is from the original S (x + y) to (S x) + y in Robby's code.

If you ask Robby why, he'd talk about “tail recursion,” and about why the second form is tail recursive (and so runs in constant stack space), whereas the first form is not (and so involves putting a bunch of pending “apply S to the result, and return” frames on the stack). And he'd be perfectly right. In Scheme. But Haskell is not Scheme, and Robby's definition involves a “loss of laziness” if carried over unreflectively from Scheme to Haskell. Let's see how that works.

Suppose we want to evaluate ten + ten == one. If we use the original definition, we'd have

ten + ten == one ==> ten + S nine == S zero ==> S (ten + nine) == S zero ==> ten + nine == zero ==> ten + S eight == Zero ==> S (ten + eight) == Zero ==> False

In effect, we only needed to apply the successor case of the addition rule twice to prove that ten + ten /= one. Whereas, with Robby's implementation, we'd have to do something like this:

ten + ten == one ==> ten + S nine == S zero ==> S ten + nine == S zero ==> S ten + S eight == S zero ==> S (S ten) + eight == S zero ==> S (S ten) + S seven == S zero ==> S (S (S ten)) + seven == S zero ... -- 13 steps elided ==> S (S (S (S (S (S (S (S (S (S ten))))))))) + Zero == S zero ==> S (S (S (S (S (S (S (S (S (S ten))))))))) == S zero ==> S (S (S (S (S (S (S (S (S ten)))))))) == zero ==> S (S (S (S (S (S (S (S (S ten)))))))) == Zero ==> False

Note that we got the same answer both times, but that Robby's implementation required that we completely reduce the addition, whereas the original implementation did not. This point can be driven even further. With the first definition, we can evaluate nine + infinity > ten, and promptly obtain the result True. With Robby's definition, this would run forever without returning a result.

*Exercise A1.4 The axiom for the successor case of multiplication in the Wikipedia article is not what I remembered from graduate school. The crux of the matter is whether you consider S x = x + 1, or S x = 1 + x, and the Wikipedia article assumes the second. If we assume the first, as I remember it, the natural definition for the successor case of multiplication is subtly different:

x * S y = x * y + x

The form that I remember is better Haskell, in the sense that it's lazier. Illustrate this by a simple example, as above.

A complete version of today's program (and a reasonable starting point for today's exercises) is here: NaturalNumber.hs.