Addition in Agda

In the previous entry, we saw how relatively straightforward it was to build the natural numbers in Agda, following the tutorial PLFA. The next operation we want to define is addition. However, in my opinion, the presentation of addition in PLFA is not as neat.

For example, to be able to define addition, we are told to import some modules from the Agda standard library, which will allow access to some new symbols (or names), such as \(\equiv\) and \(\mathtt{refl}\). We are then given a very (very!) brief explanation as to what these symbols mean. The result, at least in my case, was that I could follow the lesson and make the code work… But I didn’t quite get why it worked, nor what it all meant. And the whole point of using Agda was to make the underlying theory (i.e., type theory) clearer, not more confusing. To remedy this, I had to translate Agda notation back into mathematical notation, and only then did things become clear.

So, to start, in Agda, we declare addition as follows:

_+_ : ℕ → ℕ → ℕ
zero + n = n
(suc m) + n = suc (m + n)

The first thing to note is that this is a definition. The equals symbol here has the same role as the math definition symbol \(\coloneqq\) (or, in some books \(:\equiv\)). As a definition, the only thing we require of it is that it is well-founded. We begin the definition with the signature, which tells us that \(\_ + \_\) is a new function-term of type \(\mathbb{N} \to (\mathbb{N} \to \mathbb{N})\). In other words, it’s a curried function.

The function, taking a term m of \(\mathbb{N}\), becomes another function-term \(m + \_\) of type \(\mathbb{N} \to \mathbb{N}\). Taking another term \(n: \mathbb{N}\), it becomes the atomic term \(m + n: \mathbb{N}\), i.e., a natural number.¹ (Alternatively, \(\_ + \_\) is a “binary” function that takes two terms of \(\mathbb{N}\) and returns a natural number.)

The terms m and n of type \(\mathbb{N}\) can be, as we just saw, either zero or the successor of some number. In the second and third lines of the definition we consider just the case where the first argument \(m\) is either zero or some successor. This is all we need: the method is called “induction on the first variable.”

When the first argument of \(\_ + \_\) is the constant zero, and the second is the fixed \(n\), i.e., \(\mathtt{zero} + n\), then we make this term definitionally equivalent to \(n\). Similarly, when the first argument is \((\mathtt{suc}\ m)\), i.e., a successor (any number except zero), then we make the term \((\mathtt{suc}\ m) + n\) definitionally equivalent to the term \(\mathtt{suc}\ (m + n)\), that is, the constructor \(\mathtt{suc}\) applied to the term \(m + n\). (Note the recursive nature of the definition.)

Example

With the definition out of the way, we can prove that 3 + 4 is 7 as follows:

_ : 3 + 4 ≡ 7
_ = 
  begin
  3 + 4
  ≡⟨⟩
  (suc (suc (suc zero))) + (suc (suc (suc (suc zero))))
  ≡⟨⟩
  suc (suc (suc (suc (suc (suc (suc zero))))))
  ≡⟨⟩
  7
  ∎

The code works, but why? What is going on here?

In the first line we have the presence of a colon (:), meaning that we are introducing a term of some type. We also find the first use of the symbol \(\equiv\). In the tutorial, we are told \(\equiv\) is an operator and used for assertions. What is left out (and this stumped me for a while) is that the word “assertion” is used to mean a proposition, and a proposition in type theory is a type! Specifically, it’s an identity type. So the first line is saying that “something” is a term of the identity type \(3 + 4 \equiv 7\), which, read as a proposition says “3 plus 4 is equal to 7”. The “something” here is the term denoted with an underscore \((\_)\) (a “dummy” name).

Another way to read this is by interpreting the term \((\_)\) as a proof of the proposition “3 plus 4 is equal to 7”.

Next problem: On the right-hand side we have what is called equational reasoning. This involves a chain of equations that starts with the keyword \(\mathtt{begin}\), ends with the QED symbol \(\blacksquare\), and each reasoning step is separated by the symbols \(\equiv\langle\rangle\). In the example, we translate the components of the term \(3 + 4\) into applications of \(\mathtt{zero}\) and \(\mathtt{suc}\), then apply our definition of \(\_ + \_\), so that we get the term \(\mathtt{suc (suc (suc (suc (suc (suc (suc zero))))))}\), which is the long form of the number \(7\). Therefore, the conclusion seems to be that our dummy term \((\_)\) is judgmentally the same as \(7\), right?

Wrong! If instead of that chain of equations you write

_ : 3 + 4 ≡ 7
_ = 7

Agda will complain and give you an error!

In math, you also have equational reasoning, e.g.:

\[\begin{align*} 2(3 + 2) &= 2\cdot 3 + 2 \cdot 2\\ &= 6 + 4\\ &= 10 \end{align*}\]

So you can correctly conclude that \(2(3 + 2) = 10\). But this is not what is happening in Agda.

It took me a few days to figure this out, and I think I finally understood what I got wrong. But since this entry is getting a bit long, I’ll publish that separately.