Well-founded Relation

Idea

In constructive type theory, a relation is well-founded if every element of the domain is accessible. Accessibility is defined inductively: an element $x$ is accessible if all elements “smaller” than it are accessible. This definition enables the principle of well-founded induction (recursion) without assuming LEM or requiring a decreasing measure to naturals.

Definition

Let $A$ be a type and $\prec$ be a binary relation on $A$ (i.e., $\prec :A\to A\to \mathcal{U}$).

The accessibility predicate, ${\text{Acc}}_{\prec }:A\to \mathcal{U}$, is defined inductively. The single constructor is:

$$\text{acc}:\prod _{x:A}\left(\prod _{y:A}(y\prec x\to {\text{Acc}}_{\prec }(y))\right)\to {\text{Acc}}_{\prec }(x)$$

The relation $\prec$ is well-founded if every element of $A$ is accessible:

$$\text{IsWellFounded}(\prec ):\equiv \prod _{x:A}{\text{Acc}}_{\prec }(x)$$

Well-Founded Induction

The induction principle derived from well-foundedness states that to prove a predicate $P(x)$ for all $x$, it suffices to show that for any $x$, if $P(y)$ holds for all $y\prec x$, then $P(x)$ holds.

$$\text{wf-ind}:\left(\prod _{x:A}(\prod _{y:A}y\prec x\to P(y))\to P(x)\right)\to \prod _{x:A}P(x)$$

In type theory, this corresponds to the recursor on the Acc type.

Well-Founded Recursion

Well-founded recursion generalizes well-founded induction by allowing $P$ to be a family of types that is generated by the recursion procedure. See Distinction from well-founded induction below.

Agda Implementation

The definition translates directly to an inductive family.

module WellFounded where
 
open import Agda.Primitive
 
data Acc {ℓ ℓ'} {A : Set ℓ} (_<_ : A → A → Set ℓ') (x : A) : Set (ℓ ⊔ ℓ') where
  acc : ((y : A) → y < x → Acc _<_ y) → Acc _<_ x
 
WellFounded : {ℓ ℓ' : Level} {A : Set ℓ} → (A → A → Set ℓ') → Set (ℓ ⊔ ℓ')
WellFounded _<_ = ∀ x → Acc _<_ x
 
-- Induction principle (dependent eliminator)
wfInd : {ℓ ℓ' ℓ'' : Level} {A : Set ℓ} {_<_ : A → A → Set ℓ'}
      → (P : A → Set ℓ'')
      → ((x : A) → ((y : A) → y < x → P y) → P x)
      → (x : A) → Acc _<_ x → P x
wfInd P step x (acc rs) = step x (λ y y<x → wfInd P step y (rs y y<x))

Remarks

Distinction from well-founded induction

The primary distinction between well-founded induction and recursion lies in the universe level of the motive. Induction targets a predicate $P:A\to \text{Prop}$ to establish validity, whereas recursion targets a family of types $B:A\to \mathcal{U}$ to compute data. Computationally, wfRec functions as a fixpoint combinator that performs structural recursion on the accessibility witness $\pi :\text{Acc}(x)$. This allows the definition of total functions on domains that are not inductively defined, provided the relation is well-founded, without requiring a decreasing natural number measure.

A critical subtlety in intensional type theory is the function’s dependence on the specific witness $\pi$. Because Acc is an inductive type in $\mathcal{U}$, distinct derivation trees of accessibility could theoretically result in distinct values for $f(x)$. To ensure the function $f$ is extensionally determined solely by $x$, one typically requires that Acc x be a mere proposition (proof irrelevance), which is often provable in Homotopy Type Theory or Cubical Agda given the extensionality of the underlying relation.

• Induction: The motive is a predicate $P:A\to \text{Prop}$ (or a subsingleton type). The goal is to construct a witness of truth. Since propositions are proof-irrelevant, the specific structure of the Acc derivation is computationally irrelevant to the resulting truth value.
• Recursion: The motive is a family of types $B:A\to \text{Type}$. The goal is to compute a value. The resulting function $f(x)$ is defined by structural recursion on the proof $\pi :\text{Acc}(x)$.

Accessibility Witnesses

In well-founded recursion, an accessibility witness is a proof that an element is accessible. The structure of this witness determines the computational behavior of functions defined by well-founded recursion.

In intensional type theory, functions may depend on the specific derivation tree of the accessibility proof, requiring proof irrelevance to ensure extensionality.