Are induction and recursion twin sisters?

Question

I am asking a soft question.

For me it feels like induction and recursion are dual to each other (in somewhat category-theory-like sense, which I can not define rigorously):

• both do have at least one base case (yeah, some recursions do not have, I am aware of that and this fact seems to break some of my assumptions);
• both can be seen as a "sequence of consequences", where: a) induction defines $n + 1$ consequence in term of $n$ consequence (i.e. next state in terms of previous one) and b) recursion defines $n$ in terms of $n + 1$ (dependency arrow turned around: once again, reminds category theory's duality).

I'd like to now how deep the rabbit hole goes.

Answer 1

They are not 'dual' to each other. They are essentially the same thing.

In dependent type theories, the induction principle on the natural numbers looks something like:

induction : (T : ℕ -> Type) -> T 0 -> (∀ n. T n -> T (suc n)) -> ∀ n. T n

This says that for a family of types indexed by the naturals T, if we can exhibit a value with type T 0 and a function for constructing a T (suc n) from a T n for all n, then we can construct a T n for every choice of n. However, if we simply use a constant family of types T n = R, we instead get the type:

(R : Type) -> R -> (ℕ -> R -> R) -> ℕ -> R

And this is the type of primitive recursion on the natural numbers. So, one of the fundamental ideas in type theory is that the computational behavior of an induction principle is recursion. Or, the induction principle is recursion with a fancier type.

Over in category theory, one talks about these inductively defined types as free algebras. If you have a functor $F$, then an algebra is a pair $(A, α : F A → A)$. Here $A$ might be called the 'carrier' and $α$ the 'action'. Homomorphisms between algebras are maps between carriers that form a commutative square with the actions in an 'obvious' way. Then a free (or initial) algebra is one $(μF, ι : F μF → μF)$ such that there is a unique homomorphism from it to every other algebra.

In the case of the naturals, the functor is $F A = 1 + A$, and an algebra action $1 + A → A$ is actually like two of the arguments to structural recursion $(1+A→A) \cong A × (A → A)$. Given these arguments, we get a homomorphism $\mathsf{rec} : ℕ → A$, and the commutative property it has means that it behaves like recursion.

Now, in the type theories above we can define a type Σ ℕ T, which has values (n, t) such that n : ℕ and t : T n. Given tz : T 0 we can construct sz = (0, tz) : Σ ℕ T, and with ts : ∀ n. T n -> T (suc n) we can define:

 ss : Σ ℕ T -> Σ ℕ T
 ss (n, tn) = (suc n, ts n tn)

With sz and ss, we can define an algebra with carrier Σ ℕ T. So this gives us a function ℕ -> Σ ℕ T. But, it turns out that the uniqueness property of $\mathsf{rec}$ above (along with the definition of ss and sz) allows us to deduce that the first component of the result of $\mathsf{rec}$ is the number we fed in. And this means that if we gave it n, then the second component of the result has type T n. So this means that this use of $\mathsf{rec}$ gives us induction above.

Depending on the exact setting, more machinery might be involved. But induction and recursion are indeed closely related.

Answer 2

Assume the well-ordering principle.

Theorem. (Induction) Let $\varphi(x)$ be a formula with free variable $x$. Assume $$(\forall n\in\mathbb{N})[(\forall m<n)[\varphi(m)]\:\Rightarrow\:\varphi(n)].$$ Then $\{n\in\mathbb{N}:\neg\varphi(n)\}$ has no minimum. Furthermore, $\{n\in\mathbb{N}:\neg\varphi(n)\}=\varnothing$.

Theorem. (Recursion) Let $X$ be a set. Fix $f:X\to X$. Fix $a\in X$. There exists a unique function $g:\mathbb{N}\to X$ such that $$g(0)=a\qquad\text{and}\qquad g(n+1)=f(g(n))$$ for every $n\in\mathbb{N}$. Furthermore,

(i) $g:\mathbb{N}\hookrightarrow X \iff a\notin \mathrm{ran}(f\big|_O)$ and $f\big|_O:O\hookrightarrow X$, where $O:=\{g(n):n\in\mathbb{N}\}$.

(ii) $g:\mathbb{N}\twoheadrightarrow X\iff (\forall A\in\mathscr{P}(X))[a\in A\,\wedge\,f(A)\subseteq A\:\Rightarrow\:A=X]$.

Terminology. Let $X$ be a set. Fix $f:X\to X$. Fix $a\in X$. Say $\langle X,f,a\rangle$ is isomorphic to the natural numbers, denoted $\langle X,f,a\rangle\cong\langle\mathbb{N},+1,0\rangle$, if $a\notin \mathrm{ran}(f)$ and $f$ is 1-to-1 and for each $A\in\mathscr{P}(X)$, if $a\in A$ and $f(A)\subseteq A$, then $A=X$.

Answer to your question. Induction is a corollary of the well-ordering principle. Recursion is the existence of morphisms from the natural numbers to structures of the form $\langle X,f,a\rangle$.