## Introduction

As we (may) know recursion is one of the most important elements in functional programming, and one of the charm of recursion, usually paired with algebraic data types is that the computation can be guaranteed to terminate by the compiler, if implemented in a specific way, a.k.a. the “Structural Recursion”.

For example:

```
data Tree = Leaf | Branch Tree Int Tree
treeSum :: Tree -> Int
treeSum Leaf = 0
treeSum (Branch l x r) = treeSum l + x + treeSum r
```

`treeSum`

could be guaraneteed that it terminates regardless of
the input (although haskell doesn’t do that by default), because the argument of
the recursive call `treeSum l`

and `treeSum r`

is *strictly smaller* than the
parameter, in the sense that `l`

and `r`

are the “sub-structure” of the input
`Branch l x r`

.

The structural recursion is even more important in theorem provers like Agda and Coq, and the structural condition is strictly enforced by those compilers, because otherwise we would be able to prove anything with an infinite loop.

```
(* Of course this would be rejected by Coq *)
Definition anything_is_true (A : Prop) : A := anything_is_true A.
```

However, the structural restriction is sometimes a bit too strong, even though sometimes it’s “easy” to tell that the structure of the arguments for the recursive call should be decreasing, consider this famous sorting algorithm:

```
quickSort :: Ord a => [a] -> [a]
quickSort [] = []
quickSort (x : xs) = quickSort l ++ [x] ++ quickSort r
where
l = filter (<= x) xs
r = filter (> x) xs
```

Of course haskell doesn’t argue with us about this recursive definition, but it
should be clear that this is **not** a structural recursion, as `l`

and `r`

here are
not necessarily structurally smaller than the argument `x : xs`

. And language
like “Coq” would mercilessly reject a similar definition. Although coq is being
reasonable rejecting this definition, how do we convince the compiler that this
is indeed a safe recursive call, given the `filter`

is implemented properly.
Years ago I implemented a similar thing in agda, and what I did is use a compiler
pragma to bypass the structural termination check, which surely is not a very
reliable way if we are going to implement something more complicated than this.

In these two (or three) articles, I’m going to share some of the interesting techniques I learned which enable us to implement less restricted recursions, without violating the structural recursion restriction.

For the sake of visual clarity I would use Idris (instead of Coq) as the sample langauge which has a similar syntax to Haskell.

## Well-founded Recursion/Induction

### Well-founded Relation and the Finitely Descending Chain

Our first technique, probably the most practical one we are going to explore
, makes use of this set theory concept “Well-founded Relation”,
frankly the mathematical definition looks quite scary for those unfamiliar with the notations.
But the idea is, given a set \(S\) with a binary relation \(R\), and
with an arbitrary element \({a~|~a \in S}\), we can find a chain with relation \(R\):
\(R~a_0~a\), \(R~a_1~a_0\) , \(R~a_2~a_1\) and it goes on.
If for any element \(a \in S\), this chain starts from \(a\) **stops** at some point,
i.e. \(R~a_{n+1}~a_n\) , but there does **NOT** exist \(\{m~|~m \in S \land R~m~a_{n+1} \}\),
then we say the relation is well-founded. For example, the “less-than”
(\(<\)) relation on natural number set is well-founded, because for any
arbitrarily chosen number \(n\) and an arbitrarily chosen “less-than chain”,
the chain always stops at 0, because there isn’t any natural number that is
less than 0.

Why is this useful? Well, not immediately, but it gives us a tangible approach
to convince someone who doesn’t trust intuition (the compilers) that some recursive
call terminates: if we are given a natural
number `x`

as argument for some recursive function `f`

, then as long as we guarantee
the argument of all the recursive calls are *less than* `x`

, we guarantee the
recursion terminates, because “less-than” is a well-founded relation, and as
long as we follows the “chain” when making recursive calls, the chain has to
terminate at some point to respect the mathematical truth.

And we can conceptualize the “chain” with something like this:

```
data ChainOf : (a -> a -> Type) -> a -> Type where
Stop : (x : a) -> ((y : a) -> Not (DPair a (\y => r y x))) -> ChainOf r x
GoOn : (x : a) -> (y : a) -> r y x -> ChainOf r y -> ChainOf r x
f : ChainOf r a -> ()
f (Stop x p) = () -- do something with base case
f (GoOn x y p subChain) = f subChain -- do something between x and y
```

And we can safely define a recursive function with respect to the structure of
the chain constrained by the relation `r`

, breaking free from having to recurse
on the structure of the exact value (`y`

doesn’t have to be a sub-structure of `x`

,
yet the recursive call shift the argument from something about `x`

to something about `y`

).

However this definition of `ChainOf`

isn’t that practically useful, since we have
no control over the value of the sub-case of recursion,
we are given `y`

and a proof that `r y x`

holds, but when defining recursive function like `quickSort`

,
what we want is a specific value of argument for sub-cases
(from `x : xs`

to `filter (<=) xs`

, for example), an arbitrary pre-selected choice wouldn’t do.

`Acc`

and its Recursion Operator

So instead of recursing on a specific chain, we need a collection of chains from which we can select the ones that suits our need. In most of the cases the potential choices could be infinite, so we could do something like this:

```
-- Acc is short for "Accessible"
data Acc : (a -> a -> Type) -> a -> Type where
MkAcc : (x : a) -> ((y : a) -> r y x -> Acc r y) -> Acc r x
```

Here `Acc r x`

reads: `x`

is *accessible* (from the end of the chain) using relation `r`

.
The function `(y : a) -> r y x -> Acc r y`

gives us a way to select the next step of recursion,
but of course we cannot just select an arbitrary value in the set (of type `a`

), we need
to provide a proof that the `y`

we choose indeed satisfies `r y x`

.
So this simple, eh, probably not, this minimal definition captures all the
possible chains from the end of the chain to `Acc r x`

.

But wait, how this single constructor expresses where the chain stops? The chain
stops when there isn’t any `y : a`

such that `r y x`

, so the selection pool for
“next steps” is practically empty as we wouldn’t be able to access any next
step `Acc r y`

if we cannot prove any `r y x`

.

And for those of you who are familiar with inductive/recursive principles, the recursive principle for this type, or the fixpoint operator we are looking for is:

```
accRec : {P : a -> Type}
-> ((x : a) -> ((y : a) -> r y x -> P y) -> P x)
-> {x : a} -> Acc r x -> P x
accRec rec (MkAcc x f) = rec x $ \y, ryx => accRec rec (f y ryx)
```

From the perspective of the definition of this operator, ignoring the the
longest parameter type, the type of the function says:
if `x`

is *accessible* with a certain `r`

, when you give me *something* (the parameter with the longest type),
I can help you run the recursive procedure and give you the final result (`P x`

).
And the longest parameter type says: for all the possible `x`

,
if you can show me how to compute the result for all `y`

which is the next step
of the chain, I can show give you the result for `x`

.

Then the definition is rather short since we only have one case to deal with,
the key is to show the recursive procedure (`rec`

) that, starting from an
arbitrary sub-case (`y : a`

with `r y x`

), how to compute the result about `x`

(`P x`

),
which is indeed possible because the accessibility condition (`Acc r x`

) helps
us prove that any sub-case `y`

is accessible given `r y x`

.
Then the recursive call of `accRec`

handles the rest.

Before delving into the important details of this recursive definition, let’s quickly formulate the “well-founded” condition, and show you how they are used:

```
wellFounded : (r : a -> a -> Type) -> Type
wellFounded {a} r = (x : a) -> Acc r x
-- simply delegates to accRec
-- as `wellFounded` says any value of `a` is accessible
wfRec : {P : a -> Type}
-> ((x : a) -> ((y : a) -> r y x -> P y) -> P x)
-> wellFounded r -> (x : a) -> P x
wfRec rec wf x = accRec rec (wf x)
```

### Well-founded Recursion and Revisiting Quicksort

Now let’s go back to the quicksort and think about what are we doing with the list. The well-founded relation we can find here, is that the argument lists for the recursive call is guaranteed to be shorter than the the original argument. And we know that the length of finite lists can only decrease finitely, hence a comparison on length of the two lists is a well-founded relation.

So first we are going to define a relation about the lengths of two lists, and convince our compiler that the relation is indeed well-founded.

```
LengthLT : {a : Type} -> List a -> List a -> Type
LengthLT xs ys = LT (length xs) (length ys)
wfLengthLT : {a : Type} -> wellFounded (LengthLT {a})
wfLengthLt = ...
```

I omit the proofs here, but if you are interested you can find them here

Then the implementation for quicksort follows:

```
quickSort : Ord a => List a -> List a
quickSort {a} = wfRec {P = const (List a)} quickSort' wfLengthLT
where
quickSort' : (xs : List a)
-> ((ys : List a) -> LengthLT ys xs -> List a)
-> List a
quickSort' [] _ = []
quickSort' (x :: xs) rec
= rec (filter (\v => v <= x) xs) (LTESucc (filterSmaller _))
++ [x]
++ rec (filter (\v => v > x) xs) (LTESucc (filterSmaller _))
```

Unlike the complex-looking types of the fixpoint operator and quicksort itself,
the actual definition is rather clean. We delegate the implementation of quicksort
to a application of the well-foundedness recursive operator `wfRec`

. Like using a
conventional fixpoint operator, we accept the recursive version of the function
as a parameter (`rec`

), but here the recursive call is guarded by the condition
that the argument have to be shorter than the argument of parent call (`LengthLT ys xs`

).
And we have to provide the proof of such relation holds upon making the recursive
call (`LTESucc (filterSmaller _)`

). In this case we guarantee that the whatever
comes out of the `filter`

must not be longer than whatever goes in (idris
generously provide exactly what we need in the library (`filterSmaller`

)), hence the
argument of the recursive call is at least shorter by one than the argument of
the caller. Then the rest is only that you convincing yourself calling the `rec`

is indeed making a recursive call.

Although it looks like we are doing exactly the same thing as in the intro, this definition perfectly conforms the structural restriction, hence is guaranteed by the compiler that it terminates with all possible inputs. Quite impressive isn’t it?

### The Mystery of Structural Recursion

Apparently we achieve all these with the conventional structural recurison, but if you looking carefully at the definition of our essential operator:

```
accRec : {P : a -> Type}
-> ((x : a) -> ((y : a) -> r y x -> P y) -> P x)
-> {x : a} -> Acc r x -> P x
accRec rec (MkAcc x f) = rec x $ \y, ryx => accRec rec (f y ryx)
```

The argument of the recursive call is `f y ryx`

. How is it a sub-structure of
`MkAcc x f`

when it’s a return value of a function call? And more importantly
this definition doesn’t look terminating when there is only one case, and it’s
a recursive case.

Well, it definitely should terminate as that’s what mathematics tells us.
~~The most straightforward way to look at it is that it’s an generalized inductive
type (or reflexive data type) that the function represents a mapping from an
generalized index to a sub-structure.~~ But probably easier to understand, another
way is realizing that the function is not arbitrary, it comes from a correctly
constructed value of inductive types, which is obligated to find a function
that correctly construct the “sub-structure” whose procedure has to be finite
(with the structural restriction enforced). So in the end, it *will* go down
to the end of the chain, where any further descend will lead to a
contradiction. For example when constructing (Acc (<) 0), it’s impossible to find
any natural number `a`

such that `a < 0`

, hence the definition of
`(a : Nat) -> a < 0 -> Acc (<) a`

is trivial.

That’s also how a (seemingly) single case of recursion covers both base case
and recursive case. When reaching the end of the chain, where there is no `y`

such that `r y x`

, `r y x`

is isomorphic to \(\bot\) (a type with no value),
so whatever we do when constructing `(y : a) -> r y x -> P y`

is trivial
since it’s impossible to find its arguments and the recursion will never be called.