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 *well-founded* if, for all *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****F**A ← A **F****F**X . R

### Reductivity

Inductivity, on the other hand, is generalised to **F****F**

A relation **F**A ← A if

**F**-reductive

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

where *monotype factor* defined by **F**P**F**P

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 **F**P

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

Taking the fixed point means to look for the minimum

$\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 **F**P) = id`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**

### 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

`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

`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**

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