recursion.md

Characterize recursable data structures

Recursion

Recursion is a procedure that allows us to iterate through certain data structure. For example we can iterate through lists

sum : List Nat -> Nat
sum list =
    if (empty list)
    then 0
    else (head list) + (sum (tail list))

or through natural numbers

factorial : Nat -> Nat
factorial n =
    if (n == 0)
    then 1
    else n * (factorial (n - 1))

The question is now: How can we describe all the data structures (types) where we can perform recursion.

Find the key elements

We need two things to actually recurse over a data structure T:

• a base case, when recursion terminates
• a way to reduce to a case somehow closer to the base case, to perform the inductive step

In terms of functions, the base case is just a functions

isBaseCase : T -> Bool

which returns True if we are in the base case. In the above examples, this was empty for lists and \n -> n == 0 for natural numbers.

To perform the inductive step instead, we have a function

reduce : T -> T

which corresponds to tail for lists and \n -> n - 1 for natural numbers.

(Note: actually reduce needs to be defined only for T \ isBaseCase^{<-}(True), where isBaseCase^{<-}(True) is the set of elements of T which evaluate to True when we apply isBaseCase)

We're still not expressing the fact that, when we perform the inductive step, we end up closer to the base step. Moreover, when we recurse, we would really like to end up in the base case in a finite number of steps.

We can express this introducing a new function

distance : T -> Nat
distance t = min {n / isBaseCase (reduce^n (t)) = True}

which tells us how many times (reduce^n means reduce composed with itself n times) we need to apply reduce to end up in the base case. For lists this function is just length, while for natural numbers is the identity.

Now we can express that reduce actually takes us closer to the base case saying that the following relation must be satisfied

distance (reduce t) < distance t

for every t \in T.

Generalize

If what we said above is actually true, now to know if we can perform recursion on a data structure, we just need to have the functions defined above. Once we have them, we can do recursion without knowing anything else about our type T.

Moreover, this allows us to write generic recursive functions of the form

recursive : T -> A
recursive t =
    if (isBaseCase t)
    then f(t)
    else g(t) <> recursive (reduce t)

where f : T -> A and g: T -> A and <>: T x T -> T is just a binary operation of T

Thinking further

Maybe we can solve the Note above, and at the same time simplify everything, by introducing a new data type

data RecursionState
    = BaseCase
    | Distance Nat

and a single function

distance : T -> RecursionState

which now is total (read: defined for every t in T) and holds the same information that isBaseCase and distance hold above.

@marcosh according to you could the induction and recursion be the same concept? I see a lot of similarities between them. Or is it just that induction is the approach we use to "explain" how recursion works? See here, for example.

The two concepts are certainly related.

If with induction we talk about proof by induction, we can see a proof as a function proof : T -> Bool which always returns true (think for example to "every natual number is >= 0" as the function \n -> n >= 0). If proof can be written in the form of the recurse above, we can "prove" such a function by doing recursion on T (if T admits recursion). If that is the case, it is enough to prove that proof returns true in the base case and that we can prove proof(t) by using the value of proof(reduce(t)) (i.e. we need to prove g(t) <> proof(reduce t) returns True is reduce t returns True)

So basically could we define an inductive proof as a type of recursion "type class"?

I don't want to trouble the Curry-Howard correspondance, but we should be able to make the following connections:

• a proposition is a type T
• we can evaluate the "truthness" of a proposition with a function T -> Bool
• (here I think I'm deviating from Curry-Howard) a proof of a proposition T is a function T -> Bool which always evaluates to True
• an inductive proof is a function T -> Bool, where T is a recursive data structure (i.e. T implements Recursable), of the form

proof : T -> Bool
recursive t =
    if (isBaseCase t)
    then f(t)
    else g(t) <> recursive (reduce t)

Does this answer your question?

For sure your answer boosts my brain 💥 , so I'd say that it is helping me to figure out how to reason about this 😄

Just as another set of notes to discuss about: Inductive Proofs with Idris Lang.