Well-Foundedness and Reductivity

Before learning dependent types, all I knew about program termination was from the work of Henk Doornbos and Roland Backhouse [DB95, DB96]. I am curious about the connection between their formulation of well-foundedness by relational calculation and the type theoretic view.

It is generally accepted that a relation _<_ is well-founded if, for all x, there is no infinite chain x > x₁ > x₂ > x₃ > …. . A related concept is inducvitity. We say that a relation admits induction of we can use it to perform induction. For example, the less-than ordering on natural number is inductive.

Most of the type theoretical paper I have seen equate well-foundedness to the concept of accessibilty, which I talked about in a previous post. For example, Bengt Nordström [Nor88] introduced the datatype Acc as a “constructively more useful description” of well-foundedness.

Doornbos and Backhouse generalised well-foundedness and other related notions to an arbitrary F-algebra. Well-foundedness, however, was generalised to “having a unique solution.” A relation R : FA ← A is F-well-founded if there is a unique solution for X = S . FX . R.

Reductivity

Inductivity, on the other hand, is generalised to F-reductivity. While F-reductivity is a generalisation of strong induction, Doornbos and Backhouse called it reductivity “in order to avoid confusion with existing notions of inductivity.” [DB95] (Nevertheless, an equivalent concept in Algebra of Programming modelled using membership relation rather than monotype factors, calls itself “inductivity”. Different usage of similar terminology can be rather confusing sometimes.)

A relation R : FA ← A is F-reductive if

$\mu (\lambda P\; .\; R⧷$FP) = id

where ⧷ is the monotype factor defined by ran(R . A) ⊆ B ≡ A ⊆ R⧷B. The function λP . R⧷FP takes coreflexive (a relation that is a subset if id) P to coreflexive R⧷FP, and μ takes its least fixed-point.

Well, it is a definition that is very concise but also very hard to understand, unless you are one of the few who really like these sort of things. If we take P to be a predicate, R\FP expands to a predicate on x that is true if

$\forall y\; .\; y\; R\; x\; \Rightarrow$FP y

Taking the fixed point means to look for the minimum P such that

$\forall x\; .\; (\forall y\; .\; y\; R\; x\; \Rightarrow$FP y) ⇒ P x

The expression now resembles strong induction we all know very well. Computationally, how do we take the fixed point? Of course, by defining a recursive datatype:

data Acc {a : Set}(R : a -> a -> Set) : a -> Set where
  acc : (x : a) -> (forall y -> y < x -> f (Acc R) y) -> Acc R x

where f : (a -> Set) -> (F a -> Set) is the arrow-operation of functor F. When we take F to be the identity functor, it is exactly the definition of accessibility in my previous post! Finally, the requirement that μ(λP . R⧷FP) = id means every element in a is accessible.

So, it seems that reductivity of Doornbos and Backhouse is in fact accessibility, which is often taken by type theorists to be an alternative definition of well-foundedness. Doornbos and Backhouse, however, showed that reductivity guarantees uniqueness solution of hylo equations (which is their definition of F-well-foundedness). The converse, however, is not true in general.

New Reductive Relations from Old

Doornbos and Backhouse also developed some principles to build new reductive relations from existing ones. Let us try to see their Agda counterparts. For simplicity, we take F to be the identity functor in the discussion below.

All initial algebras are reductive. For example, given Pred relating n and suc n, one can show that Pred is reductive.

data Pred : ℕ -> ℕ -> Set where
  pre : (n : ℕ) -> Pred n (suc n)

ℕPred-wf : well-found Pred
ℕPred-wf n = acc n (access n)
  where
    access : (n : ℕ) -> (m : ℕ) -> Pred m n -> Acc Pred m
    access .(suc n) .n (pre n) = acc n (access n)

We have seen in the previous post that the less-than relation is reductive.

If R is reductive and S ⊆ R, then S is reductive too:

acc-⊑ : {a : Set}{S R : a -> a -> Set} ->
      S ⊑ R-> (x : a) -> Acc R x -> Acc S x
acc-⊑ {a}{S} S⊑R x (acc .x h) = acc x access
  where
    access : (y : a) -> (y S x) -> Acc S y
    access y y≪x = acc-⊑ S⊑R y (h y (S⊑R y x ySx))

If f . R . f˘ is reductive for some function f, so is R. This is how we often prove termination of loops using f as the variant.

acc-fRf˘ : {a b : Set}{R : a -> a -> Set}{f : a -> b} ->
    (x : a) -> Acc (fun f ○ R ○ ((fun f) ˘)) (f x) -> Acc R x
acc-fRf˘ {a}{b}{R}{f} x (acc ._ h) = acc x access
  where
    access : (y : a) -> R y x -> Acc R y
    access y xRy = acc-fRf˘ y
      (h (f y) (exists x (exists y (≡-refl , xRy) , ≡-refl)))

where the operators for relational composition (_○_) and converse (_˘) is that defined in AoPA.

Finally, for the special case where F is the identity functor, R is reductive if and only if its transitive closure R⁺ is. Let us first define transitive closure:

data _⁺ {a : Set}(R : a -> a -> Set) : a -> a -> Set where
  ⁺-base : forall {x y} -> R x y -> (R ⁺) x y
  ⁺-step : forall {x z} -> ∃ a (\y -> R y z × (R ⁺) x y) -> (R ⁺) x z

The “if” direction is easy. Let us prove the “only-if” direction.

acc-tc : {a : Set}{R : a -> a -> Set} ->
    (x : a) -> Acc R x -> Acc (R ⁺) x
acc-tc {a}{R} x ac = acc x (access x ac)
  where
    access : (x : a) -> Acc R x ->
        (y : a) -> (R ⁺) y x -> Acc (R ⁺) y
    access x (acc .x h) y (⁺-base yRx) = acc-tc y (h y yRx)
    access x (acc .x h) y (⁺-step (exists z (zRx , yR⁺z))) =
      access z (h z zRx) y yR⁺z

Combined with the proof that Pred is reductive, we have another way to show that the less-than relation is reductive. One may compare it with the proof of well-found _<′_ in the previous post.

References

[DB95] Henk Doornbos and Roland Backhouse. Induction and recursion on datatypes. B. Moller, editor, Mathematics of Program Construction, 3rd Internatinal Conference, volume 947 of LNCS, pages 242-256. Springer-Verslag, July 1995.

[DB96] Henk Doornbos and Roland Backhouse. Reductivity. Science of Computer Programming, 26, pp. 217--236, 1996.

[Nor88] Bengt Nordström. Terminating general recursion. BIT archive, Volume 28, Issue 3, pp 605-619. 1988.