Structural Recursion

Foundations must be built on a sound layer of ballast. The edifice of mathematics
rests on calculi of expressions composed of symbols written on paper or coded
in a computer. To make a mathematical study of this edifice itself, or of the
ways of handling expressions mechanically, we must consider the completed
infinities of formulae, such as **N**. Since these completed infinities
have no existence as objects in the real world, but only as characters in the
drama of mathematics, this kind of study ( *meta-*mathematics) must
be made within a pre-existing mathematical context. This is why we are doing
it in Chapter VI and not Chapter I.

Mathematically, the algebras of formulae are *free* for certain
free theories, whose operations are the connectives and proof rules of logic
and type theory. In the category-theoretic tradition, a free algebra is
the *initial object* in the category of all algebras. However, the
very general nature of universal properties - the fact that this mode of
description applies to so many other mathematical phenomena, as we have
seen - means that this does not give a ``hands on'' appreciation of term
algebras.

In formal languages, terms cannot be equal unless they have been built in
the same way. Since they are *put together* with connectives such
as +, Ù and $, they form an algebra, but, unlike the
arithmetical examples which motivated Section 4.6,
they can also be *taken apart* - parsed by analysis into cases.
This leads to the techniques of structural recursion, which we have been
using from the first page of this book, and unification, the subject of Section
6.5. We shall characterise, and thereby construct,
the free algebras for free theories, by the property that the parsing operation
is well defined and well founded, *ie* that it terminates (Section
6.3).

Section 6.4 specialises to tail recursion, which can
be implemented more efficiently using imperative **while**
programs. The interpretation in this case is described in terms of coequalisers,
from the previous chapter.

The properties of term algebras also hold for infinitary operations. More
careful consideration, indeed, shows that notions of induction are needed
to capture finiteness, and not *vice versa* (Section
6.6).

The mathematisation of symbolism also gives us the means to create new
mathematical worlds *inside* existing ones, for example in a model
of set theory or in a topos of sheaves. In this book we have been careful to make
clear which logical connectives are needed for each application, rather
than rely globally on higher order logic: cartesian closed categories are
used in functional programming, and pretoposes serve many of the purposes
of universal algebra. Certain *other* structure is needed in the
*meta-logic* to express or construct these features, so for example
we might treat the l-calculus symbolically using algebraic tools.
Category theory, unlike symbolic logic, is well adapted to the parallel
treatment of different fragments, because it can both *represent*
logical structure very naturally and also *be represented* in a clear
combinatorial way.

Set theory tried to deal with both the internal and external structure, though it was particularly ill suited to universal algebra. The inductive hierarchy of sets, on which mathematics was allegedly founded, is defined using the quantifiers, and Lemma 6.3.12 shows that it also relies on the Pasting Lemma 5.8.9. Nevertheless, set theory does throw some light on induction: Section 6.3 uses category theory to generalise some of its ideas and apply them to new inductive situations.

One reason for the difficulty in understanding set-theoretic induction was that the ordinals, as traditionally presented, depend heavily on excluded middle. My original draft of this chapter contained material from set theory which was embarrassingly old fashioned. I tried to develop a simple intuitionistic account of the ordinals; such an account now exists in [ JM95], [Tay96a] and [Tay96b], and is summarised at the end of the chapter, though it is hardly simple. But the motivating problem was solved in the mean time in a more elementary way (Exercise 3.45 ).

The sections of this chapter depend very little on one another.