Structural recursion over free algebras is crucial for foundations because, from the outside, the mathematical world is just a string of symbols: to handle it at the most basic level we need concatenation and parsing operations. On the other hand, van Kampen's Theorem 5.4.8 illustrates that lists pervade mathematics way beyond foundational considerations. Finite sets arise even more frequently, but to count a set means to form an exhaustive, nonrepeating list of its elements (Section 6.6).
Induction for numbers and lists Richard Dedekind (1888) studied the natural numbers as well as the reals, and gave the following axiomatisation, but it is usually attributed to Giuseppe Peano (1889).
The last is the induction scheme, which we have already mentioned as an example of well founded induction in Example 2.5.5(b).
The set of lists of elements of a set X may be defined in a similar way. The set X is sometimes called an alphabet, and lists are words. Other names for lists are strings, paths and texts.
Stephen Kleene used the notations X^{*} = List(X) and X^{+} = X^{*}\{[ ]} in the theory of regular grammars, cf \leadsto ^{*} for the transitive reduction relation (Definition 1.2.3), but we shall not use them. It is usual to write

DEFINITION 2.7.3 The last axiom says that the relation t\prec cons(h,t) is well founded and gives rise to list induction:

Concatenation Many of the uses of lists can be seen as simply ``adding them up,'' where the notion of addition is some associative operation with a unit, ie it defines a monoid. Concatenation of lists is the generic such operation. In the following examples, notice that functions of two lists may often be defined by recursion on only one of them.

omitted diagram environment
For practical purposes, these recursive definitions are rather inefficient; Exercise 6.28 gives extensionally equivalent versions of fold and append which are tail recursive, ie they are essentially while programs. But we need to know much more about lists and monoids to understand how to transform programs in this way.


PROOF: To use list induction in each case we have to identify the variable l and the predicate q[l] (namely the displayed equation), then prove the base case q[*] and the induction step "h."t.q[t]Þ q[cons(h,t)]. We are given one unit law, *;l = l, and so the base case, *;* = *, for the other.

Write [[l]] = fold(e,m,f,l), so
The operation fold has countless programming applications. We freely mix (functional) programs and mathematical notation.
EXAMPLES 2.7.6 Let l Î List(X) and y Î X.

Useful though they are, fold and append are not in fact the fundamental operations of recursion over lists.
Primitive recursion for the natural numbers
REMARK 2.7.7 Zero and successor are the introduction rules for N:


omitted eqnarray* environment
EXAMPLE 2.7.8 Addition and multiplication are defined by

Predecessor and pattern matching Successor and cons would be bijective functions, but for the omission of one element (zero or the empty list) from their images. It is tempting to overlook this and define ``inverses,'' pred(n+1) = n, tail(cons(h,t)) = t and head(cons(h,t)) = h.
REMARK 2.7.9 The new operations are only partially defined, but we may extend them as we like to total functions, since the support is complemented. For example pred(0) may be taken to be zero, ``error'' or ``exception.'' (The last is a nonjudgemental word for error, such as the exit from a loop.)
Although the operations can be forced to be total in this fashion, the rules, such as succ(pred(x)) = x, are only conditionally valid. A similar situation arises with division by zero, and we shall discuss how algebraic methods may be extended to handle it in Examples 4.6.4 and 5.5.9.
A more flexible approach is to say that each case offers a pattern r([(x)\vec]) against which the terms may be matched. Then we may define functions as we like by case analysis, so long as the patterns are mutually exclusive (nonoverlapping). The function so defined is total iff the patterns are also exhaustive.
In particular, definitions of ``well formed'' formulae (wffs) in complex type theories (Section 6.2) may be given by sideconditions involving the outermost operationsymbol(s). Sometimes we have to parse more than once, the general procedure being unification (Section 6.5).
Typetheoretic rules for lists We shall now give the Gentzenstyle presentation for lists, but if you are not yet familiar with the rules for the sum type you should skip the remainder of this section.
REMARK 2.7.10 Empty list and cons are introduction rules for List(X):


omitted eqnarray* environment
The operator listrec must also be invariant under substitution. By using a function \ops_{Q} instead of a term with free variables of types X and Q we have avoided introducing yet another variable binder together with its aequivalence ( cf Remark 2.3.11).
Let us compare cons and listrec with append and fold.
COROLLARY 2.7.11 List(X)  in particular N º List(1)  is the free algebra for two different theories:
No analogue of Proposition 2.7.5 is needed in the unary case. In fact

REMARK 2.7.12 The terms \opz_{Q} :Q and \ops_{Q} :XxQ® Q in the premises of (E List) are called the seed and action of X on Q. The continuation rule says that if z:Q® Q¢ is a homomorphism for this structure,
omitted diagram environment
then it is a recursion invariant ( cf Theorem 6.4.17 for while).

Although we have written Proof after these assertions, it will take us until Section 6.3 to show that List(X), the type of lists with elements from a given set X, actually exists in Zermelo type theory and has the required properties. On the other hand, in functional programming it is more appropriate to treat List as a new type constructor like +, x and ® , together with the rules in Remark 2.7.10.
List recursion is a typetheoretic phenomenon for which we haven't yet given the propositional analogue. This is induction for the reflexivetransitive closure of any binary relation, and is discussed in Sections 3.8 and 6.4. This will be based on another general induction idiom (on closure conditions), given in Definition 3.7.8. Similar methods are used for finite subsets in Section 6.6, which we shall also discuss using lists. In Chapter VI we shall introduce a new approach to induction based on a categorical analysis of free algebras. Theorem 6.2.8(a) constructs the free category on an oriented graph using the list idea.