1.10 Pattern matching and recursion

The natural numbers introduce an additional subtlety over the types considered up until now. In the case of coproducts, for instance, we could define a function $f:A+B\to C$ either with the recursor:

$$f:\equiv {\mathrm{𝗋𝖾𝖼}}_{A+B}(C,g_0,g_1)$$

or by giving the defining equations:

$f(\mathrm{𝗂𝗇𝗅}(a))$ $:\equiv g_0(a)$

$f(\mathrm{𝗂𝗇𝗋}(b))$ $:\equiv g_1(b).$

To go from the former expression of $f$ to the latter, we simply use the computation rules for the recursor. Conversely, given any defining equations

$f(\mathrm{𝗂𝗇𝗅}(a))$ $:\equiv {\mathrm{\Phi }}_0$

$f(\mathrm{𝗂𝗇𝗋}(b))$ $:\equiv {\mathrm{\Phi }}_1$

where ${\mathrm{\Phi }}_0$ and ${\mathrm{\Phi }}_1$ are expressions that may involve the variables $a$ and $b$ respectively, we can express these equations equivalently in terms of the recursor by using $\lambda$-abstraction:

$$f:\equiv {\mathrm{𝗋𝖾𝖼}}_{A+B}(C,\lambda a.{\mathrm{\Phi }}_0,\lambda b.{\mathrm{\Phi }}_1).$$

In the case of the natural numbers, however, the “defining equations” of a function such as $\mathrm{𝖽𝗈𝗎𝖻𝗅𝖾}$:

$\mathrm{𝖽𝗈𝗎𝖻𝗅𝖾}(0)$ $:\equiv 0$ (1)

$\mathrm{𝖽𝗈𝗎𝖻𝗅𝖾}(\mathrm{𝗌𝗎𝖼𝖼}(n))$ $:\equiv \mathrm{𝗌𝗎𝖼𝖼}(\mathrm{𝗌𝗎𝖼𝖼}(\mathrm{𝖽𝗈𝗎𝖻𝗅𝖾}(n)))$ (2)

involve the function $\mathrm{double}$ itself on the right-hand side. However, we would still like to be able to give these equations, rather than (LABEL:eq:dbl-as-rec), as the definition of $\mathrm{𝖽𝗈𝗎𝖻𝗅𝖾}$, since they are much more convenient and readable. The solution is to read the expression “$\mathrm{𝖽𝗈𝗎𝖻𝗅𝖾}(n)$” on the right-hand side of (2) as standing in for the result of the recursive call, which in a definition of the form $\mathrm{𝖽𝗈𝗎𝖻𝗅𝖾}:\equiv {\mathrm{𝗋𝖾𝖼}}_{\mathbb{N}}(\mathbb{N},c_0,c_s)$ would be the second argument of $c_s$.

More generally, if we have a “definition” of a function $f:\mathbb{N}\to C$ such as

$f(0)$ $:\equiv {\mathrm{\Phi }}_0$

$f(\mathrm{𝗌𝗎𝖼𝖼}(n))$ $:\equiv {\mathrm{\Phi }}_s$

where ${\mathrm{\Phi }}_0$ is an expression of type $C$, and ${\mathrm{\Phi }}_s$ is an expression of type $C$ which may involve the variable $n$ and also the symbol “$f(n)$”, we may translate it to a definition

$$f:\equiv {\mathrm{𝗋𝖾𝖼}}_{\mathbb{N}}(C,{\mathrm{\Phi }}_0,\lambda n.\lambda r.{\mathrm{\Phi }}_s^{\prime })$$

where ${\mathrm{\Phi }}_s^{\prime }$ is obtained from ${\mathrm{\Phi }}_s$ by replacing all occurrences of “$f(n)$” by the new variable $r$.

This style of defining functions by recursion (or, more generally, dependent functions by induction) is so convenient that we frequently adopt it. It is called definition by pattern matching. Of course, it is very similar to how a computer programmer may define a recursive function with a body that literally contains recursive calls to itself. However, unlike the programmer, we are restricted in what sort of recursive calls we can make: in order for such a definition to be re-expressible using the recursion principle, the function $f$ being defined can only appear in the body of $f(\mathrm{𝗌𝗎𝖼𝖼}(n))$ as part of the composite symbol “$f(n)$”. Otherwise, we could write nonsense functions such as

$f(0)$ $:\equiv 0$

$f(\mathrm{𝗌𝗎𝖼𝖼}(n))$ $:\equiv f(\mathrm{𝗌𝗎𝖼𝖼}(\mathrm{𝗌𝗎𝖼𝖼}(n))).$

If a programmer wrote such a function, it would simply call itself forever on any positive input, going into an infinite loop and never returning a value. In mathematics, however, to be worthy of the name, a function must always associate a unique output value to every input value, so this would be unacceptable.

This point will be even more important when we introduce more complicated inductive types in http://planetmath.org/node/87578Chapter 5,http://planetmath.org/node/87579Chapter 6,http://planetmath.org/node/87585Chapter 11. Whenever we introduce a new kind of inductive definition, we always begin by deriving its induction principle. Only then do we introduce an appropriate sort of “pattern matching” which can be justified as a shorthand for the induction principle.

Title	1.10 Pattern matching and recursion