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 either with the recursor:
or by giving the defining equations:
To go from the former expression of to the latter, we simply use the computation rules for the recursor.Conversely, given any defining equations
where and are expressions that may involve the variables and 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 :
(1) | ||||
(2) |
involve the function 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 “” on the right-hand side of (2) as standing in for the result of the recursive call, which in a definition of the form would be the second argument of .
More generally, if we have a “definition” of a function such as
where is an expression of type , and is an expression of type which may involve the variable and also the symbol “”, we may translate it to a definition
where is obtained from by replacing all occurrences of “” by the new variable .
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 being defined can only appear in the body of as part of the composite symbol “”.Otherwise, we could write nonsense functions such as
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.