Definitions, Definitions

So, unlike the previous chapter, this chapter will actually involve some coding in Agda. We start with a module name.

module peano where

Most language tutorials start with the typical “Hello, World” example, but this is not really appropriate for a first example in Agda. Unlike other languages, which rely on a whole lot of primitive operations and special cases for basic constructs, Agda is very minimal - most of the “language constructs” are actually defined in libraries.

Agda doesn’t even have numbers built in, so the first thing we’re going to do is define them - specifically natural numbers. Natural numbers are positive integers, that is, the whole numbers starting with zero and going up. Mathematics uses the symbol ℕ to represent natural numbers, so we’re going to borrow that for our example (Another thing that sets Agda apart from other languages is its extensive use of unicode to make mathematical constructs more natural). To enter ℕ into emacs, type \bn. To enter the unicode arrow (→), type \->. I’m going to demonstrate this line by line, so bear with me.

open import Agda.Primitive

module Hidden0 where

  data ℕ : Set where

To begin, we type data ℕ. The data keyword means we’re defining a type - in this case, ℕ. For this example, we’re specifying that this type, ℕ, is of type Set (that’s what the colon means).

Hold on a second, types have types?

If you recall the introduction, I mentioned that in Agda, types and values are treated the same way. This means that, seeing as values are given types, types are given types as well. Types are merely a special group of language terms, and in Agda, all terms have types.

Even Set (the type of our type ℕ) has a type: Set₁, which has a type Set₂, going on all the way up to infinity. We’ll touch more on what these Set types mean later, but for now you can think of Set as the type we give to all the data types we use in our program.

Structural Induction

Okay, so, we’ve defined our type, but now we need to fill the type with values. While a type with no values does have its uses, a natural numbers type with no values is categorically wrong. So, the first natural number we’ll define is zero:

module Hidden01 where

  data ℕ : Set where
    zero : ℕ

Here we are simply declaring the term zero to be a member of our new type ℕ. We could continue to define more numbers this way:

    one   : ℕ
    two   : ℕ
    three : ℕ 
    four  : ℕ

But we’d quickly find our text editor full of definitions and we’d be no closer to defining all the natural numbers than when we started. So, we should instead refer to a strict mathematical definition. The notation I’m using here should be familiar to anyone who knows set theory and/or first-order logic - don’t panic if you don’t know these things, we’ll be developing models for similar things in Agda later, so you will be able to pick it up as we go along.

• Zero is a natural number ().
• For any natural number , is also a natural number. For convenience, We shall refer to as ¹. ().

This is called an inductive definition of natural numbers. We call it inductive because it consists of a base rule, where we define a fixed starting point, and an inductive rule that, when applied to an element of the set, induces the next element of the set. This is a very elegant way to define infinitely large sets. This way of defining natural numbers was developed by a mathematician named Giuseppe Peano, and so they’re called the Peano numbers.

We will look at inductive proof in the coming chapters, which shares a similar structure.

For the base case, we’ve already defined zero to be in by saying:

module Hidden where

  data ℕ : Set where 
    zero : ℕ

For the second point (the inductive rule), it gets a little more complicated. First let’s take a look at the inductive rule definition in first order logic:

This means, given a natural number n, the constructor suc will return another natural number. So, in other words, suc could be considered a function that, when given a natural number, produces the next natural number. This means that we can define the constructor suc like so:

data ℕ : Set where 
  zero : ℕ
  suc  : ℕ → ℕ

Now we can express the number one as suc zero, and the number two as suc (suc zero), and the number three as suc (suc (suc zero)), and so on.

data Nat = Zero | Suc Nat

data Nat :: * where
  Zero :: Nat
  Suc  :: Nat -> Nat

One, Two.. Five!

Now we’re going to define some arithmetic operations on our natural numbers. Let’s try addition, first.

_+_ : ℕ → ℕ → ℕ 

Here I’m declaring a function. To start with, I give it a type² - it takes two natural numbers, and returns a natural number.

if_then_else_ : ∀ { a } → Bool → a → a → a

Now, let’s implement this function by structural recursion⁴.

_+_ : ℕ → ℕ → ℕ 
zero + zero = zero
zero + n    = n
(suc n) + n′ = suc (n + n′)  -- use \' to input ′.

Our First Check

Normally we’d run the program at this point to verify that it works, but in Agda one does that pretty rarely. Instead, what we do is get Agda to check our code. This checks that all our proof obligations have been met:

• It checks your types. Types are how you encode proof obligations in Agda (although we haven’t done any non-trivial proofs yet), so this is important.
• It checks that your program provably terminates. Checking that any program terminates is in general undecidable (see The Halting Problem), but proof obligations can only be machine-checked by Agda if your program terminates. To circumvent this dilemma, Agda runs its checker only on structural recursion with finite data structures, and warns that it can’t check proof obligations if non-structural recursion is ever used. We will discuss this more in later chapters, but the only examples presented in the early part of this book will be ones that Agda can already prove terminates.

To run a check, type C-c C-l into emacs, or choose Load from the Agda menu. If your program checks correctly, there will be no error messages, no hole markers (yellow highlighting) and no orange-highlighted non-terminating sections. It should also say Agda: Checked at the bottom of the window, and you get syntax highlighting.

Right now, our checks aren’t all that meaningful - the only thing they prove is that our addition function does indeed take any two natural numbers and produce a natural number, as the type suggests. Later on, when we encode more information in our types, our checks can mean a lot more - even more than running and testing the program.

“I Have Merely Proven It Correct”

To evaluate an expression (just to verify that it truly does work), we can type C-c C-n into emacs, or select “Evaluate term to normal form” from the Agda menu. Then, in the minibuffer, we can type an expression for 3 + 2:

(suc (suc (suc zero))) + (suc (suc zero))

And we get the result (5):

(suc (suc (suc (suc (suc zero)))))

In this chapter we have examined the Peano natural numbers, and defined some basic functions and data types in Agda. In the next chapter, we’ll look at propositional logic, and how to encode logical proofs in Agda using this system.