Constructing Recursion Operators in Intuitionistic Type Theory

Lawrence C Paulson Computer Laboratory Corn Exchange Street Cambridge CB2 3QG England

October 1984

Abstract

Martin-Löf’s Intuitionistic Theory of Types is becoming popular for formal reasoning about computer programs. To handle recursion schemes other than primitive recursion, a theory of well-founded relations is presented. Using primitive recursion over higher types, induction and recursion are formally derived for a large class of well-founded relations. Included are < on natural numbers, and relations formed by inverse images, addition, multiplication, and exponentiation of other relations. The constructions are given in full detail to allow their use in theorem provers for Type Theory, such as Nuprl. The theory is compared with work in the field of ordinal recursion over higher types.

Contents

1 Introduction 3

2 Notation 5

3 Backwards proof 7

4 Well-founded relations in Type Theory 8

5 Defining Quicksort by well-founded recursion 10

6 The less-than ordering on the natural numbers 12 6.1 Induction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 6.2 Recursion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13

7 Subrelations 14 7.1 Induction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 7.2 Recursion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15

8 Inverse image 15 8.1 Induction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 8.2 Recursion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17

9 Transitive closure 17 9.1 Induction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 9.2 Recursion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18

10 Disjoint sum 19 10.1 Induction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 10.2 Recursion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20

11 Lexicographic product 21 11.1 Induction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 11.2 Recursion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22

12 Lexicographic exponentiation 23 12.1 Definition of power types . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 12.2 Induction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 12.3 Intermezzo . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 12.4 Recursion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 13 Wellordering types 30

13.1 Induction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 13.2 Recursion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32

14 A characterization of well-founded relations 32

15 Well-founded relations in the literature 33

16 Questions 36 16.1 Computation on proof objects . . . . . . . . . . . . . . . . . . . . . . . . . . 36 16.2 Does induction entail recursion? . . . . . . . . . . . . . . . . . . . . . . . . . 37

1 Introduction

Per Martin-Löf originally developed his Intuitionistic Type Theory [15] as a formal notation for constructive mathematics, but it may also be regarded as a programming language [14]. It supports the principle of propositions as types: there is a type forming operator for each logical connective and quantifier, with typing rules that correspond to the intuitionistic rules of natural deduction. This type structure is rich enough to completely specify computational problems: Nordström and Smith specify a program to produce a KWIC index [17]. Its potential for the systematic development for correct programs is attracting the interest of computer scientists [1, 3].

Many people have used the interactive theorem prover LCF to verify functional programs by computer. Most LCF work until now [10, 18] has been conducted in a logic for domain theory. Petersson [21] has already implemented a version of LCF for Intuitionistic Type Theory (henceforth Type Theory). Constable’s group has implemented an elaborate theorem prover, called Nuprl, for a version of Type Theory [6]. I am also experimenting with Type Theory in a new theorem prover, Isabelle [19].

Type Theory has no explicit principle of general recursion: it forces all functions to terminate by allowing only primitive recursion. Many functions that are not primitive recursive can be defined as primitive recursive functionals: the classic example is Ackermann’s function [16]. The study of functionals leads to a simple theory of types, including at least the natural numbers Nat, and function types A → B if A and B are types [27]. Each type A can be assigned a level L(A) such that L(Nat) = 0 and L(A → B) is the greater of L(A) + 1 and L(B). (This scheme of type levels is too simple for Intuitionistic Type Theory.) Primitive recursive functionals are also called primitive recursive functions of higher type.

Primitive recursive functionals do not consititute a natural programming language. To facilitate reasoning about programs in Type Theory, this paper formalizes a more conventional programming style: writing arbitrary recursion equations annotated with a termination proof.

Every computer scientist knows of Quicksort, a total function not obviously definable by primitive recursion. Jan Smith [24] defines Quicksort in Type Theory by first deriving appropriate rules of induction and recursion, using primitive recursion over higher types. The “while rule” of Backhouse and Khamiss [1] is also a form of primitive recursion. This paper considers induction and recursion over a wide class of well-founded (w.f.) relations.

The rule of induction over a well-founded relation ≺ is

\frac{∀x. (∀x′ ≺ x. P (x′)) → P (x)}{∀x. P (x)} .

Classically, this rule is sound if ≺ has no infinite descending chains x_{1} ≻ x_{2} ≻ · · ·. W.f. induction (or Noetherian induction) is often used in program verification, and is the fundamental method for proving termination [11]. Total functions can be defined by the related principle of w.f. recursion.

Even if it is apparent that a relation is w.f., proving this may be difficult. W.f. relations are most easily constructed from simpler ones, using rules that preserve the w.f. property. Later sections present Type Theory derivations of induction and recursion over

• the ordering < on the natural numbers

• a subrelation of a w.f. relation

• the inverse image of a w.f. relation

• the transitive closure of a w.f. relation

• the disjoint sum of two w.f. relations

• the lexicographic product of two w.f. relations

• the lexicographic power of a w.f. relation

• the immediate subtree relation on a wellordering type.

These ideas have been extensively studied by both computer scientists and logicians. Manna and Waldinger [13] describe and verify similar rules for w.f. relations. The sole induction principle of the Boyer-Moore theorem prover [2] is w.f. induction, over lexicographic products of inverse images of <. The theory of ordinal recursion concerns recursion over total wellorderings constructed by addition, multiplication, and exponentiation of simpler wellorderings [26]. These operations suffice to reach wellorderings of order type ϵ_{0}, which is the first ordinal α to satisfy ω^{α} = α. The functions definable by ordinal recursion up to ϵ_{0} include all functions provably recursive in Peano arithmetic. Terlouw’s work on ordinal recursion over higher types [27] is related to the rule for powers in section 12.

It should not surprise anyone that various principles of w.f. recursion can be developed within Intuitionistic Type Theory. The point of this paper is to present the derivations in full detail. They can be used with a mechanical theorem prover like Nuprl. The present set of w.f. relations is complete in two senses. (1) It includes nearly all the w.f. relations I have encountered in the literature. (2) The set includes order types well beyond ϵ_{0}, indeed any ordinal that a proof of program termination could reasonably require.

The paper assumes a basic knowledge with Type Theory. Good introductions include Martin-Löf [14, 15] and Nordström and Smith [17]. Jan Smith [25] presents the inference rules and gives a formal interpretation of the semantics. Each section begins with an easy introduction, then becomes increasingly formal. At any point you may skip to the next section. The remaining sections

• describe a notation for Type Theory;

• describe the LCF style of backwards proof used in this paper; • formalize w.f. relations, induction, and recursion operators in Type Theory;

• define the function Quicksort using a recursion operator, and show that it satisfies the usual recursion equations;

• derive w.f. induction and recursion for each rule for constructing w.f. relations,

• show that w.f. relations are precisely the inverse images of wellordering types;

• use the rules to construct w.f. relations taken from the literature;

• comment on drawbacks and questions about the approach.

2 Notation

There is a lamentable diversity of notations for Type Theory. Constable and Backhouse have completely different notations; Martin-Löf’s has evolved between his earlier and later papers. The notation of Chalmers University [17] is Martin-Löf’s except for the names of the selectors. The application of the function f to arguments a_{1}, …, a_{n} is written f(a_{1}, …, a_{n}); the abstraction of an expression c over the variables x_{1}, …, x_{n} is written (x_{1}, …, x_{n})c. A function of several arguments is regarded as a function-valued function, a device known as currying; so f(a, b) abbreviates f(a)(b), and (x, y)c abbreviates (x)(y)c.

My notation for Type Theory is similar. Types include

⊥, the empty type

⊤, the type containing the one value 0

Bool, the type of truth values {T, F}

a =_{A} a′, the equality type Eq(A, a, a′), where A is a type (the subscript A may be omitted if obvious from context)

The selectors take their arguments in an unconventional order: the argument p being eliminated appears last rather than first. If the constructions c, c_{0}, c_{1}, … have type C, then so do the following selections. Each is listed together with Martin-Löf’s version [15]:

For p ∈ ⊥, I use contr(p) instead of R_{0}(p).

For p ∈ Bool, I use cond(c_{1}, c_{2}, p) instead of R_{2}(p, c_{1}, c_{2}).

For p ∈ A × B, I use split((x, y)c, p) instead of E(p, (x, y)c).

For p ∈ A + B, I use when((x)c_{1}, (y)c_{2}, p) instead of D(p, (x)c_{1}, (y)c_{2}).

For p ∈ Nat, I use natrec(c_{0}, (x, y)c_{1}, p) instead of R(p, c_{0}, (x, y)c_{1}), similarly for listrec, transrec, etc.

This argument order works well with curried functions. For instance, cond(c_{1}, c_{2}) means the same as (p) cond(c_{1}, c_{2}, p); it is a function on type Bool, mapping T to c_{1} and F to c_{2}. If f, g, and h are appropriate functions, then split(f) is a function with domain A × B and when(g, h) is a function with domain A + B. The advantages of this argument order are apparent in complex expressions involving selectors, such as

λ(when(natrec(p, q), split((x) split((y, z)r(x, y, z))))) ,

which could have type (Nat+(A×(B ×C))) → D. The standard argument order requires additional variables v_{1}, v_{2}, v_{3}, v_{4}, denoting intermediate values that we have no wish to see:

λv_{1}. when(v_{1}, (v_{2}) natrec(v_{2}, p, q), (v_{3}) split(v_{3}, (x, v_{4}) split(v_{4}, (y, z)r(x, y, z))))

Actually, the details of selectors are not important; in my presentation of proof constructions, most selectors are banished in favor of new functions and equations defining them.

The pair of a and b is written ⟨a, b⟩. The functions fst and snd are special cases of split, with fst(⟨a, b⟩) = a and snd(⟨a, b⟩) = b. The application of the function object f to the object a is written f ∗ a rather than the usual apply(f, a). The canonical objects of a function type have the form λ((x)b), which may equivalently be written in the traditional lambda style, λx.b . When d is a large expression, λ(d) is simpler and clearer than λx.d(x).

Here are a few inference rules in the notation:

→ and Π elimination

\frac{f ∈ ∏_{x∈A} B(x) a ∈ A}{f ∗ a ∈ B(a)}

× and Σ introduction

\frac{a ∈ A b ∈ B(a)}{⟨a, b⟩ ∈ ∑_{x∈A} B(x)}

× and Σ elimination

\frac{\begin{matrix}[x ∈ A; y ∈ B(x)] \\ c(x, y) ∈ C(⟨x, y⟩) \end{matrix} p ∈ ∑_{x∈A} B}{split(c, p) ∈ C(p)}

+ elimination

\frac{\begin{matrix}[x ∈ A] \\ c_{A}(x) ∈ C(inl(x)) \end{matrix}  \begin{matrix}[y ∈ B] \\ c_{B}(y) ∈ C(inr(y)) \end{matrix}  p ∈ A + B}{when(c_{A}, c_{B}, p) ∈ C(p)}

Nat elimination

\frac{c_{0} ∈ C(0)  \begin{matrix}[x ∈ Nat; u ∈ C(x)] \\ c_{1}(x, u) ∈ C(succ(x)) \end{matrix}  p ∈ Nat}{natrec(c_{0}, c_{1}, p) ∈ C(p)}

Classically, a wellordering is a linear well-founded relation. Martin-Löf’s wellordering type is a general kind of tree structure. Both uses of ‘wellordering’ are firmly established. To prevent confusion, I always write ‘wellordering type’ for Martin-Löf’s usage, and ‘wellordering’ for the classical usage.

The rule for wellordering elimination uses the latest innovation, hypothetical hypotheses. A hypothesis of the form f(x) ∈ B [x ∈ A] asserts that f is a function from A to B.

This is hardly different from the assumption f ∈ A → B, but allows the wellordering types to be defined without mention of function types. The types in Type Theory are defined independently of each another.

\frac{p ∈ W_{x∈A} B(x) \begin{matrix}[ & \begin{matrix}x ∈ & A \\ f(z) ∈ & W_{x∈A} B(x) & [z ∈ B(x)] \\ u(z) ∈ & C(f(z)) & [z ∈ B(x)] \end{matrix} & ] \\ & c(x, f, u) ∈ C(sup(x, f)) \end{matrix}}{transrec(c, p) ∈ C(p)}

I make occasional, non-essential use of the subtype {x ∈ A | B(x)}. This is similar to the type ∑_{x∈A} B(x), but its elements are those of A instead of pairs ⟨a, b⟩. Subtypes are convenient when B(x) represents a proposition such as equality, whose elements are uninteresting. Constable gives a fuller explanation [5, page 74], as does Petersson [22]. Rules include

type formation

\frac{A type \begin{matrix}[x ∈ A] \\ B(x) type \end{matrix}}{\{x ∈ A | B(x)\} type}

introduction

\frac{a ∈ A b ∈ B(a)}{a ∈ \{x ∈ A | B(x)\}}

elimination

\frac{a ∈ \{x ∈ A | B(x)\} \begin{matrix}[x ∈ A; B(x) true] \\ c(x) ∈ C(x) \end{matrix}}{c(a) ∈ C(a)}

The assumption B(x) true means that B(x) is a true proposition, namely that the type B(x) contains an element. Such reasoning can be formalized by introducing a set of rules about true propositions. An alternative is to regard this assumption as an abbreviation of y ∈ B(x), with the restriction that y must not appear free elsewhere in the rule.

3 Backwards proof

A traditional method of searching for a proof is to work backwards from goals to subgoals. For instance, to prove A ∧ B, it suffices to prove A and B separately. Backwards proof is more difficult in Type Theory: the goal would be written p ∈ A × B, for an unknown construction p. As the proof proceeds, constraints upon p accumulate; when the proof is finished, they determine p completely. Recording the constraints requires tedious bookkeeping, whether the proof is conducted by hand or by computer. The LCF architecture does not allow unknown expressions in goals, so Petersson’s Type Theory system does not support backwards proof. Nuprl [6] works explicitly with types only, handling constructions internally.

I have worked out the proofs in this paper by hand. If the type A represents a proposition to be proved, then the initial goal is p ∈ A, for some construction p. In proving p ∈ A, each backwards step decomposes the type A, incrementally discovering the structure of p. The letters p, q, r, … stand for unknown constructions.

Unification gives a flexible treatment of unknown expressions in goals [19]. An inference rule

\frac{Φ_{1}(p⃗)  ⋯  Φ_{n}(p⃗)}{Φ(p⃗)} ,

where p⃗ stands for a vector of unknowns, specifies a way to reduce a goal Φ to subgoals Φ_{1}, …, Φ_{n}. Suppose that the goal is Ψ(q⃗), and that the vector of expressions a⃗ unifies the goal with the conclusion of the rule: Φ(a⃗) is identical to Ψ(a⃗). Then instantiating the unknowns p⃗ and q⃗ reduces Ψ(q⃗) to Φ_{1}(a⃗), ⋯, Φ_{n}(a⃗). The unifier a⃗ may contain new unknowns. Most hand proofs only require trivial unifications.

Backwards proof is natural for both discovering and presenting formal proofs. Consider this backwards proof of the Axiom of Choice. You might compare it with Martin-Löf’s forwards proof [14, 15].

It suffices to find some construction choice of type

( ∏_{x∈A} ∑_{y∈B(x)} C(x, y)) → ∑_{f∈Π(A,B)} ∏_{x∈A} C(x, f(x)) .

By product introduction, choice could be λz.p, where

p ∈ ∑_{f∈Π(A,B)} ∏_{x∈A} C(x, f(x)) [ z ∈ ∏_{x∈A} ∑_{y∈B(x)} C(x, y) ] .

By sum introduction, p could be the pair ⟨f, q⟩, where f ∈ Π(A, B) and q ∈ ∏_{x∈A} C(x, f(x)) . First try to find f. By product introduction, f could be λx.r, where

r ∈ B(x) [ \begin{matrix}z & ∈ ∏_{x∈A} ∑_{y∈B(x)} C(x, y) \\ x & ∈ A \end{matrix} ] .

Product elimination gives z ∗ x ∈ ∑_{y∈B(x)} C(x, y) . By sum elimination, r is fst(z ∗ x), and f = λx. fst(z ∗ x); by similar reasoning, q = λx. snd(z ∗ x). Putting the pieces together gives

choice = λz. ⟨λx. fst(z ∗ x), λx. snd(z ∗ x)⟩ .

4 Well-founded relations in Type Theory

In Type Theory, the rule of w.f. induction can be stated as

\frac{a ∈ A \begin{aligned}[ & \begin{aligned}x & ∈ A \\ ih(x′, ls) & ∈ P (x′) [x′ ∈ A; ls ∈ x′ ≺ x] \end{aligned} & ] \\ & s(x, ih) ∈ P (x) \end{aligned}}{wfrec(s, a) ∈ P (a)} .

(Note that the induction hypothesis ih is itself hypothetical.) The operator wfrec can be used to define functions on A. From our understanding of w.f. recursion, it is natural to expect wfrec to satisfy the recursion rule

\frac{(premises as above)}{wfrec(s, a) = s(a, (x, ls) wfrec(s, x)) ∈ P (a)} .

Definition. A binary relation ≺ on a type A is well-founded (w.f.) precisely when the rules of w.f. induction and recursion hold.

A w.f. relation need not be transitive, hence need not be an ordering. It must be irreflexive and asymmetric. The recursion rule has a key advantage: its conclusion does not make use of the propositional variable ls. This variable justifies the recursion but plays no role in computation. When using a function f defined by w.f. recursion, the induction rule serves to prove facts about f, while the recursion rule allows computation of f. By w.f. induction, it is trivial to prove that wfrec gives the unique solution to this recursion equation.

The symbol wfrec denotes a complex Type Theory construction dependent upon the relation ≺. A version of wfrec is derived for each w.f. relation considered below. For a w.f. relation defined in terms of other w.f. relations, its wfrec invokes the wfrec of those relations.

How does wfrec compare with the fixedpoint operator of domain theory? For x ∈ A, let [A]_{≺x} denote the subtype of A below x, namely {x ∈ A | x ≺ a}. Roughly speaking, w.f. recursion produces a total function of type A → B given something that maps x ∈ A to ([A]_{≺x} → B) → B. Domain theory produces a function of type A → B, given something of type (A → B) → (A → B). So the two recursion operators have similar functionality.

The universe rules of Type Theory allow us to form universes of w.f. relations, with induction and recursion restricted to small types. Abstract over the rules’ premises, including implicit ones like P (x) type. For the type of a w.f. induction step, use the abbreviation

STEP(A, ≺, P) ≡ ∏_{x∈A} ( ∏_{x′∈A} x′ ≺ x → P ∗ x′) → P ∗ x.

The universe WF_{0} of small w.f. relations is

∑_{A∈U_{0}} ∑_{≺∈A×A→U_{0}}
∏_{P ∈A→U_{0}} ∏_{step∈STEP(A,≺,P)}

{wf ∈ ∏_{x∈A} P ∗ x | ∏_{x∈A} wf ∗ x =_{P ∗x} step ∗ x ∗ (λx′ ls.wf ∗ x′)}

Derivations of w.f. relations can be regarded as constructions within WF_{0}. The ordering < is an element of WF_{0}; lexicographic product is a binary operation on WF_{0}, etc. Members of WF_{0} have the form ⟨A, ⟨≺, wf⟩⟩. If P (x) ∈ U_{0} for any x ∈ A, then w.f. induction and recursion hold under the definition

wfrec(s, a) ≡ wf ∗ λ(P) ∗ (λx ih.s(x, (x′, ls)ih ∗ x′ ∗ ls)) ∗ a .

5 Defining Quicksort by well-founded recursion

Before plunging into the formal derivations of w.f. induction and recursion, let us see how to use these rules to reason about recursive functions in Type Theory. Consider an example due to Jan Smith [24]. If A is a type with some total ordering of type A×A → Bool, then any list of elements of A can be sorted into ascending order. Quicksort sorts a non-empty list cons(a, l) by partitioning l into two sublists: one containing the elements that are less or equal to a, and one containing the elements that are greater. It recursively sorts these sublists, then concatenates them.

Smith introduces Quicksort within Type Theory by deriving a new principle of primitive recursion. Below, Quicksort is defined by w.f. recursion over a w.f. relation, ≺. Each recursive call includes an explicit termination argument involving ≺. An unfolding step shows that the resulting function satisfies the usual recursion equations for Quicksort.

Quicksort terminates because the length of the list is smaller in each recursive call. The function length is defined as

length ≡ listrec(0, (x, l, u) succ(u)) .

Thus length satisfies the recursion equations

length(nil) = 0
length(cons(a, l)) = succ(length(l)) .

Henceforth, functions will be defined by recursion equations whenever these can obviously be translated into a formal definition involving natrec, listrec, etc. The two equations for length give a precise and readable definition.

Define the w.f. relation ≺ on lists such that l′ ≺ l means length(l′) < length(l). In other words, ≺ is the inverse image of < under the function length. Quicksort is defined by recursion over ≺. Be careful not to confuse the total ordering on A with the w.f. relation on List(A).

Partitioning the input list requires a function filter. Given a predicate function pf ∈ A → Bool, and a list, filter returns the list of elements for which pf returns T:

filter(pf , nil) = nil
filter(pf , cons(a, l)) = \{ \begin{matrix}cons(a, filter(pf , l)) & if pf ∗ a = T \\ filter(pf , l) & if pf ∗ a = F \end{matrix}

It is straightforward to prove that filter does not make the list longer:

length(filter(pf , l)) ≤ length(l) true

A corollary of this, needed to justify the recursion of Quicksort, is (for some construction qless)

[ pf ∈ A → Bool; x ∈ A; l ∈ List(A) ] qless(pf , x, l) ∈ length(filter(pf , l)) < length(cons(a, l)) ,

or equivalently qless(pf , x, l) ∈ filter(pf , l) ≺ cons(a, l) .

Two predicate functions provide the ordering used for sorting:

before(a) ∗ b  whether b is less than or equal to a
after(a) ∗ b  whether b is greater than a.

Let ⊕ denote the append operation on lists (concatenation). We would like to establish the usual recursion equations for Quicksort, namely

quick(nil) = nil
quick(cons(a, l)) = (quick(filter(before(a), l)))

⊕ cons(a, quick(filter(after(a), l))) .

Defining Quicksort by w.f. recursion requires defining an induction step s(l, ih) in terms of a list l and induction hypothesis

ih(l′, ls) ∈ List(Nat) [ l′ ∈ List(Nat); ls ∈ l′ ≺ l ] .

The induction hypothesis allows a recursive call for any list l′ smaller than l. A proof of l′ ≺ l must be supplied as an argument. This proof will be a construction, involving qless, of type l′ ≺ l. Since the list may be empty or not, the definition of s considers two cases:

s(nil, ih) = nil
s(cons(a, l), ih) = ih(filter(before(a), l), qless(before(a), a, l))

⊕ cons(a, ih(filter(after(a), l), qless(after(a), a, l)))

Now Quicksort is just quick ≡ wfrec(s). To produce the familiar recursion equations, unfold quick according to the recursion rule for wfrec:

quick(l) = s(l, (l′, ls)quick(l′))

The termination arguments involving qless drop out:

quick(cons(a, l)) = s(cons(a, l), (l′, ls)quick(l′))
= (quick(filter(before(a), l)))

⊕ cons(a, quick(filter(after(a), l)))

Quicksort is correct if its result is always an ordered permutation of its argument. The proof involves w.f. induction, where the induction hypothesis states that quick is correct in its recursive calls. Manna and Waldinger verify Quicksort in detail [13].

How efficient is the execution of Quicksort in Type Theory? A detailed analysis of Quicksort’s version of wfrec is required. Efficiency questions are particularly delicate because Type Theory programs are executed under lazy evaluation. Ideally, Quicksort’s recursion equations should be executed directly as rewrite rules: we know that they represent a terminating computation.

6 The less-than ordering on the natural numbers

Well-founded induction over the ordering < on natural numbers is the familiar course-of-values induction. It is easy to derive from mathematical induction, just as course-of-values recursion is easy to derive from primitive recursion. The relation < is defined to satisfy (remember that + denotes disjoint union!)

\begin{matrix}m < 0 = & ⊥ \\ m < succ(n) = & (m =_{Nat} n + m < n). \end{matrix}

The substructure relation for lists and other tree-like types is analogous to <. Manna and Waldinger use w.f. induction on this relation for their l-expressions [12]. I was surprised to discover that w.f. induction on l-expressions has essentially the same derivation as that for <. However, we shall see later on that the substructure relation for any tree-like type follows from the rules for wellordering types and transitive closure.

6.1 Induction

Assume throughout that P (n) is a type for n ∈ Nat, and assume the induction step

step ∈ ∏_{n∈Nat} ( ∏_{m∈Nat} m < n → P (m)) → P (n) .

To justify w.f. induction, it suffices to find wf ∗ n ∈ P (n) for n ∈ Nat. Appealing to the induction step, wf could be λn.step ∗ n ∗ p(n), where

p(n) ∈ ∏_{m∈Nat} m < n → P (m) .

By natural number induction, p(n) could be natrec(p_{0}, p_{1}, n), where

p_{0} ∈ ∏_{m∈Nat} m < 0 → P (m).

and

p_{1}(n, u) ∈ ∏_{m∈Nat} m < succ(n) → P (m) [ \begin{matrix}n & ∈ Nat \\ u & ∈ ∏_{m∈Nat} m < n → P (m) \end{matrix} ] .

Clearly p_{0} is λm ls.contr(ls) . By product introduction and unfolding the less-than relation, p_{1}(n, u) could be λm ls.p_{2}, where

p_{2} ∈ P (m) [ n; u; m ∈ Nat; ls ∈ m = n + m < n ] .

To save space, I have abbreviated the assumptions n ∈ Nat and

u ∈ ∏_{m∈Nat} m < n → P (m)

as n and u. By + elimination, p_{2} could be when(q_{1}, q_{2}, ls), where

q_{1}(e) ∈ P (m) [ n; u; m; e ∈ m = n ]

and

q_{2}(ls) ∈ P (m) [ n; u; m; ls ∈ m < n ] .

The induction hypothesis u solves both goals. Replacing m by n, the w.f. induction step gives q_{1}(e) = step ∗ n ∗ u; also q_{2}(ls) = u ∗ m ∗ ls.

The definition of wf is too long to work with directly. Instead we can derive a set of equations for it, retaining p as an auxiliary function. Even p is inconveniently complex. It involves the selectors natrec and when. Therefore it is described by equations where the selectors can be eliminated:

p(0) ∗ m ∗ ls = contr(ls)  ∈ P (m)  [ls ∈ m < 0]
p(succ(n)) ∗ m ∗ inl(eq) = step ∗ m ∗ p(n) ∈ P (m)  [eq ∈ m = m]
p(succ(n)) ∗ m ∗ inr(ls) = p(n) ∗ m ∗ ls ∈ P (m)  [ls ∈ m < n]
wf ∗ n = step ∗ n ∗ p(n) ∈ P (n)

Most of derivations of constructions in this paper end with such equations, which summarize the derivation. The following proof of the recursion rule illustrates that the equations provide the needed information in a convenient form.

6.2 Recursion

The desired property is

wf ∗ n = step ∗ n ∗ (λm ls.wf ∗ m) ∈ P (n) [ n ∈ Nat ] .

Unfolding wf, it remains to show

step ∗ n ∗ p(n) = step ∗ n ∗ (λm ls.wf ∗ m) ∈ P (n) [ n ∈ Nat ] .

Canceling (product elimination and introduction), it is enough to show

p(n) ∗ m ∗ ls = wf ∗ m ∈ P (m) [ n; m ∈ Nat; ls ∈ m < n ] .

By equality and product elimination, it is enough to show

∏_{ls∈m<n} p(n) ∗ m ∗ ls =_{P (m)} wf ∗ m true [ n; m ∈ Nat ] .

By natural number induction on n, and product introduction, it remains to show

p(0) ∗ m ∗ ls = wf ∗ m ∈ P (m) [ m ∈ Nat; ls ∈ m < 0 ] ,

which holds by the contradiction m < 0, and also to show

[ \begin{matrix}m & ∈ Nat \\ n & ∈ Nat \\ u & ∈ ∏_{ls∈m<n} p(n) ∗ m ∗ ls =_{P (m)} wf ∗ m \\ ls & ∈ m = n + m < n \end{matrix} ] p(succ(n)) ∗ m ∗ ls = wf ∗ m ∈ P (m) .

By + elimination, it remains to consider two cases, using the appropriate equation for p(succ(n)):

step ∗ n ∗ p(n) = wf ∗ n ∈ P (n) [ m; n; u; e ∈ m = n ]

and

p(n) ∗ m ∗ ls = wf ∗ m ∈ P (m) [ m; n; u; ls ∈ m < n ]

The first goal is the equation for wf; the second is an instance of the induction hypothesis.

7 Subrelations

This paper is less concerned with particular w.f. relations like < as it is with rules for constructing w.f. relations from others. The simplest rule concerns subrelations of w.f. relations. Suppose that ≺ is a w.f. relation on the type A, and that ≪ is a subrelation of ≺, namely there is a function f satisfying

f(x′, x, lt) ∈ x′ ≺ x [ x ∈ A; x′ ∈ A; lt ∈ x′ ≪ x ] .

Then A is w.f. by the relation ≪.

A typical use of this rule is to justify w.f. induction on the ‘properly divides’ relation on natural numbers [13]. If m properly divides n, then m < n. But the main application in Type Theory is when one relation is logically equivalent to another. A proposition may be expressed as many different types; this rule provides compatibility between them.

For instance, the proof that < is w.f. uses a particular definition of <. You may prefer to work with the logically equivalent definition

m ≪ n ≡ ∑_{k∈Nat} succ(m plus k) = n .

In order to justify w.f. induction on ≪, you need only show that m ≪ n implies m < n.

7.1 Induction

Assume throughout that P (x) is a type for x ∈ A, and assume the induction step

step ∈ ∏_{x∈A} ( ∏_{x′∈A} x′ ≪ x → P (x′)) → P (x).

It suffices to find wf ∗ x ∈ P (x) for x ∈ A. Since the relation ≺ is w.f., induction gives wf = λx. wfrec(s, x), where

s(x, ih) ∈ P (x) [ \begin{matrix}x & ∈ A \\ ih(x′, ls) & ∈ P (x′) [x′ ∈ A; ls ∈ x′ ≺ x] \end{matrix} ] .

Using the induction step, s(x, ih) could be step ∗ x ∗ t, where

t ∈ ∏_{x′} x′ ≪ x → P (x′).

By product introduction, t is λx′.λlt.ih(x′, f (x′, x, lt)), and we have

s(x, ih) = step ∗ x ∗ (λx′ lt.ih(x′, f(x′, x, lt))).

7.2 Recursion

Since A is w.f. under ≺, it satisfies the recursion rule

wfrec(s, a) = s(a, (x, ls) wfrec(s, x)).

The recursion rule A under ≪ is easy to prove, by unfolding wf:

wf ∗ x = wfrec(s, x)
= s(x, (x′, ls)wf ∗ x′)
= step ∗ x ∗ (λx′ lt.((x′, ls)wf ∗ x′)(x′, f(x′, x, lt)))
= step ∗ x ∗ (λx′ lt.wf ∗ x′).

8 Inverse image

Suppose that ≺_{B} is a w.f. relation on the type B, and that f is a function such that f(x) ∈ B if x ∈ A. Define the relation ≺_{A} on A as the inverse image of ≺_{B} under f:

x′ ≺_{A} x ≡ f(x′) ≺_{B} f(x).

A function used for this purpose is often called a rank or measure function. Measure functions play the central role in the induction principle of Boyer and Moore [2], and in my characterization of w.f. types (Section 14).

8.1 Induction

Assume throughout that, if x ∈ A, then P (x) is a type and f(x) ∈ B. Also assume

step ∈ ∏_{x∈A} ( ∏_{x′∈A} x′ ≺_{A} x → P (x′)) → P (x)

It suffices to find wf ∗ x ∈ P (x) for x ∈ A. By reflexivity, equality introduction, substitution, and product elimination, wf could be λx.wf_{2} ∗ eq, where

wf_{2} ∈ (f(x) =_{B} f(x)) → P (x) [ x ∈ A ] .

Now rename certain occurrences of x as z: put

R(y) ≡ ∏_{z∈A} (f(z) =_{B} y) → P (z) .

By product elimination, wf_{2} could be wf_{3} ∗ x, where

wf_{3} ∈ R(f(x)) [ x ∈ A ] .

W.f. induction on ≺_{B} gives wf_{3} = wfrec_{B}(s, f(x)), where

s(y, ih) ∈ R(y) [ \begin{matrix}x & ∈ A \\ y & ∈ B \\ ih(y′, ls) & ∈ R(y′) [y′ ∈ B; ls ∈ y′ ≺_{B} y] \end{matrix} ] .

By product introduction, s(y, ih) could be λz e.s_{2}(z, e), where

s_{2}(z, e) ∈ P (z) [ x; y; ih; z ∈ A; e ∈ f(z) =_{B} y ] .

The induction step gives s_{2}(z, e) = step ∗ z ∗ t(y, ih), where

t(y, ih) ∈ ∏_{x′∈A} (f(x′) ≺_{B} f(z)) → P (x′) [ x; y; ih; z; e ] .

Using the assumption f(z) = y, product introduction gives t(y, ih) = λx′ ls.t_{2}, where

t_{2} ∈ P (x′) [ x; y; ih; z; x′ ∈ A; ls ∈ f(x′) ≺_{B} y ] .

By reflexivity and the induction hypothesis, t_{2} is ih(f(x′), ls) ∗ x′ ∗ eq.

Let p(y) ≡ wfrec_{B}(s, y). Then we can summarize the derivation with equations:

t(y, ih) = λx′ ls.ih(f(x′), ls) ∗ x′ ∗ eq ∈ ∏_{x′∈A}(f(x′) ≺_{B} y) → P (x′)
p(y) ∗ x ∗ e = step ∗ x ∗ t(y, (y′, ls)p(y)) ∈ P (x)  [e ∈ f(x) =_{B} y]
wf ∗ x = p(f(x)) ∗ x ∗ eq  ∈ ∏_{x∈A} P (x)

The equation for p uses the recursion rule for ≺_{B}, which is valid under the assumption that ≺_{B} is w.f. This is used in several summaries below, and will not be pointed out again.

8.2 Recursion

The recursion rule for ≺_{A} follows from the equations above:

wf ∗ x = p(f(x)) ∗ x ∗ eq ∈ P (x)
= step ∗ x ∗ t(f(x), (y′, ls)p(y′))
= step ∗ x ∗ (λx′ ls.p(f(x′)) ∗ x′ ∗ eq)
= step ∗ x ∗ (λx′ ls.wf ∗ x′)

9 Transitive closure

A relation ≺ is stronger than its transitive closure ≺^{+}. This means that ≺^{+} gives a more powerful induction rule, while it is easier to prove that ≺ is w.f. We get the best of both worlds by showing that the (irreflexive) transitive closure of any w.f. relation is a w.f. ordering. Suppose that ≺ is a w.f. relation on the type A. The derivation of induction and recursion works for any definition of the transitive closure ≺^{+} satisfying

x′ ≺^{+} x ↔ x′ ≺ x + (∑_{y∈A} x′ ≺^{+} y × y ≺ x) .

The → direction is particularly important: it means there is a construction trcases such that if x′ ∈ A, x ∈ A, and lt ∈ x′ ≺^{+} x, then

trcases(x′, x, lt) ∈ x′ ≺ x + (∑_{y∈A} x′ ≺^{+} y × y ≺ x) .

For example, recursion on the natural numbers defines finite powers ≺^{n} of the relation ≺, satisfying

\begin{matrix}x ≺^{0} y = & (x =_{A} y) \\ x ≺^{succ(n)} z = & ∑_{y∈A} x ≺^{n} y × y ≺ z . \end{matrix}

We can now define the transitive closure ≺^{+}, and the reflexive/transitive closure ≺^{∗} (which is obviously not w.f.):

x ≺^{+} y ≡ ∑_{n∈Nat} x ≺^{succ(n)} y
x ≺^{∗} y ≡ ∑_{n∈Nat} x ≺^{n} y .

The proof for this definition of ≺^{+} uses the Nat elimination rule instead of case analysis on trcases.

9.1 Induction

Assume that P (x) is a type for x ∈ A. Introduce the abbreviation

Q(x) ≡ ∏_{x′∈A} x′ ≺^{+} x → P (x′) .

Assume the induction step, which is simply

step ∈ ∏_{x∈A} Q(x) → P (x) .

It suffices to find wf ∗ x ∈ P (x) for x ∈ A. Using the induction step, wf ∗ x could be step ∗ x ∗ q(x), where q(x) ∈ Q(x). W.f. induction on x gives q(x) = wfrec(s, x), where

\begin{aligned}[ & \begin{aligned}x & ∈ A \\ ih(y, ls) & ∈ Q(y) [y ∈ A; ls ∈ y ≺ x] \end{aligned} & ] \\ & s(x, ih) ∈ Q(x) \end{aligned} .

By product introduction, unfolding ≺^{+} and Q, and sum elimination, s(x, ih) could be λx′ lt.s_{1}, where

s_{1} ∈ P (x′) [ x; ih; x′ ∈ A; lt ∈ x′ ≺^{+} x ] .

Using trcases and + elimination, s_{1} could be when(s_{2}, s_{3}, trcases(x′, x, lt)), where

s_{2}(ls) ∈ P (x′) [ x; ih; x′; ls ∈ x′ ≺ x ]

and also

s_{3}(y, lt, ls) ∈ P (x′) [ x; ih; x′; y ∈ A; lt ∈ x′ ≺^{+} y; ls ∈ y ≺ x ] .

Clearly s_{2}(ls) = step ∗ x′ ∗ ih(x′, ls) and s_{3}(y, lt, ls) = ih(y, ls) ∗ x′ ∗ lt.

Summarizing,

q(x) ∗ x′ ∗ lt_{0} = \{ \begin{matrix}step ∗ x′ ∗ q(x′) & if trcases(x′, x, lt_{0}) = inl(ls) \\ q(y) ∗ x′ ∗ lt ∈ P (x′) & if trcases(x′, x, lt_{0}) = inr(⟨y, ⟨lt, ls⟩⟩) \end{matrix}
wf ∗ x = step ∗ x ∗ q(x) ∈ P (x) .

9.2 Recursion

The desired rule is

wf ∗ x = step ∗ x ∗ (λx′ lt.wf ∗ x′) ∈ P (x) [ x ∈ A ] .

Unfolding wf in the left side, and canceling, it suffices to prove

∏_{lt∈x′≺^{+}x} q(x) ∗ x′ ∗ lt =_{P (x′)} wf ∗ x′ [ x ∈ A; x′ ∈ A ] .

W.f. induction over ≺ on x, followed by product introduction, gives

[ \begin{matrix}x′ & ∈ A \\ x & ∈ A \\ ih(y, ls) & ∈ ∏_{lt∈x′≺^{+}y} q(y) ∗ x′ ∗ lt =_{P (x′)} wf ∗ x′ [y ∈ A; ls ∈ y ≺ x] \\ lt & ∈ x′ ≺^{+} x \end{matrix} ] q(x) ∗ x′ ∗ lt = wf ∗ x′ ∈ P (x′) .

Using trcases(x′, x, lt), it is enough to show both

step ∗ x′ ∗ q(x′) = wf ∗ x′ ∈ P (x′) [ x′; x; ih; ls ∈ x′ ≺ x ] ,

which follows from the definition of wf, and also

q(y) ∗ x′ ∗ lt = wf ∗ x′ ∈ P (x′) [ x′; x; ih; y ∈ A; lt ∈ x′ ≺^{+} y; ls ∈ y ≺ x ] ,

which follows from the induction hypothesis.

10 Disjoint sum

Suppose that ≺_{A} and ≺_{B} are w.f. on the types A and B respectively. The relation ≺ on the type A + B puts the elements of A before the elements of B. With x′, x in A and y′, y in B, it satisfies

inl(x′) ≺ inl(x) = x′ ≺_{A} x
inl(x) ≺ inr(y) = ⊤
inr(y) ≺ inl(x) = ⊥
inr(y′) ≺ inr(y) = y′ ≺_{B} y .

10.1 Induction

Assume that P (z) is a type for all z ∈ A + B, and assume the induction step

step ∈ ∏_{z∈A+B} ( ∏_{z′∈A+B} z′ ≺ z → P (z′)) → P (z).

Before proving P (z) for all z in A+B, consider the special case of finding p(x) ∈ P (inl(x)), for x ∈ A. W.f. induction on ≺_{A} gives p(x) = wfrec_{A}(p_{1}, x), where

p_{1}(x, ih) ∈ P (inl(x)) [ \begin{matrix}x & ∈ A \\ ih_{A}(x′, ls) & ∈ P (inl(x′)) [x′ ∈ A; ls ∈ x′ ≺_{A} x] \end{matrix} ] .

The induction step gives p_{1}(x, ih_{A}) = step ∗ inl(x) ∗ q(x, ih_{A}), where

q(x, ih_{A}) ∈ ∏_{z′∈A+B} z′ ≺ inl(x) → P (z′) [ x; ih_{A} ] .

By product introduction and + elimination, q(x, ih_{A}) could be λ(when(p_{3}, p_{4})), where

p_{3}(x′) ∈ inl(x′) ≺ inl(x) → P (inl(x′)) [ x; ih_{A}; x′ ∈ A ]

and

p_{4}(y′) ∈ inr(y′) ≺ inl(x) → P (inr(y′)) [ x; ih_{A}; y′ ∈ B ] .

The equations for ≺ give p_{3}(x′) = λls.ih_{A}(x′, ls) and p_{4}(y′) = λls.contr(ls).

Now try to find wf ∗ z ∈ P (z) for z ∈ A + B. By + elimination, wf could be λ(when(p, r)), where p(x) is as above and r(y) ∈ P (inr(y)) for y ∈ B. Reasoning as for p, using w.f. induction on ≺_{B} and then the induction step, gives

r(y) = wfrec_{B}((y, ih_{B})step ∗ inr(y) ∗ s(y, ih_{B}), y) ,

where

[ \begin{matrix}y & ∈ B \\ ih_{B}(y′, ls) & ∈ P (inr(y′)) [y′ ∈ B; ls ∈ y′ ≺_{B} y] \end{matrix} ] s(y, ih_{B}) ∈ ∏_{z′∈A+B} z′ ≺ inl(x) → P (z′) .

Product introduction followed by case analysis on z′, using p again, gives

s(y, ih_{B}) = λ(when((x′)λls.p(x′), (y′)λls.ih_{B}(y′, ls))) .

Summarizing,

s(y, ih_{B}) ∗ inl(x′) ∗ ls = p(x′) ∈ P (inl(x′))
s(y, ih_{B}) ∗ inr(y′) ∗ ls = ih_{B}(y′, ls) ∈ P (inr(y′))
r(y) = step ∗ inr(y) ∗ s(y, (y′, ls)r(y′)) ∈ P (inr(y))
q(x, ih_{A}) ∗ inl(x′) ∗ ls = ih_{A}(x′, ls) ∈ P (inl(x′))
q(x, ih_{A}) ∗ inr(y′) ∗ ls = contr(ls) ∈ P (inr(y′))
p(x) = step ∗ inl(x) ∗ q(x, (x′, ls)p(x′)) ∈ P (inl(x))
wf ∗ inl(x) = p(x) ∈ P (inl(x))
wf ∗ inr(y) = r(y) ∈ P (inr(y)) .

10.2 Recursion

It suffices to show

wf ∗ z = step ∗ z ∗ (λz′ ls.wf ∗ z′) ∈ P (z) .

By + elimination on z, it suffices to show

wf ∗ inl(x) = step ∗ inl(x) ∗ (λz′ ls.wf ∗ z′) ∈ P (inl(x)) ,

and a similar goal for inr(y). Unfolding wf and p and canceling, it is enough to show

q(x, (x′, ls)p(x′)) = λz′ ls.wf ∗ z′ ∈ ∏_{z′∈A+B} z′ ≺ inl(x) → P (z′) .

Product introduction and + elimination on z′, unfolding q, gives two goals. We already know the first, p(x′) = wf ∗ inl(x′); the second has the contradictory assumption inr(y′) ≺ inl(x).

Proving the goal for inr(y) is similar; the final case analysis reduces it to the known equations p(x′) = wf ∗ inl(x′) and r(y′) = wf ∗ inr(y′).

11 Lexicographic product

The lexicographic product of w.f. relations ≺_{A} and ≺_{B} is perhaps the most familiar method of combining w.f. relations. Induction over the product amounts to little more than induction over ≺_{A} followed by induction over ≺_{B}.

This section actually derives w.f. induction for the sum of a family of types ∑_{x∈A} B(x), of which A×B is a special case. Suppose that A is a type with a w.f. relation ≺_{A}. Suppose also that B(x) is a family of types indexed by x ∈ A, with a family of w.f. relations ≺_{B(x)}. Define the lexicographic relation ≺ on the type Σ(A, B) as

⟨x′, y′⟩ ≺ ⟨x, y⟩ ≡ x′ ≺_{A} x + (x′ =_{A} x × y′ ≺_{B(x)} y) .

11.1 Induction

Assume that P (z) is a type for all z ∈ Σ(A, B), and assume the induction step

step ∈ ∏_{z∈Σ(A,B)} ( ∏_{z′∈Σ(A,B)} z′ ≺ z → P (z′)) → P (z).

It suffices to find wf ∗ z ∈ P (z) for z ∈ Σ(A, B). By sum elimination, wf could be λ(split(wf_{1})), where

wf_{1}(x, y) ∈ P (⟨x, y⟩) [ x ∈ A; y ∈ B(x) ] .

By product elimination, wf_{1}(x, y) could be p(x) ∗ y, where

p(x) ∈ ∏_{y∈B(x)} P (⟨x, y⟩) [ x ∈ A ] .

W.f. induction on ≺_{A} gives p(x) = wfrec_{A}(p_{1}, x), where

\begin{aligned}[ & \begin{aligned}x & ∈ A \\ ih_{A}(x′, ls_{A}) & ∈ ∏_{y∈B(x)} P (⟨x′, y⟩) [x′ ∈ A; ls_{A} ∈ x′ ≺ x] \end{aligned} & ] \\ & p_{1}(x, ih_{A}) ∈ ∏_{y∈B(x)} P (⟨x, y⟩) \end{aligned} .

By product introduction, p_{1}(x, ih_{A}) could be λy.q(x, ih_{A}, y), where

q(x, ih_{A}, y) ∈ P (⟨x, y⟩) [ x; ih; y ∈ B(x) ] .

W.f. induction on ≺_{B(x)} gives q(x, ih_{A}, y) = wfrec_{B(x)}(q_{2}, y), where

\begin{aligned}[ & \begin{aligned}x & ∈ A \\ ih_{A}(x′, ls_{A}) & ∈ ∏_{y∈B(x)} P (⟨x′, y⟩) [x′ ∈ A; ls_{A} ∈ x′ ≺ x] \\ y & ∈ B(x) \\ ih_{B}(y′, ls_{B}) & ∈ P (⟨x, y′⟩) [y′ ∈ B(x); ls_{B} ∈ y′ ≺_{B(x)} y] \end{aligned} & ] \\ & q_{2}(y, ih_{B}) ∈ P (⟨x, y⟩) \end{aligned} .

By the induction step, q_{2}(y, ih_{B}) could be step ∗ ⟨x, y⟩ ∗ r(x, ih_{A}, y, ih_{B}), where

r(x, ih_{A}, y, ih_{B}) ∈ ∏_{z′∈Σ(A,B)} z′ ≺ ⟨x, y⟩ → P (z′) [ x; ih_{A}; y; ih_{B} ] .

By product introduction and sum elimination on z′, unfolding ≺, r(x, ih_{A}, y, ih_{B}) could be λ(split((x′, y′)λ(t))), where

t ∈ P (⟨x′, y′⟩) [ \begin{matrix}x; ih_{A}; y; ih_{B} \\ x′ & ∈ A \\ y′ & ∈ B(x′) \\ ls & ∈ x′ ≺_{A} x + (x′ =_{A} x × y′ ≺_{B(x)} y) \end{matrix} ] .

By + elimination on ls, t could be when(t_{A}, split(t_{B}), ls), where (suppressing the assumptions x, ih_{A}, …, y′)

t_{A}(ls_{A}) ∈ P (⟨x′, y′⟩) [ ls_{A} ∈ x′ ≺_{A} x ]

and

t_{B}(e, ls_{B}) ∈ P (⟨x′, y′⟩) [ e ∈ x′ =_{A} x; ls_{B} ∈ y′ ≺_{B(x)} y ]

Clearly t_{A}(ls_{A}) = ih_{A}(x′, ls_{A}) ∗ y′. For the second goal, replacing x′ by x gives t_{B}(e, ls_{B}) = ih_{B}(y′, ls_{B}).

Define p′ ≡ (x′, ls)p(x′). This simplifies the equation about p in the summary:

r(x, ih_{A}, y, ih_{B}) ∗ ⟨x′, y′⟩ ∗ inl(ls_{A}) = ih_{A}(x′, ls_{A}) ∗ y′ ∈ P (⟨x′, y′⟩)
r(x, ih_{A}, y, ih_{B}) ∗ ⟨x′, y′⟩ ∗ inr(e, ls_{B}) = ih_{B}(y′, ls_{B}) ∈ P (⟨x′, y′⟩)
q(x, ih_{A}, y) = step ∗ ⟨x, y⟩ ∗ r(x, ih_{A}, y, (y′, ls)q(x, ih_{A}, y′)) ∈ P (⟨x, y⟩)
p(x) ∗ y = q(x, p′, y) ∈ P (⟨x, y⟩)
wf ∗ ⟨x, y⟩ = p(x) ∗ y ∈ P (⟨x, y⟩)

11.2 Recursion

For the recursion rule of ≺ on Σ(A, B), it suffices to show

wf ∗ z = step ∗ z ∗ (λz′ ls.wf ∗ z′) ∈ P (z) [ z ∈ Σ(A, B) ] .

By sum elimination on z, it suffices to show

p(x) ∗ y = step ∗ ⟨x, y⟩ ∗ (λz′ ls.wf ∗ z′) ∈ P (⟨x, y⟩) [ x ∈ A; y ∈ B(x) ] .

Unfolding p, it is enough to show

q(x, p′, y) = step ∗ ⟨x, y⟩ ∗ (λz′ ls.wf ∗ z′) ∈ P (⟨x, y⟩) [ x ∈ A; y ∈ B(x) ] .

Unfolding q and canceling on both sides, it is enough to show

\begin{matrix}[ & x ∈ A; y ∈ B(x) & ] \\ r(x, p′, y, (y′, ls)q(x, p′, y′)) = λz′ ls.wf ∗ z′ ∈ ∏_{z′∈Σ(A,B)} z′ ≺ ⟨x, y⟩ → P (z′) \end{matrix}

By product introduction and sum elimination on z′, it is enough to show

\begin{matrix}[ & x; y; x′ ∈ A; y′ ∈ B(x′); ls ∈ ⟨x′, y′⟩ ≺ ⟨x, y⟩ & ] \\ r(x, p′, y, (y′, ls)q(x, p′, y′)) ∗ ⟨x′, y′⟩ ∗ ls = wf ∗ ⟨x′, y′⟩ ∈ P (⟨x′, y′⟩) \end{matrix} .

By case analysis on ⟨x′, y′⟩ ≺ ⟨x, y⟩, unfolding r, it remains to show

p(x′) ∗ y′ = wf ∗ ⟨x′, y′⟩ ,

which is the equation for wf, and

q(x, p′, y′) = wf ∗ ⟨x′, y′⟩ ,

which follows from the equations for wf and p.

12 Lexicographic exponentiation

Suppose that ≺_{A} is a w.f. relation on A. The alphabetic ordering of words in a dictionary can be formalized as the lexicographic relation on lists [x_{1}, …, x_{n}], where x_{1}, …, x_{n} ∈ A. Define the relation ≺^{)} to satisfy [x_{1}, …, x_{m}] ≺^{)} [a_{1}, …, a_{n}] whenever there is some k such that x_{i} = a_{i} for i ≤ k, and either k = m < n or x_{k+1} ≺_{A} a_{k+1}. Note that ≺^{)} is not necessarily w.f. — there is a descending chain [1], [0, 1], [0, 0, 1], . . ..

To rule out such chains we must allow only lists whose elements appear in decreasing order. The w.f. relation ≺ is simply ≺^{)} restricted to the set

{[x_{1}, …, x_{n}] | x_{1} ≻_{A} ⋯ ≻_{A} x_{n}} ,

formalized as a sum type of the form ∑_{l∈List(A)} D(l). I call this the power type of A, or Pow(A). Its elements correspond to finite subsets of A whenever ≺_{A} is a total ordering; furthermore, if ≺_{A} has order type α, then ≺ has order type 2^{α}.

12.1 Definition of power types

The derivation of induction for Pow(A) is the most complex in this paper. We begin with basic concepts of lists:

[x_{1}, …, x_{n}]  abbreviates  cons(x_{1}, ⋯ cons(x_{n}, nil) ⋯) .

The operations of append (⊕) and reverse (rev) satisfy by definition

nil ⊕ l = l
cons(x, l_{1}) ⊕ l = cons(x, l_{1} ⊕ l)
rev ∗ nil = nil
rev ∗ cons(x, l) = (rev ∗ l) ⊕ [x] .

The relation ≺^{)} is defined such that

l′ ≺^{)} nil = ⊥
nil ≺^{)} cons(x, l) = ⊤
cons(x′, l′) ≺^{)} cons(x, l) = x′ ≺_{A} x + (x′ =_{A} x × l′ ≺^{)} l) .

We have the familiar facts

l ⊕ nil = l
(l_{1} ⊕ l_{2}) ⊕ l_{3} = l_{1} ⊕ (l_{2} ⊕ l_{3})
rev ∗ (rev ∗ l) = l

The constructions apls and lsap assert facts about ≺^{)}, proved by induction on the lists l and l′:

apls(l′, l′′, l) ∈ l′ ⊕ l′′ ≺^{)} l → l′ ≺^{)} l
lsap(l′, l, l_{2}) ∈ l′ ≺^{)} l ⊕ l_{2} → l′ ≺^{)} l + ∑_{l_{1}∈List(A)}(l′ = l ⊕ l_{1} × l_{1} ≺^{)} l_{2})

Normally we build lists by adding elements to the front, using cons. Here we also must consider adding elements to the rear. Define

rlistrec(c_{0}, c_{1}, l) ≡ listrec(c_{0}, (x, l, u)c_{1}(rev ∗ l, x, u), rev ∗ l) ;

it is easy to verify the rule of reverse list induction:

\frac{l ∈ List(A) c_{0} ∈ C(nil) \begin{matrix}[l ∈ List(A); x ∈ A; u ∈ C(l)] \\ c_{1}(l, x, u) ∈ C(l ⊕ [x]) \end{matrix}}{rlistrec(c_{0}, c_{1}, l) ∈ C(l)}

Functions defined by reverse list recursion obey the computation rules

rlistrec(c_{0}, c_{1}, nil) = c_{0} ∈ C(nil)
rlistrec(c_{0}, c_{1}, l ⊕ [x]) = c_{1}(l, x, rlistrec(c_{0}, c_{1}, l)) ∈ C(l ⊕ [x]) .

The predicate D(l), defined using rlistrec, expresses that the elements of the list l appear in descending order:

\begin{matrix}D(nil) = & ⊤ \\ D([x]) = & ⊤ \\ D(l ⊕ [x] ⊕ [x′]) = & x′ ≺_{A} x × D(l ⊕ [x]) \end{matrix}

Evidently D(l ⊕ [x]) implies D(l); reverse list induction on l gives

descap(l_{1}, l) ∈ D(l_{1} ⊕ l) → D(l_{1}) × D(l)
endls(l, y, x) ∈ D(l ⊕ [y]) × l ⊕ [y] ≺^{)} [x] → y ≺_{A}^{+} x .

Recall that ≺_{A}^{+} denotes the transitive closure of ≺_{A}.

Define the power type of A as

Pow(A) ≡ ∑_{l∈List(A)} D(l) .

The w.f. relation ≺ compares the underlying lists using ≺^{)}:

⟨l′, d′⟩ ≺ ⟨l, d⟩ = l′ ≺^{)} l

12.2 Induction

Assume that P (z) is a type for z ∈ Pow(A); define

Q(z) ≡ ∏_{z′∈Pow(A)} z′ ≺ z → P (z′) ;

assume the induction step

step ∈ ∏_{z∈Pow(A)} Q(z) → P (z) .

It suffices to find wf ∗ z ∈ P (z) for z ∈ Pow(A). By the induction step, wf could be λz.step ∗ z ∗ wf_{1}, where wf_{1} ∈ Q(z). By sum elimination on z, wf_{1} could be split(wf_{2}, z), where

wf_{2}(l, d) ∈ Q(⟨l, d⟩) [ l ∈ List(A); d ∈ D(l) ] .

By product elimination, wf_{2}(l, d) could be p(l) ∗ d, where

p(l) ∈ ∏_{d∈D(l)} Q(⟨l, d⟩) .

By reverse list induction, p(l) could be rlistrec(p_{0}, p_{1}, l), where

p_{0} ∈ ∏_{d∈D(nil)} Q(⟨nil, d⟩) ,

and

p_{1}(l, x, u) ∈ ∏_{d∈D(l⊕[x])} Q(⟨l ⊕ [x], d⟩) [ \begin{matrix}l & ∈ List(A) \\ x & ∈ A \\ u & ∈ ∏_{d∈D(l)} Q(⟨l, d⟩) \end{matrix} ] .

In the nil goal, unfolding Q gives the contradictory assumption z′ ≺ ⟨nil, d⟩; thus p_{0} is λd z′ ls.contr(ls). By product elimination, p_{1}(l, x, u) could be q(x) ∗ l ∗ u, where

q(x) ∈ ∏_{l∈List(A)} ( ∏_{d∈D(l)} Q(⟨l, d⟩) → ∏_{d∈D(l⊕[x])} Q(⟨l ⊕ [x], d⟩)) [ x ∈ A ] .

Now use w.f. induction over the transitive closure of ≺_{A}. Iterating the induction hypothesis proves Q for a descending list of any length, provided its elements are all smaller than x. This key step is discussed at length below. Write the recursion operator as wfrec_{A}^{+} . Then q(x) could be wfrec_{A}^{+}(q_{1}, x), where

[ \begin{matrix}x & ∈ A \\ ih(x′, ls) & ∈ ∏_{l∈List(A)} (∏_{d∈D(l)} Q(⟨l, d⟩) → ∏_{d∈D(l⊕[x′])} Q(⟨l ⊕ [x′], d⟩)) \\ & [x′ ∈ A; ls ∈ x′ ≺_{A}^{+} x] \end{matrix} ] q_{1}(x, ih) ∈ ∏_{l∈List(A)} ( ∏_{d∈D(l)} Q(⟨l, d⟩) → ∏_{d∈D(l⊕[x])} Q(⟨l ⊕ [x], d⟩)) .

By product introduction and sum elimination on z′, unfolding Q and ≺, gives

q_{1}(x, ih) = λl u d.λ(split((l′, d′)λlx.r(ih, l, u, d, x, l′, d′, lx))) ,

where

r(ih, l, u, d, x, l′, d′, lx) ∈ P (⟨l′, d′⟩) [ \begin{matrix}x; ih; l ∈ List(A) \\ u & ∈ ∏_{d∈D(l)} Q(⟨l, d⟩) \\ d & ∈ D(l ⊕ [x]) \\ l′ & ∈ List(A) \\ d′ & ∈ D(l′) \\ lx & ∈ l′ ≺^{)} l ⊕ [x] \end{matrix} ] .

Using lsap, case analysis on l′ ≺^{)} l ⊕ [x] gives

r(ih, l, u, d, x, l′, d′, lx) = when(r_{1}, split((l_{1}) split((e, lx)r_{2})), lsap(l′, l, [x], lx))

where

r_{1}(lx) ∈ P (⟨l′, d′⟩) [ x; ih; l; u; d; l′; d′; lx ∈ l′ ≺^{)} l ]

and, substituting with l′ = l ⊕ l_{1},

r_{2} ∈ P (⟨l ⊕ l_{1}, d′⟩) [ x; ih; l; u; d; l_{1} ∈ List(A); d′ ∈ D(l ⊕ l_{1}); lx ∈ l_{1} ≺^{)} [x] ] .

Since u gives Q(⟨l, d⟩) for any d ∈ D(l), the first goal holds with

r_{1}(lx) = u ∗ fst(descap(l, [x], d)) ∗ ⟨l′, d′⟩ ∗ lx .

(To be absolutely formal I should write descap(l, [x]) ∗ d, but descap(l, [x], d) is simpler and clearer. Likewise for lsap, apls, endls.)

In the second goal, the induction step gives r_{2} as step ∗ ⟨l ⊕ l_{1}, d′⟩ ∗ r_{3}, where

r_{3} ∈ Q(⟨l ⊕ l_{1}, d′⟩) [ x; ih; l; u; d; l_{1}; d′; lx ] .

Product elimination gives r_{3} as s(ih, l, u, d, x, l_{1}) ∗ lx ∗ d′, where

s(ih, l, u, d, x, l_{1}) ∈ l_{1} ≺^{)} [x] → ∏_{d′∈D(l⊕l_{1})} Q(⟨l ⊕ l_{1}, d′⟩) [ x; ih; l; u; d; l_{1} ] .

Reverse list induction shows that the elements of l_{1} are all smaller than x. Take s(ih, l, u, d, x, l_{1}) as rlistrec(s_{0}, s_{1}, l_{1}), where

s_{0} ∈ nil ≺^{)} [x] → ∏_{d′∈D(l⊕nil)} Q(⟨l ⊕ nil, d′⟩) [ x; ih; l; u; d ]

and

\begin{matrix}[ & \begin{matrix}x; ih; l; u; d; l_{1} ∈ List(A); y ∈ A \\ v ∈ l_{1} ≺^{)} [x] → ∏_{d′∈D(l⊕l_{1})} Q(⟨l ⊕ l_{1}, d′⟩) \end{matrix} & ] \\ s_{1}(l, y, v) ∈ l_{1} ⊕ [y] ≺^{)} [x] → ∏_{d′∈D(l⊕l_{1}⊕[y])} Q(⟨l ⊕ l_{1} ⊕ [y], d′⟩) \end{matrix} .

The first goal holds because l⊕nil = l and the assumption u gives Q(⟨l, d⟩); take s_{0} = λlx.u.

The second goal holds because the w.f. induction hypothesis allows us to append y to the list l ⊕ l_{1}, preserving the truth of Q. The construction is complex; let us consider it in pieces. Under the assumptions x, ih, …, v, recalling that ⊕ is associative, note the facts

descap(l_{1}, [y], d′) ∈ D(l) × D(l_{1} ⊕ [y])) [ d′ ∈ D(l ⊕ (l_{1} ⊕ [y])) ]

endls(l, y, x, d_{1}, lx) ∈ y ≺_{A}^{+} x [ \begin{matrix}d_{1} & ∈ D(l_{1} ⊕ [y]) \\ lx & ∈ l_{1} ⊕ [y] ≺^{)} [x] \end{matrix} ]

apls(l_{1}, [y], [x], lx) ∈ l_{1} ≺^{)} [x] [ lx ∈ l_{1} ⊕ [y] ≺^{)} [x] ]

ih(y, ls) ∗ (l ⊕ l_{1}) ∗ (v ∗ lx_{1}) ∗ d′ ∈ Q(⟨l ⊕ l_{1} ⊕ [y], d′⟩) [ \begin{matrix}ls & ∈ y ≺_{A}^{+} x \\ lx_{1} & ∈ l_{1} ≺^{)} [x] \\ d′ & ∈ D((l ⊕ l_{1}) ⊕ [y]) \end{matrix} ]

The construction using endls to assert y ≺_{A}^{+} x from l_{1} ⊕ [y] ≺^{)} [x] and D(l_{1} ⊕ [y]) is the sole essential appeal to the descending property D. These constructions combine to solve the second goal:

s_{1}(l_{1}, y, v) = λlx d′.ih(y, endls(l, y, x, snd(descap(l_{1}, [y], d′)), lx))
∗ (l ⊕ l_{1}) ∗ (v ∗ apls(l_{1}, [y], [x], lx)) ∗ d′

Define q′ ≡ (x′, ls)q(x′). Summarizing,

s(ih, l, u, d, x, nil) ∗ lx = u ∈ ∏_{d∈D(l)} Q(⟨l, d⟩)
s(ih, l, u, d, x, l_{1} ⊕ [y]) ∗ lx ∗ d′ = ih(y, endls(l, y, x, snd(descap(l_{1}, [y], d′)), lx)) ∗
(l ⊕ l_{1}) ∗ (s(ih, l, u, d, x, l_{1}) ∗ apls(l_{1}, [y], [x], lx)) ∗ d′
∈ Q(⟨l ⊕ l_{1} ⊕ [y], d′⟩)

q(x) ∗ l ∗ u ∗ d ∗ ⟨l′, d′⟩ ∗ lx_{0} = \{ \begin{matrix}u ∗ fst(descap(l, [x], d)) ∗ ⟨l′, d′⟩ ∗ lx ∈ P (⟨l′, d′⟩) \\ if lsap(l′, l, [x], lx_{0}) = inl(lx) [lx ∈ l′ ≺^{)} l] \\ step ∗ ⟨l ⊕ l_{1}, d′⟩ ∗ (s(q′, l, u, d, x, l_{1}) ∗ lx ∗ d′) \\ if lsap(l′, l, [x], lx_{0}) = inr(⟨l_{1}, ⟨e, lx⟩⟩) \\ [l′ = l ⊕ l_{1}; lx ∈ l_{1} ≺^{)} [x]] \end{matrix}

p(nil) ∗ d ∗ z′ ∗ ls = contr(ls) ∈ P (z′)
p(l ⊕ [x]) = q(x) ∗ l ∗ p(l) ∈ ∏_{d∈D(l⊕[x])} Q(⟨l ⊕ [x], d⟩)
wf ∗ ⟨l, d⟩ = step ∗ ⟨l, d⟩ ∗ (p(l) ∗ d) ∈ P (⟨l, d⟩)

The equation for q(x) uses the recursion rule of wfrec_{A}^{+}.

12.3 Intermezzo

This derivation is related to work in the theory of ordinal recursion. Let α be any ordinal less than ϵ_{0}. Terlouw derives recursion on 2^{α}, using recursion on α to define a functional of a higher type level [27]. To examine the connection with the present derivation of induction over ≺ on Pow(A) from induction over ≺_{A}, our first problem is reconciling the notations. Let ≺ (also) denote a wellordering of order type 2^{α}, and ≺_{A} a wellordering of order type α, and [F]_{≺z} the restriction of the function F to arguments below z. Let the function F_{0}(z) defined by the transfinite recursion F_{0}(z) = G([F_{0}]_{≺z}, z). Terlouw expresses F_{0} using a functional H defined in terms of G by transfinite recursion on ≺_{A}.

Below x, y, z range over ordinals, while + denotes ordinal addition, and < ordinal comparison. Transfinite induction on the proposition P (x) requires that P be progressive. The property Prog(P) is essentially a w.f. induction step: Prog(P) ≡ ∀x. ((∀y < x. P (y)) → P (x)). Terlouw remarks: To prove P (x) for all x up to ϵ_{0}, let α be arbitrary and prove ∀x < 2^{α}. P (x) using only transfinite induction up to α. This follows by proving ∀x < α. B(x), where

B(x) ≡ ∀z. ((∀y < z. P (y)) → ∀y < z + 2^{x}. P (y)) .

Induction is sound because Prog(P) implies Prog(B).

Up to ϵ_{0} there is a one-to-one correspondence between ordinals and descending lists of ordinals 2^{α_{0}} + ⋯ + 2^{α_{n}}, where α_{0} > ⋯ > α_{n}. So we can regard any ordinal z uniquely as a list [α_{0}, …, α_{n}], and if x < α_{n}, adding 2^{x} to z corresponds to putting x on the end of the list. Thus B(x) is essentially the type of the construction q(x) above. Induction up to the ordinal α proves B(x); w.f. recursion over ≺_{A}^{+} establishes q(x).

Terlouw does not incant “propositions as types,” but remarks (page 398) that the relationship between the functionals H and G “is nothing other than the functionalanalogy” of the relationship between B and P. In H, the variables x and z are those of B, while F denotes a function defined below z, of “type” ∀y < z. P (y). The construction q(x) ∗ l ∗ u corresponds to H(x, z, F), for u is a function asserting P everywhere below l. To clarify the correspondence between H and q, define the Type Theory function h(x, z, F) such that h(x, ⟨l, d⟩ , F) ≡ q ∗ l ∗ F ∗ d. Take the type A to be the natural numbers, and take x = 0. Suppressing constructions of type z′ ≺ z, unfold the equations for q and s in the previous subsection. The second equation for q has l_{1} ≺^{)} [0], which is only possible if l_{1} = nil and l′ = l. This gives

h(0, z, F) ∗ z′ = \{ \begin{matrix}F ∗ (⋯) ∗ z′ if & z′ ≺ z \\ λlx.step ∗ z′ ∗ (F ∗ ⋯) if & z′ = z . \end{matrix}

Terlouw defines H to satisfy

H(0, z, F)(z′) = \{ \begin{matrix}F (z′) if & z′ ≺ z \\ G([F]_{≺z′}, z′) if & z′ = z . \end{matrix}

Noting that [F]_{≺z} corresponds to some construction F′ of type Q(z), and that G([F]_{≺z}, z) corresponds to step ∗ z ∗ F′, the two sets of equations are nearly identical. Unfortunately, I cannot carry the correspondence between H and q any further. The rest of the definition of H is more complicated, involving functions for computing ordinal operations in terms of an embedding in the natural numbers. Apparently H builds up its result in a different manner from q.

12.4 Recursion

The desired property is

wf ∗ z = step ∗ z ∗ (λz′ ls.wf ∗ z′) ∈ P (z) [ z ∈ A ] .

Unfolding wf and canceling, it suffices to prove

p(l) ∗ d = λz′ ls.wf ∗ z′ ∈ Q(⟨l, d⟩) [ l ∈ List(A); d ∈ D(l) ] .

By product elimination, it suffices to show

∏_{d∈D(l)} ∏_{z′∈Pow(A)} ∏_{ls∈z′≺⟨l,d⟩} p(l) ∗ d ∗ z′ ∗ ls =_{P (z′)} wf ∗ z′ true [ l ∈ List(A) ] .

By reverse list induction on l, followed by product introduction, it is enough to show

contr(ls) = wf ∗ z′ ∈ P (z′) [ d; z′; ls ∈ z′ ≺ ⟨nil, d⟩ ]

(which holds by contradiction), and also

[ \begin{matrix}l & ∈ List(A); x ∈ A \\ u & ∈ ∏_{d∈D(l)} ∏_{z′∈Pow(A)} ∏_{ls∈z′≺⟨l,d⟩} p(l) ∗ d ∗ z′ ∗ ls =_{P (z′)} wf ∗ z′ \\ d & ∈ D(l ⊕ [x]); z′ ∈ Pow(A); ls ∈ z′ ≺ ⟨l ⊕ [x], d⟩ \end{matrix} ] q(x) ∗ l ∗ p(l) ∗ d ∗ z′ ∗ ls = wf ∗ z′ ∈ P (z′) .

By sum elimination on z′, unfolding ≺, it suffices to show

\begin{matrix}[ & l; x; u; d; l′ ∈ List(A); d′ ∈ D(l′); lx ∈ l′ ≺^{)} l ⊕ [x] & ] \\ q(x) ∗ l ∗ p(l) ∗ d ∗ ⟨l′, d′⟩ ∗ lx = wf ∗ ⟨l′, d′⟩ ∈ P (⟨l′, d′⟩) \end{matrix} .

By case analysis with lsap on l′ ≺^{)} l ⊕ [x], unfolding q, it suffices to show

[ l; x; u; d; l′; d′; lx ∈ l′ ≺^{)} l ]
p(l) ∗ fst(descap(l, [x], d)) ∗ ⟨l′, d′⟩ ∗ lx = wf ∗ ⟨l′, d′⟩ ∈ P (⟨l′, d′⟩)

(which holds by the induction hypothesis), and also

[ l; x; u; d; l_{1} ∈ List(A); d′ ∈ D(l ⊕ l_{1}); lx ∈ l_{1} ≺^{)} [x] ] step ∗ ⟨l ⊕ l_{1}, d′⟩ ∗ (s(q′, l, p(l), d, x, l_{1}) ∗ lx ∗ d′) = wf ∗ ⟨l ⊕ l_{1}, d′⟩ ∈ P (⟨l ⊕ l_{1}, d′⟩) .

By canceling and product elimination, it suffices to show

\begin{matrix}[ & l; x; u; d; l_{1} & ] \\ ∏_{lx∈l_{1}≺^{)}[x]} ∏_{d′∈D(l⊕l_{1})} s(q′, l, p(l), d, x, l_{1}) ∗ lx ∗ d′ =_{Q(⟨l⊕l_{1},d′⟩)} p(l ⊕ l_{1}) ∗ d′ true \end{matrix} .

Use reverse list induction on l_{1}, then product introduction, and then unfold s. It suffices to show p(l) = p(l ⊕ nil), which is trivial, and also

[ \begin{matrix}& l; x; u; d; l_{1} ∈ List(A); y ∈ A \\ v & ∈ ∏_{lx∈l_{1}≺^{)}[x]} ∏_{d′∈D(l⊕l_{1})} s(q′, l, p(l), d, x, l_{1}) ∗ lx ∗ d′ =_{Q(⟨l⊕l_{1},d′⟩)} p(l ⊕ l_{1}) ∗ d′ \\ lx & ∈ l_{1} ⊕ [y] ≺^{)} [x]; d′ ∈ D(l ⊕ l_{1} ⊕ [y]) \end{matrix} ]
q(y) ∗ (l ⊕ l_{1}) ∗ (s(q′, l, p(l), d, x, l_{1}) ∗ apls(l_{1}, [y], [x], lx)) ∗ d′
= p(l ⊕ l_{1} ⊕ [y]) ∗ d′ ∈ Q(⟨l ⊕ l_{1} ⊕ [y], d′⟩)

Unfolding p and canceling, it remains to show

s(q′, l, p(l), d, x, l_{1}) ∗ apls(l_{1}, [y], [x], lx) = p(l ⊕ l_{1}) ∈ ∏_{d′∈D(l⊕l_{1})} Q(⟨l ⊕ l_{1}, d′⟩) ,

which follows by product introduction and the induction hypothesis.

13 Wellordering types

If A is a type, and B(x) is a type for each x ∈ A, then there is a type W_{x∈A} B(x), equivalently W(A, B). Each value of this wellordering type is a tree such that each node is labeled with some element a of A, and has a branch for each element b in B(a). A tree has the form sup(a, f), where f(y) ∈ W_{x∈A} B(x) for y ∈ B(a). In this notation, a labels the node, while f(b) follows the branch for b to a subtree having the same wellordering type.

The natural numbers belong to a simple wellordering type. There are two kinds of node:

• those with no branches represent 0;

• those with one branch represent successor numbers.

A possible definition is Nat = W(Bool, cond(⊥, ⊤)) .

Lists are a similar wellordering type: the second kind of node contains a member of the list, while the branch points to the rest of the list. Wellordering types can also have infinite branching, as in the second number class of ordinals [15, page 82]. (Note: the w.f. relation defined below is not < on the second number class.)

There is a close connection between wellordering types and well-founded relations, as the terminology suggests. Every wellordering type W is w.f. under the relation ≺_{W}, where w′ ≺_{W} w whenever w′ is an immediate subtree of w. Formally (by transfinite induction), it is easy to define ≺_{W} such that

w′ ≺_{W} sup(a, f) = {y ∈ B(a) | w′ =_{W} f(y)} .

Since the natural numbers can be defined as the wellordering type N, with < as the transitive closure of ≺_{N}, w.f. induction for < follows from that of wellordering types. I include the separate proof for < because it is a simple introduction to w.f. relations. There is an apparent circularity: the proof for transitive closure involves Nat elimination, the rule for induction over the natural numbers. But this is merely to argue by cases, a number is either 0 or is succ(n). It does not require w.f. induction for <.

13.1 Induction

Assume that P (w) is a type for w ∈ W(A, B), and assume the induction step

step ∈ ∏_{w∈W(A,B)} ( ∏_{w′∈W(A,B)} w′ ≺ w → P (w′)) → P (w).

To justify w.f. induction, it suffices to find wf ∗ w ∈ P (w) for w ∈ W(A, B). By transfinite induction, wf could be λw. transrec(p, w), where

p(a, f, u) ∈ P (sup(a, f)) [ \begin{matrix}a ∈ & A \\ f(y) ∈ & W(A, B) & [y ∈ B(a)] \\ u(y) ∈ & P (f(y)) & [y ∈ B(a)] \end{matrix} ]

Using the induction step, p(a, f, u) could be step ∗ sup(a, f) ∗ p_{1}, where

p_{1} ∈ ∏_{w′∈W(A,B)} w′ ≺ sup(a, f) → P (w′) [ a; f; u ] .

Unfolding ≺, product introduction gives p_{1} = λw′ ls.p_{2}(ls), where

p_{2}(ls) ∈ P (w′) [ a; f; u; w′ ∈ W(A, B); ls ∈ {y ∈ B(a) | w′ = f(y)} ] .

Using subset elimination and replacing w′ by f(y), the goal becomes

p_{2}(y) ∈ P (f(y)) [ a; f; u; w′ ∈ W(A, B); y ∈ B(a) ] .

Appealing to the induction hypothesis, p_{2}(y) is u(y).

Summarizing,

wf ∗ sup(a, f) = step ∗ sup(a, f) ∗ (λw′ ls.wf ∗ f(ls)) ∈ P (sup(a, f)) .

13.2 Recursion

The desired property is

wf ∗ w = step ∗ w ∗ (λw′ ls.wf ∗ w′) ∈ P (w) .

By W-elimination, w must have the form sup(a, f), in

[ \begin{matrix}a & ∈ A \\ f(y) & ∈ W(A, B) [y ∈ B(a)] \end{matrix} ] wf ∗ sup(a, f) = step ∗ sup(a, f) ∗ (λw′ ls.wf ∗ w′) ∈ P (sup(a, f)) .

Unfolding the left side, canceling, and unfolding ≺, it remains to show

wf ∗ f(ls) = wf ∗ w′ ∈ P (w′) [ \begin{matrix}a; f \\ w′ & ∈ W(A, B) \\ ls & ∈ \{y ∈ B(a) | w′ = f(y)\} \end{matrix} ] .

By subset elimination, it remains to show

wf ∗ f(y) = wf ∗ w′ ∈ P (w′) [ a; f; w′; y ∈ B(a); w′ = f(y) true ] .

This holds because w′ equals f(y).

14 A characterization of well-founded relations

Classically, a relation ≺ on a set A is w.f. whenever there are no infinite descending chains a_{0} ≻ a_{1} ≻ a_{2} · · ·. Another classical characterization is that every nonempty subset of A contains a minimal element [13]. I know of no constructive derivation of w.f. induction from either of these characterizations. However, there is a constructive characterization: Theorem. A relation ≺_{A} on a type A is w.f. if and only if there is some wellordering type W, and rank function wof ∈ A → W, such that ≺_{A} is logically equivalent to the inverse image of ≺_{W}. Proof. The if part is immediate, because every wellordering type is w.f., and taking an inverse image preserves this property. To show the converse requires constructing a wellordering type and rank function whose inverse image is ≺_{A}. Each node of the wellordering type is labeled by an element of A and has one branch for every predecessor a′ of a: define

W ≡ W_{a∈A} (∑_{x∈A} x ≺_{A} a) .

The rank function wof is defined by w.f. recursion, such that wof ∗ a is a tree rooted in a and with branches to subtrees wof ∗ a′ for every predecessor a′. There is a branch for each pair ⟨a′, ls⟩ where a′ ∈ A and ls ∈ a′ ≺_{A} a, so the definition involves split:

s(a, ih) ≡ sup(a, split(ih))
wof ≡ λ(wfrec(s)) .

Unfolding wof using the recursion rule gives

wof ∗ a = wfrec(s, a)
= s(a, (x, ls) wfrec(s, x))
= s(a, (x, ls)wof ∗ x)
= sup(a, split((x, ls)wof ∗ x)) .

By a trivial transfinite recursion, the function aof ∈ W → A maps any element sup(a, f) to a: put aof ≡ λ(transrec((a, f, e)a). Then wof is one-to-one, since aof ∗ (wof ∗ a) = a for all a. Also

wof ∗ a′ ≺_{W} wof ∗ a = wof ∗ a′ ≺_{W} sup(a, split((x, ls)wof ∗ x))
= {y ∈ ∑_{x∈A} x ≺_{A} a | wof ∗ a′ =_{W} split((x, ls)wof ∗ x, y)}

To show that ≺_{A} is logically equivalent to the inverse image under wof of ≺_{W}, it suffices to show

a′ ≺_{A} a ↔ wof ∗ a′ ≺_{W} wof ∗ a true [ a ∈ A; a′ ∈ A ] .

For the → direction, it is enough to show

{y ∈ ∑_{x∈A} x ≺_{A} a | wof ∗ a′ =_{W} split((x, ls)wof ∗ x, y)} true [ ls ∈ a′ ≺_{A} a ]

which is immediate, putting ⟨a′, ls⟩ for y.

For the ← direction, by product introduction, subset elimination, and sum elimination, it is enough to show

a′ ≺_{A} a true [ \begin{matrix}x & ∈ A \\ ls & ∈ x ≺_{A} a \\ e & ∈ wof ∗ a′ =_{W} wof ∗ x \end{matrix} ] .

Since wof is one-to-one, a′ = x.

The wellordering types generalize the notion of ordinal. The theorem generalizes the notion of order type: each w.f. relation has a normal form, the inverse image of a wellordering type. This characterization of w.f. relations seems less natural than the classical ones.

15 Well-founded relations in the literature

People have proved program termination using a variety of w.f. relations, most of which are easily constructed in this Type Theory framework. The lexicographic product of w.f. relations appears often, but sometimes in disguise. In deriving a unification algorithm, Manna and Waldinger [12] define the “unification ordering” ≺_{un} on pairs of expressions. Let vars(x) denote the (finite) set of variables in an expression, and ≺ the (w.f.) substructure relation on expressions. Manna and Waldinger define ⟨x′, y′⟩ ≺_{un} ⟨x, y⟩ to hold whenever

vars(x′) ∪ vars(y′) ⊂ vars(x) ∪ vars(y) or

vars(x′) ∪ vars(y′) = vars(x) ∪ vars(y)  and  x′ ≺ x .

The proper subset relation is w.f. on finite sets: if |a| denotes the cardinality of a, then a ⊂ b implies |a| < |b|. So ≺_{un} is also w.f.: it is a subrelation of the inverse image of a lexicographic product, mapping each ⟨x, y⟩ to the lexicographically ordered pair ⟨|vars(x) ∪ vars(y)|, x⟩.

Generalizing the lexicographic product from A × B to the sum ∑_{x∈A} B(x) produces many more w.f. relations. The second number class is the set of all countable ordinals, and is the smallest class of ordinals containing 0 and closed under successor and countable limits [4]. These three principles underlie standard systems of ordinal notations such as Kleene’s O [23]. In Type Theory, take ⊥ for 0, and A + ⊤ for successor, and ∑_{n∈Nat} A(n) for limit. Then any notation for a constructive ordinal can be translated into a w.f. relation of the same order type.

A concrete application of lexicographic product for both Σ and × is the stepped lexicographic ordering [7, page 474] on n-tuples of A:

A^{ω} ≡ ∑_{n∈Nat} A^{n}  where  \begin{matrix}A^{0}  = & ⊤ \\ A^{succ(n)} = & A × A^{n} \end{matrix}

The empty relation on the type ⊤ is trivially w.f., so the relation ≺_{A^{n}} on the finite power A^{n} is w.f. by induction on n. Each element of A^{ω} is an n-tuple, represented in the form ⟨n, ⟨x_{1}, …, ⟨x_{n}, 0⟩⟩⟩. Under the w.f. relation on A^{ω}, shorter tuples preceed longer ones and tuples of equal length are compared lexicographically.

Now consider lexicographic exponentiation of the relation ≺_{A}. Recall that elements of the power type Pow(A) are lists [x_{1}, …, x_{n}] with elements in descending order x_{1} ≻_{A} ⋯ ≻_{A} x_{n}. The w.f. relation on power types differs from that on A^{ω}, for [1, 0] ≺ [2] even though [1, 0] is the longer list.

A two-argument form of exponentiation is sometimes seen [26]. Suppose B is a type with w.f. relation ≺_{B}. An element of the type B^{A} is a list of pairs from A × B, descending under ≺_{A}:

\{ [⟨x_{1}, y_{1}⟩ , …, ⟨x_{n}, y_{n}⟩] | x_{1} ≻_{A} ⋯ ≻_{A} x_{n}\} \begin{matrix}x_{1}, …, x_{n} ∈ A \\ y_{1}, …, y_{n} ∈ B \end{matrix}

This list represents a finite function from A to B. The w.f. relation on lists is that for Pow(A × B), comparing each pair ⟨x_{i}, y_{i}⟩ under the relation for A × B. Clearly x_{1} ≻_{A} ⋯ ≻_{A} x_{n} implies ⟨x_{1}, y_{1}⟩ ≻_{A×B} ⋯ ≻_{A×B} ⟨x_{n}, y_{n}⟩; formalizing this implication as a Type Theory function defines the w.f. relation for B^{A} as an inverse image of that for Pow(A × B). In fact we could generalize exponentiation to the “finitary product” of the family of types B(x) for x ∈ A, as an inverse image of Pow(Σ(A, B)). If ≺_{A} has order type α and ≺_{B} has order type β then the relation on B^{A} has order type β^{α}.

If ≺_{A} is a total ordering, then taking B as the natural numbers gives Dershowitz and Manna’s [7] ordering on finite multisets of A; define M(A) ≡ Nat^{A}. Informally, a multiset is like a set except that multiple occurrences of an element are significant. Suppose that a_{1} ≺_{A} ⋯ ≺_{A} a_{n}, where a_{i} ∈ A for 1 ≤ i ≤ n. Then the finite multiset containing m_{i} occurrences of a_{i} is represented in M(A) as [⟨a_{1}, m_{1}⟩ …, ⟨a_{n}, m_{n}⟩].

The type M^{∗}(A) of nested multisets over A contains finite multisets with members drawn from both A and M^{∗}(A). Nesting is finite: M^{∗}(A) is built up in stages using the family M^{n}(A) of multisets nested to depth n. The w.f. derivations for + and Σ give the appropriate w.f. relation for M^{∗}(A). Define

M^{∗}(A) ≡ ∑_{n∈Nat} M^{n}(A)  where  M^{0}(A) = A M^{succ(n)} = M^{n}(A) + M(M^{n}(A))

The definition of M^{∗}(A) will be complete once we have defined operations like ∪ and {x} for nested multisets, expressing each multiset as ⟨n, M^{n}(A)⟩ for the smallest n possible.

The type M^{∗}(⊤) is essentially Gentzen’s notation [9] for the ordinals up to ϵ_{0}. While order type ϵ_{0} is larger than necessary for most termination questions in computer science, Dershowitz and Manna give several examples where multisets allow simpler proofs. Often the only alternative ordering is the inverse image of < under a complex and subtle arithmetic function [2].

As defined here, the type M(A) contains only those multisets whose elements are pairwise related under ≺_{A}. If ≺_{A} is not a total ordering, then some multisets are excluded. I doubt that this restriction will seriously complicate program proofs. The typical partial ordering is an inverse image of <. For example, multisets are often used with the subtree ordering on trees; a termination proof using multisets of trees is easily changed to one using multisets of heights of trees. No problems arise in the examples by Dershowitz and Manna [7]. Still, I would like to eliminate the restriction by proving, in Type Theory, that the multiset ordering is w.f. Their proof is far from constructive — it appeals to König’s Infinity Lemma — but perhaps can be formalized using wellordering types.

Boyer and Moore present a particularly interesting termination question [2, pages 67– 71]. Calling the recursive function norm(x) puts the expression x into a certain normal form. Its termination is not obvious because it sometimes calls itself with a larger expression than it was called with. Boyer and Moore justify the definition of norm using a complicated measure function. The LCF system, based on domain theory, can deal with partial functions; it allows a different termination proof, using a lemma that norm(x) terminates for certain x. I have proved the termination of norm in Type Theory by defining a relation corresponding to norm’s recursive calls, and deriving w.f. induction and recursion for this relation [20]. The Type Theory proof bears a striking resemblance, in its outer structure, to the LCF proof; furthermore, it suggests an obviously total alternative definition of norm.

16 Questions

Type Theory seems ideal for working with w.f. recursion and induction. The rules and constructions make computational sense, having as natural a feel as can be expected from a formal notation. I am generally satisfied with this theory of w.f. relations, and look forward to using it in computer proofs. However, some questions present themselves.

16.1 Computation on proof objects

The ability to represent propositions as types allows for a compact logical system, since type operators serve also as logical connectives. Its drawback is that uninteresting propositional constructions can complicate computational ones. Treating the proposition x′ ≺ x as a type causes complications, even though the recursion rule allows wfrec(s, a) to be computed without computation on elements of x′ ≺ x. Recall the rule of w.f. induction:

\frac{a ∈ A \begin{aligned}[ & \begin{aligned}x & ∈ A \\ ih(x′, ls) & ∈ P (x′) [x′ ∈ A; ls ∈ x′ ≺ x] \end{aligned} & ] \\ & s(x, ih) ∈ P (x) \end{aligned}}{wfrec(s, a) ∈ P (a)}

Completely eliminating the dependence of ih on ls would give the rule

\frac{a ∈ A  [ \begin{matrix}x & ∈ A \\ ih(x′) & ∈ P (x′) [x′ ∈ A; x′ ≺ x true] \end{matrix} ] s(x, ih) ∈ P (x)}{wfrec(s, a) ∈ P (a)}

The conclusion of the recursion rule, which is now

wfrec(s, a) = s(a, (x, ls) wfrec(s, x)) ∈ P (a),

would simplify to

wfrec(s, a) = s(a, wfrec(s)) ∈ P (a).

For the characterization of w.f. relations, the type W would become

W ≡ W_{a∈A} {x ∈ A | x ≺_{A} a} ,

and the rank function wof would be just λ(wfrec(sup)).

To achieve all this requires deriving w.f. induction from an induction step that has the slightly stronger induction hypothesis

ih(x′) ∈ P (x′) [ x′ ∈ A; x′ ≺ x true ] .

The proof of ih(x′) may no longer use a particular element ls of x′ ≺ x, though assuming its truth. I doubt that this can be done in general. Though the derivations for subrelations and inverse images use ls only for appealing to w.f. induction on another relation, most other derivations depend crucially on ls.

Consider decidable relations defined as x′ ≺ x ≡ (f(x′, x) = T), where f is a computable function. The rule of equality elimination prevents any dependence on an element of x′ ≺ x. Many w.f. relations are decidable: for every constructive ordinal α, there is a recursive relation corresponding to < for the ordinals below α [23]. But it is unpleasant to impose decidability when none of the derivations appeal to it; furthermore, the subtree relation on infinitely branching wellordering types is clearly undecidable.

Dybjer suggests a radical alternative [8]: reason about programs in an untyped Logical Theory of propositions. Type Theory interprets propositions as types; the Logical Theory takes propositions as primitive and adopts the more conventional interpretation of types as predicates [25]. Because there are no type constraints, the fixedpoint combinator Y exists and can define recursive functions. Proving that a function has a type amounts to proving its termination. Well-founded induction is still required, but Y takes the place of well-founded recursion.

16.2 Does induction entail recursion?

Each derivation of a w.f. relation consists of a derivation of w.f. induction, followed by a proof of the recursion rule for the resulting construction. In every case I have encountered, the proof of the recursion rule closely follows the derivation of induction. It is natural to imagine that the recursion rule always follows from induction, yet this seems impossible to prove. Nor is there an obvious counterexample.

Acknowledgements

Due to the new ideas involved in Type Theory, and the scarcity of published material, I have relied more than usual on discussions with other people. Particular thanks are due to Peter Aczel and Robert Constable, who visited Cambridge, answered many questions, and provided literature. Martin Hyland gave important advice about ordinals. Thanks also to Michael Fourman, Per Martin-Löf, Bengt Nordström, Kent Petersson, Dana Scott, Jan Smith, Richard Waldinger, and Glynn Winskel.

References

[1] R. Backhouse, A.-A. Khamiss, The while-rule in Martin-Löf’s Theory of Types, Dept. of Computer Science, University of Essex, Colchester (1985).

[2] R. Boyer and J Moore, A Computational Logic (Academic Press, 1979).

[3] P. Chisholm, Derivation of a parsing algorithm in Martin-Löf’s Theory of Types, Dept. of Computer Science, Heriot-Watt University, Edinburgh (1985).

[4] A. Church, The constructive second number class, Bulletin of the American Mathematical Society 44 (1938), 224–232.

[5] R. L. Constable, Constructive mathematics as a programming logic I: some principles of theory, in: M. Karpinski (editor), Foundations of Computation Theory (Springer, 1983) 64–77.

[6] R. L. Constable and the PRL staff, Implementing Mathematics with the Nuprl Proof Development System, Report, Cornell University (1986).

[7] N. Dershowitz, Z. Manna, Proving termination with multiset orderings, Communications of the ACM 22 (1979) 465–475.

[8] P. Dybjer, Program verification in a logical theory of constructions, in: J.-P. Jouannaud, editor, Functional Programming Languages and Computer Architecture (Springer LNCS 201, 1985), pages 334–349.

[9] G. Gentzen, New version of the consistency proof for elementary number theory (1938), in: M. E. Szabo, editor, The Collected Papers of Gerhard Gentzen (North-Holland, 1969), 252–286.

[10] M. J. C. Gordon, R. Milner, and C. Wadsworth, Edinburgh LCF: A Mechanised Logic of Computation (Springer, 1979).

[11] Z. Manna, Mathematical Theory of Computation, (McGraw-Hill, 1974).

[12] Z. Manna, R. Waldinger, Deductive synthesis of the unification algorithm, Science of Computer Programming 1 (1981) 5–48.

[13] Z. Manna and R. Waldinger, The Logical Basis for Computer Programming: Volume II: Deductive Techniques (in preparation).

[14] P. Martin-Löf, Constructive mathematics and computer programming, in: L. J. Cohen, J. Los, H. Pfeiffer and K.-P. Podewski, editors, Logic, Methodology, and Science VI (North-Holland, 1982) 153–175. Also in: C. A. R. Hoare and J. C. Sheperdson, editors, Mathematical Logic and Programming Languages (Prentice-Hall, 1984).

[15] P. Martin-Löf, Intuitionistic Type Theory, Bibliopolis (1984).

[16] B. Nordström, Programming in Constructive Set Theory: some examples, ACM Conference on Functional Programming Languages and Computer Architecture (1981) pages 141–153.

[17] B. Nordström and J. Smith, Propositions and specifications of programs in Martin-Löf’s type theory, BIT 24 (1984), pages 288–301.

[18] L. C. Paulson, Lessons learned from LCF: a survey of natural deduction proofs, Computer Journal 28 (1985), pages 474–479.

[19] L. C. Paulson, Natural deduction proof as higher-order resolution, Journal of Logic Programming (to appear).

[20] L. C. Paulson, Proving termination of normalization functions for conditional expressions, Journal of Automated Reasoning (to appear).

[21] K. Petersson, A programming system for type theory, Report 21, Department of Computer Sciences, Chalmers University, Göteborg, Sweden (1982).

[22] K. Petersson, The subset type former and the type of small types in Martin-Löf’s theory of types, Report 3, Department of Computer Sciences, Chalmers University, Göteborg, Sweden (1982).

[23] H. Rogers, Jr., Theory of Recursive Functions and Effective Computability (McGraw-Hill, 1967).

[24] Jan Smith, The identification of propositions and types in Martin-Löf’s Type Theory: a programming example, in: M. Karpinski (editor), Foundations of Computation Theory, (Springer, 1983) 445–456.

[25] Jan Smith, An interpretation of Martin-Löf’s type theory in a type-free theory of propositions, Journal of Symbolic Logic 49 (1984), 730–753.

[26] W. W. Tait, Functionals defined by transfinite recursion, Journal of Symbolic Logic 30 (1965), 155–174.

[27] J. Terlouw, On definition trees of ordinal recursive functionals: reduction of the recursion orders by means of type level raising, Journal of Symbolic Logic 47 (1982), 395–402.