Practical Foundations of Mathematics

Paul Taylor

2.7 Lists and Structural Induction

Now we discuss the idioms for list recursion from functional programming, and then set out the type-theoretic rules for List(X) analogous to those for + in Section 2.3. We treat the natural numbers in parallel with lists because each sheds light on the other.

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, non-repeating 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).

DEFINITION 2.7.1

(a): 0:N;
(b): if n:N then succn:N;
(c): if n:N then 0 ¹ succn;
(d): if n,m:N and succn = succm then n = m;
(e): if U Ì N is a subalgebra, ie 0 Î U and "n:N.n Î UÞ succn Î U, then U = N.

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.

DEFINITION 2.7.2

(a): The empty list, written nil, * or [ ], is in List(X);
(b): if h:X and t:List(X) then cons(h,t): List(X), the list constructed from the head h and tail t; some authors write h::t for this;
(c): * ¹ cons(h,t);
(d): if cons(h,u) = cons(k,v) then h = k and u = v;
(e): if U Ì List(X) is a subalgebra, ie * Î U and "h:X."t:List (X). t Î UÞ cons(h,t) Î U, then U = List(X).

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

cons(x₁,cons(x₂,··· cons(x_n,*)···)) as [x₁,x₂,¼,x_n].

The head and tail operations are also known as car and cdr. These are fossils of John McCarthy's original implementation of LISP in 1956 on an IBM 704. This machine had a 36-bit register with two readily accessible 15-bit parts called address and decrement, of which car and cdr extracted the contents. Lists also feature in a dynamic or imperative context as stacks, where cons is push and (head,tail) together correspond to pop.

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:

omitted prooftree environment

For the one-letter alphabet X = {s}, this is just Peano induction on List({s}) º N, where cons is the successor.

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.

DEFINITION 2.7.4

(a)

The concatenation of two lists is defined by structural recursion on the first of them (this operation also called append ):

*;l = l cons(h,t);l = cons

æ
è

h,(t;l )

ö
ø

Section 4.2 explains why we use a semicolon for this as well as for relational composition (Definition 1.3.7).

(b)

Let M be a set with an element e and a binary operation m, and f:X® M any function. Define a function List(X)® M by omitted eqnarray* environment so f(x) = fold(e,m,f,[x]).

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.

PROPOSITION 2.7.5

(a)

Lists form a monoid with * as unit and (;) as composition:

l;* = l = *;l (l;l₁);l₂ = l;(l₁;l₂).

(b)

If (M,e,m) is a monoid then l® fold(e,m ,f,l) is a homomorphism for the binary operations:

fold

æ
è

e,m,f,(l;l₁)

ö
ø

= m

æ
è

fold(e,m,f,l), fold(e,m,f,l₁)

ö
ø

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.

(a)

[[right unit, step]] Since (t;*) = t by the induction hypothesis,

cons(h,t);* = cons(h,(t;*)) = cons(h,t).

(b)

[[associativity, base]] *;(l₁;l₂) = l₁;l₂ = (*;l₁);l₂.

(c)

[[step]] omitted eqnarray* environment

Write [[l]] = fold(e,m,f,l), so

(a): [[base]] m([[*]] ,[[l₁]]) = m(e,[[l₁]]) = [[l₁]] = [[*; l₁]]
(b): [[step]] omitted eqnarray* environment

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.

(a)

length(l) = fold(0,+,(lx .1),l) Î N.

(b)

reverse(l) = fold(*,( ll₁,l₂. l₂;l₁), (lx.cons (x,*)),l) Î List(X).

(c)

fold(0,+,id,l) is the sum of the elements.

(d)

map(f,l) = fold(*,(;),f, l) applies a function f:X® Y to each of the elements of a list ``in parallel,'' so

mapf (cons(h::t)) = cons

æ
è

f(h),map(f,t)

ö
ø

(it is the effect of the functor List:Set ® Set, Section 4.4).

(e)

fold(^,Ú,(lx.y = x),l) is a proposition, namely whether the value y occurs as an element of l.

(f)

fold(Æ,È,(lx.{x}), l) Î P(X) provides the set of elements of l.

(g)

If equality in X is decidable, fold(0,+,(l x.x = y),l) Î N counts the occurrences of y in l, where ``x = y'' is the function which returns 1 if they're equal and 0 otherwise.

(h)

l® fold(*,(;),id, l):List(List(X))® List(X) flattens a list of lists.

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 prooftree environment omitted prooftree environment

The elimination rule resembles that for the sum type (case analysis, Remark 2.3.10) in that it has to provide for these two cases,

omitted prooftree environment

where \opz_Q and \ops_Q are arbitrary terms of these types, possibly involving parameters from the context G. The two cases are each matched by the b-rules, which say how to compute with rec,

omitted eqnarray* environment

EXAMPLE 2.7.8 Addition and multiplication are defined by

m+n = rec(m,succ,n) and mxn = rec

æ
è

0,(m+(-)),n

ö
ø

For factorial, we need the argument n in the evaluation phase (Definition 2.5.1(c)). Exercise 2.46 uses pairs to reduce this to the basic case.

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 non-judgemental 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 (non-overlapping). 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 side-conditions involving the outermost operation-symbol(s). Sometimes we have to parse more than once, the general procedure being unification (Section 6.5).

Type-theoretic rules for lists We shall now give the Gentzen-style 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 prooftree environment omitted prooftree environment

Again the elimination rule has to provide for these two cases,

omitted prooftree environment

which are matched by the b-rules, saying how to compute with listrec,

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 a-equivalence ( 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:

(a): One constant (variously called 0, *, [ ], \EMPTY or nil), together with one unary operation ( succ or ln.n+1), or in general ( lt.cons(h,t)) for each element h Î X, and no laws. For any other such structure (Q,\opz_Q ,\ops_Q ), listrec defines the unique mediating homomorphism.
(b): A single associative binary operation (+ or ;) with a unit (0, etc ) and a generator 1, or h for each element h Î X. The mediating homomorphism is given by fold. []

No analogue of Proposition 2.7.5 is needed in the unary case. In fact

fold(e,m,f,l) = listrec(e,\ops_Q , l), where \ops_Q (x,u) = m(f(x),u),

defines fold in terms of listrec. However, to make the elimination rule into a bijective adjoint correspondence we must use fold and not listrec, as the term below the line is a monoid homomorphism (Example 7.2.8).

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).

omitted prooftree environment

(There is no connection between z and \opz_Q at the moment: this notation will make more sense in Section 6.4.)

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 type-theoretic phenomenon for which we haven't yet given the propositional analogue. This is induction for the reflexive-transitive 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.