Even and Odd

So far we’ve been defining binary relations as collections of doubly indexed types. For example, we have inequality declared as \(\_\!\leq\!\_ : \mathbb{N \to N} \to \mathtt{Set}\), a collection that consists of individual types of the form \(m \leq n\), indexed by two naturals \(m\) and \(n\). However, we can also define unary relations in a similar manner.

It sounds odd to talk about a unary relation when, in common parlance, a relation has to be between at least two things. But in mathematical logic, a unary relation is a perfectly acceptable concept, much like a nullary function, and empty set, or even the number zero. In logic, a unary relation is called a predicate, which expresses that some “thing” has some property. In this entry, we’ll define the predicates even and odd for the natural numbers.

A unary relation can also be defined as a type family (a collection of types). In Agda code, according to the PLFA:

data even : ℕ → Set
data odd  : ℕ → Set

data even where

  zero : even zero

  suc  : ∀ {n : ℕ} → odd n → even (suc n)

data odd where

  suc  : ∀ {n : ℕ} → even n → odd (suc n)

In the first two lines, we declare or give the signature of the two new type families \(\mathtt{even}\) and \(\mathtt{odd}\). Each is a collection of types of the form \(\mathtt{even}\ n\) or \(\mathtt{odd}\ n\), where each individual type is indexed by some number \(n: \mathbb{N}\). Interpreted as propositions, \(\mathtt{even}\ n\) says “\(n\) is even”, while \(\mathtt{odd}\ n\) says “\(n\) is odd”.

A small digression

Now, usually, after the signature we immediately declare the constructors, that is, the means by which we construct the terms of the individual indexed types that make up the collection. Here, the declaration of the type families is done separately from the declaration of the constructors. Why?

I’m not entirely sure what is happening here…

… but perhaps it’ll help to see what happens if we try to make the declarations in our usual way. Suppose we were to try the following bit of code to start with:

data even : ℕ → Set where

  zero : even zero

If we compile, this will result in no errors, meaning it checks out. Now let’s try to introduce the other constructor for \(\mathtt{even}\):

data even : ℕ → Set where

  zero : even zero
  suc  : ∀ {n : ℕ} → odd n → even (suc n)

Oops! If you compiled, you probably got the error “odd not in scope.” I assume this means the compiler doesn’t know what to do with “odd” because it hasn’t been declared. Ok, then we simply add the declaration for \(\mathtt{odd}\) before the one for \(\mathtt{even}\):

data odd : ℕ → Set 
data even : ℕ → Set where

  zero : even zero
  suc  : ∀ {n : ℕ} → odd n → even (suc n)

Compiling once again results in another error: “the type odd is declared but lacks a definition”! Oops again! Ok, let’s try to add the constructor for \(\mathtt{odd}\):

data odd : ℕ → Set where

  suc  : ∀ {n : ℕ} → even n → odd (suc n)

data even : ℕ → Set where

  zero : even zero
  suc  : ∀ {n : ℕ} → odd n → even (suc n)

Compiling yet again results in an error that is similar to the first one we encountered: “even not in scope.” Huh! But \(\mathtt{even}\) is declared… except it comes after the declaration for \(\mathtt{odd}\). So the problem seems to be that each type makes a reference to the other. This is, I think, what the PLFA means by a “mutually recursive datatype declaration.” And it’s because of this chicken-and-egg situation that we first have to declare the type families \(\mathtt{even}\) and \(\mathtt{odd}\), each on a line of their own, followed by the constructor declarations.

Another thing you’ll notice is that we’re re-using the names \(\mathtt{zero}\) and \(\mathtt{suc}\) that we used to construct the natural numbers. In that entry, we declared them as \(\mathtt{zero}: \mathbb{N}\) and \(\mathtt{suc}: \mathbb{N \to N}\). But in type theory, unlike in set theory, a term (and a constructor is a term) is only allowed to be of one type, and here we are assigning them new types! This is called overloading, and Agda does allow for overloading of constructors.

Getting back on track

Let’s look again at the declarations in their right order:

data even : ℕ → Set
data odd  : ℕ → Set

data even where

  zero : even zero

  suc  : ∀ {n : ℕ} → odd n → even (suc n)

data odd where

  suc  : ∀ {n : ℕ} → even n → odd (suc n)

So the first two lines tell us that \(\mathtt{even}\) and \(\mathtt{odd}\) are collections of types indexed by a natural number. One of those types is \(\mathtt{even\ zero}\), whose term is the constant \(\mathtt{zero}\).¹ Interpreted as a proposition, the type \(\mathtt{even\ zero}\) says that “zero is even”, which is true, and \(\mathtt{zero}\) is its proof. In other words, \(0\) is even by definition.

Next, we have the second constructor for \(\mathtt{even}\), the function \(\mathtt{suc}\), which, given a number \(n\) and a term of \(\mathtt{odd}\ n\) (or a proof that \(n\) is odd), gives us a term of the type \(\mathtt{even}\ (\mathtt{suc}\ n)\). Interpreted as a proposition, \(\mathtt{even}\ (\mathtt{suc}\ n)\) says “the successor of \(n\) is even” (provided \(n\) is an odd number).

Finally, we have the constructor for \(\mathtt{odd}\), the (very overloaded) function \(\mathtt{suc}\), which given a number \(n\) and a term of \(\mathtt{even}\ n\), gives us a term of the type \(\mathtt{odd}\ (\mathtt{suc}\ n)\). Interpreted as a proposition, \(\mathtt{odd}\ (\mathtt{suc}\ n)\) says “the successor of \(n\) is odd” (provided \(n\) is an even number).

In short, we have three cases for any number: 1) if it’s zero, then it’s even by definition, 2) if it’s the successor of an odd number, then it’s even, and 3) if it’s the successor of an even number, then it is odd.

Even and odd for sums

We now want to apply this reasoning to the sum of two numbers. In particular, we want to show that the sum of two even numbers is even. In type theory, if we have a term of \(\mathtt{even}\ m\) and of \(\mathtt{even}\ n\), then we should have a term of \(\mathtt{even}\ (m + n)\). In other words, if “\(m\) is even” and “\(n\) is even”, then “the number \(m + n\) is even”.

We’ll use the following Agda code:

e+e≡e : ∀ {m n : ℕ} → even m → even n → even (m + n)

o+e≡o : ∀ {m n : ℕ} → odd m → even n → odd (m + n)

e+e≡e zero     en  =  en

e+e≡e (suc om) en  =  suc (o+e≡o om en)

o+e≡o (suc em) en  =  suc (e+e≡e em en)

Note that since the predicates \(\mathtt{even}\) and \(\mathtt{odd}\) reference each other, then we must have two functions, one that we’ll call \(\text{e+e≡e}\)² which takes proof that two numbers \(m\) and \(n\) are even and provides a term/proof that \(\mathtt{even}\ (m + n)\), and another called \(\text{o+e≡o}\)³ which takes proof that \(m\) is odd and \(n\) is even and provides a term/proof of \(\mathtt{odd}\ (m + n)\), but whose successor must be even according to the three cases mentioned above.⁴

Let’s say that the first number \(m = \mathtt{zero} = 0\). In that case, by currying, we have:

\[\begin{align*} \text{e+e≡e} &: \mathtt{even}\ 0 \to \mathtt{even}\ n \to \mathtt{even}\ (0 + n)\\ \text{e+e≡e}\ 0 &: \mathtt{even}\ n \to \mathtt{even}\ (0 + n)\\ \text{e+e≡e}\ 0\ en &: \mathtt{even}\ (0 + n)\\ \text{e+e≡e}\ 0\ en &= en \end{align*}\]

Here \(en\) is the name we give to some term of \(\mathtt{even}\ n\), so that \(\text{e+e≡e}\ 0\ en\) is the term or proof of \(\mathtt{even}\ (0 + n)\). Now, we know from our entry on addition, that the term \((0 + n)\) is judgmentally the same as (or reduces to) \(n\), and so the type \(\mathtt{even}\ (0 + n)\) is equivalent to \(\mathtt{even}\ n\). Therefore, the term \(\text{e+e≡e}\ 0\ en\) is equivalent to just \(en\).

Now suppose that \(m\) is any number except \(0\). If it’s odd, then we need a function that takes proof of \(\mathtt{odd}\ m\). That function is \(\text{o+e≡o}\), which returns proof that the sum of an odd \(m\) and an even \(n\) is odd:

\[\begin{align*} \text{o+e≡o}\ &: \mathtt{odd}\ m \to \mathtt{even}\ n \to \mathtt{odd}\ (m + n)\\ \text{o+e≡o}\ om &: \mathtt{even}\ n \to \mathtt{odd}\ (m + n)\\ \text{o+e≡o}\ om\ en &: \mathtt{odd}\ (m + n) \end{align*}\]

But recall that the successor of an odd number is even. Therefore, if \(m\) is odd, and \(om\) is a term/proof of \(\mathtt{odd}\ m\), then its successor, \(\mathtt{suc}\ om\), must be even and of type \(\mathtt{even}\ (\mathtt{suc}\ m)\). Likewise, if \(\text{o+e≡o}\ om\ en\) is odd because it’s a term of \(\mathtt{odd}\ (m+n)\), then its successor, \(\mathtt{suc}\ (\text{o+e≡o}\ om\ en)\), must be even and its type must be \(\mathtt{even}\ (m + n)\). In other words, we have the following judgmental equality of terms:

\[ \text{e+e≡e}\ (\mathtt{suc}\ om)\ en = \mathtt{suc}\ (\text{o+e≡o}\ om\ en) \]