1.10 Pattern matching and recursion

The natural numbersMathworldPlanetmath 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→C either with the recursor:


or by giving the defining equations:

f⁒(𝗂𝗇𝗅⁒(a)) :≑g0(a)
f⁒(𝗂𝗇𝗋⁒(b)) :≑g1(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⁒(𝗂𝗇𝗅⁒(a)) :≑Φ0
f⁒(𝗂𝗇𝗋⁒(b)) :≑Φ1

where Ξ¦0 and Ξ¦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 Ξ»-abstraction:


In the case of the natural numbers, however, the β€œdefining equations” of a function such as π–½π—ˆπ—Žπ–»π—…π–Ύ:

π–½π—ˆπ—Žπ–»π—…π–Ύβ’(0) :≑0 (1)
π–½π—ˆπ—Žπ–»π—…π–Ύβ’(π—Œπ—Žπ–Όπ–Όβ’(n)) :β‰‘π—Œπ—Žπ–Όπ–Ό(π—Œπ—Žπ–Όπ–Ό(π–½π—ˆπ—Žπ–»π—…π–Ύ(n))) (2)

involve the function 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 π–½π—ˆπ—Žπ–»π—…π–Ύ, since they are much more convenient and readable. The solution is to read the expression β€œπ–½π—ˆπ—Žπ–»π—…π–Ύβ’(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 π–½π—ˆπ—Žπ–»π—…π–Ύ:≑𝗋𝖾𝖼ℕ(β„•,c0,cs) would be the second argument of cs.

More generally, if we have a β€œdefinition” of a function f:β„•β†’C such as

f⁒(0) :≑Φ0
f⁒(π—Œπ—Žπ–Όπ–Όβ’(n)) :≑Φs

where Ξ¦0 is an expression of type C, and Ξ¦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


where Ξ¦sβ€² is obtained from Ξ¦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 inductionMathworldPlanetmath) 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 functionMathworldPlanetmath 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⁒(π—Œπ—Žπ–Όπ–Όβ’(n)) as part of the composite symbol β€œf⁒(n)”. Otherwise, we could write nonsense functions such as

f⁒(0) :≑0
f⁒(π—Œπ—Žπ–Όπ–Όβ’(n)) :≑f(π—Œπ—Žπ–Όπ–Ό(π—Œπ—Žπ–Όπ–Ό(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