F1 · Algebra
Recursion & induction
A function that calls itself needs only two things: a base case that stops, and a step that moves toward it. The same two parts, used as a proof, are mathematical induction.
Functional code has no loop counter. To walk a list you handle its head and recurse on its tail until nothing is left — iteration is recursion. We trace a recursion through the call stack, see why the base case is what makes it stop, and meet induction, which proves a recursive definition correct using the very same shape.
The call stack
Summing a list has a recursive shape: the sum of [h | t] is h
plus the sum of t, and the sum of the empty list is zero. Each call defers its
addition until the smaller call comes back, so the calls stack up on the way down and the results add up
on the way back.
Step through it. The stack winds down to the base case, then unwinds as each frame returns its value.
- base case
- the input small enough to answer outright — here,
sum([])is 0. - recursive step
- reduce to a smaller input and combine —
h + sum(t). - induction
- a proof with the same two parts: a base case and a step.
- termination
- each step must move toward the base, or the recursion never stops.
sum([1, 2, 3, 4]) · wind down, then unwind
def sum([]), do: 0 def sum([h | t]), do: h + sum(t)
Algebra
sum([h|t]) = h + sum(t), with sum([]) = 0 as the base.
Elixir
Two clauses: one matches [], the other [h | t] — the base and the step.
A recursive call defers its work until the smaller call returns. The stack records the pending steps; the base case is where the returns begin.
The base case
Two conditions make a recursion stop: there must be a base case the recursion can reach, and every step must move toward it. Drop the base case and the calls march past the stopping point and never return — on a real machine, until the stack runs out.
Count down from a number, with and without a base case.
count(n) · does it reach a stop?
Algebra
A recursion is well-founded when a decreasing measure must reach the base.
Elixir
Write the base clause first, and make sure each call shrinks the argument toward it.
No base case, or a step that does not shrink, means no end. Termination is a property you have to design in, not one you get for free.
Induction
Recursion computes; induction proves it correct, and the two share a shape. To show a statement holds for every natural number, prove the base — it holds at the start — and the step — if it holds at n, it holds at n+1. Like dominoes: knock the first, and arrange that each knocks the next, and all of them fall.
Take the claim that 1 + 2 + … + n = n(n+1)/2. Slide n and check the recursive sum against the formula.
Induction · base, then every step
Algebra
Prove P(0), then P(n) ⇒ P(n+1), and P holds for all n.
Elixir
The base clause is the base case; the recursive clause is the inductive step — same two parts.
A recursive function and its proof by induction are the same idea in two registers: define on a base and a step, prove on a base and a step.
What this lands
Recursion is base case plus step: answer the small input outright, reduce everything else toward it. The call stack holds the deferred work, the base case is where returns begin, and termination depends on each step shrinking the input. Induction is the same pair turned into a proof — base and step — which is why a recursive definition and its correctness argument look alike. This is how F1.05’s collections are traversed without a loop. F1.07 packages the most common patterns — map, filter, and reduce — so the recursion is written once and reused.
Next: F1.07 — Higher-order operations (planned) — map, filter, and reduce, the named patterns that capture recursion over a collection. The rest of F1 is on the chapter page.