In Douglas Hofstadter’s classic book Gödel, Escher, Bach, the philosopher Zeno introduces his famous paradox by saying:

Not the wind, not the flag—neither one is moving, nor is anything moving at all. For I have discovered a great Theorem, which states: “Motion is Inherently Impossible.”

The paradox argues that, because any motion is composed of an infinite series of ever-smaller changes, it must therefore take an infinite amount of time, and so no motion can ever be completed. We know this to be false, but his idea of turning a process into an infinitely recursive structure turns out to be a very powerful idea and underlies many results in maths and computer science.

Once upon a time, the addition of recursion to programming languages was a controversial topic, these days it is so commonplace that programmers take it for granted. For example, if we have to find information in an HTML document, we can write a recursive function. It checks to see if the current node matches our requirements, and then repeats the process on all the node’s children.

function getElementsByTagName(name, root) {
  root = root || document.body

  let elements = [],
      children = root.childNodes

  if (root.tagName === name)
    elements.push(root)

  for (let i = 0, n = children.length; i < n; i++)
    elements = elements.concat(
      getElementsByTagName(name, children[i])
    )

  return elements
}

getElementsByTagName is a recursive function, defined in terms of itself. When applied to a tree, it will eventually reach the leaves of the structure and stop recursing. If we need to scrape information from a whole website, or even all the websites in the world, we can request a page, parse it, find all the links in it, and then repeat the process on all the URLs we find.

async function spider(pageUrl) {
  let html = await fetch(pageUrl).then((resp) => resp.text())

  jsdom.env(html, (error, window) => {
    let body  = window.document.body,
        links = getElementsByTagName('A', body)

    let urls = links.map((link) => url.resolve(pageUrl, link.href))

    urls.forEach((url) => spider(url))
  })
}

Frequently we talk about recursive procedures: functions that execute a sequence of instructions, where some of those instructions are calls to the function itself. But we don’t talk so much about recursive structures. Sure, we create them all the time, when we render HTML or build a website, but they just sort of exist. They don’t do anything by themselves, the functions are the important thing!

I’d like to show you a few things recursive structures can do, some things that are useful, interesting, and in some cases surprising. We don’t have to look too far from these first examples to find a recursive structure: the JavaScript object system uses one.

When we make a new object, it has a hidden field called __proto__ that points to the object it inherits from. We can form chains of these inheritance relationships.

let person = { name: 'james' }

let p1 = Object.create(person)
// p1.__proto__ == person

let p2 = Object.create(p1)
// p2.__proto__ == p1

When we access a property or call a method in JavaScript, it checks the receiving object for that property. If the property does not exist in that object, it looks in its __proto__ object, and so on until it finds an object with that property.

p2.name // -> p2.hasOwnProperty('name') -> false
        //    p2.__proto__.name

        //    p1 = p2.__proto__
        //    p1.hasOwnProperty('name') -> false
        //    p1.__proto__.name

        //    person = p1.__proto__
        //    person.hasOwnProperty('name') -> true

        //    person.name
        //    -> 'james'

This recursive structure serves a single purpose: it describes how objects inherit from one another. And since it exists solely for that purpose, we could say this structure is how objects inherit from each other. Sure, there are functions in the JavaScript runtime that walks this structure, but we don’t need to see those functions to understand how the relationship operates.

I’m going to talk about three things in this series, three things that are made possible by recursive structures. Those things are, in no particular order: correctness, performance, and meaning. Let’s begin by talking about correctness.

In mathematics, there is a technique called proof by induction. This technique involves a recursive argument: we assume that a statement is true in some specific case in order to prove it is true in general. This sounds like begging the question, how could it possibly used in logical proofs? Well, let’s look at an example: the sum of the integers from 1 to n.

sum(1 .. 1) =  1

sum(1 .. 2) =  3

sum(1 .. 3) =  6

sum(1 .. 4) = 10

The sum of the integers from 1 to 1 is 1. The sum from 1 to 2 is 3. The sum from 1 to 3 is 6. The sum from 1 to to 4 is 10. And if we continue this sequence we may eventually realise these numbers seem to follow a pattern, namely: the sum from 1 to n equals n times n+1 all over 2.

                  n (n + 1)
sum(1 .. n)   =   ---------
                      2

We can make an intuitive argument for this being true. Think of the numbers from 1 to 10. If we pair 1 up with 10, and 2 with 9, and 3 with 8, and so on, then we end up with 5 pairs of numbers that add up to 11. That is, n/2 pairs adding up to n+1.

                1    2     3     4     5
               10    9     8     7     6
        --------------------------------
        sum:   11   11    11    11    11

But lists of concrete examples, no matter how many we have, are not proof. As programmers, we can write any number of unit tests for a function and still not know for certain that it works in general. So how do we prove it? We know, by definition, that the sum from 1 to n+1 is the sum from 1 to n, plus n+1.

sum(1 .. n+1) =   sum(1 .. n) + (n + 1)

This is recursive definition of sum that means that if we know the sum from 1 to n, we can work out the sum to n+1. We’d like to prove our formula above that gives the result purely in terms of n so that we can work out any sum without computing all the previous ones.

Proof by induction works as follows. First, we assume our formula for sum is correct, and substitute it it into the recursive definition, i.e. we replace sum(1 .. n) with our formula, n (n + 1) / 2, giving us the following:

                  n (n + 1)
sum(1 .. n+1) =   --------- + (n + 1)
                      2

If we multiply out the numerator in the first term, we get n^2 + n:

                  n^2 + n
sum(1 .. n+1) =   ------- + (n + 1)
                     2

We rewrite the second term as a fraction: 2n +2 over 2.

                  n^2 + n   2n + 2
sum(1 .. n+1) =   ------- + ------
                     2         2

And then we can add the two fractions together, giving n^2 + 3n + 1 all over 2.

                  n^2 + 3n + 2
sum(1 .. n+1) =   ------------
                        2

This can be factored as n + 1 times n + 2 over 2:

                  (n + 1) (n + 2)
sum(1 .. n+1) =   ---------------
                         2

Now, n + 2 is the same as (n + 1) + 1, so we can rewrite this as:

                  (n + 1) ((n + 1) + 1)
sum(1 .. n+1) =   ---------------------
                            2

Now, we have an expression that looks exactly like our original formula, with n replaced by n + 1.

                  n (n + 1)                         (n + 1) ((n + 1) + 1)
sum(1 .. n)   =   ---------   =>  sum(1 .. n+1) =   ---------------------
                      2                                       2

We have shown that if this formula in n is true, then this one in n+1 is true. If we can find some value of n where the formula is correct, then by a recursive argument, we know it’s true for all successive values of n. And indeed, we saw several such examples earlier, so we know this is true for all n from 1 upwards.

Now there is a related technique that allows us to do exactly the same thing with data structures, and it’s called structural induction. In functional programs, rather than having arrays that are flat sequences of values, we have lists, which are defined recursively. A list is either the empty list, or a value paired with a list. In Haskell syntax this might be written as “a list of t ([t]) is either the empty list ([]), or a value of type t paired with a list of t (t : [t])”.

data [t] = [] | t : [t]

So, our flat arrays are replaced with recursive pairs, and those pairs form a tree, with the empty list as the terminating pair.

[1, 2, 3, 4]  ==  (1 : (2 : (3 : (4 : []))))

Or, to represent this graphically, the list is a lop-sided tree whose left-branches are the values and whose right-branches point to the rest of the list.

                  .
                 / \
                1   .
                   / \
                  2   .
                     / \
                    3   .
                       / \
                      4   []

In this world, we define functions on lists recursively. For example, the length function takes a list [t] and returns an Int. The length of the empty list is zero. The length of of any other list (the pattern x:xs destructures the list into its first element and all the rest) is one plus the length of the rest of the list.

length        :: [t] -> Int
length []     =  0
length (x:xs) =  1 + length xs

map takes a function of type a to b (the a -> b type), and a list of a, and returns a list of b. Mapping a function over the empty list gives the empty list, and mapping a function over any other list means applying f to the first element and pairing that with the map over the rest.

map           :: (a -> b) -> [a] -> [b]
map f []      =  []
map f (x:xs)  =  f x : map f xs

(A note on Haskell notation: function calls do not need parens and commas like in other languages, so the expression f x : map f xs roughly means f(x) : map(f, xs) in more conventional syntax.)

In Haskell, functions are not lists of instructions that define processes. Functions are not executed from top to bottom completely before returning a value. Instead, Haskell functions define equations: they simply declare that two expressions are equal. They say, anywhere we see the expression on the left, we can replace it with the one on the right. They are rewrite rules, and these rewrite rules, just like the rules of algebra, allow us to prove things about these functions.

Let’s look at an example. We’ll prove something called the functor composition law. Haskell has a function called . (a single dot), which composes two functions. It takes a function b -> c, and a function a -> b, and returns a function a -> c. f . g is the composition of functions f and g, which if applied to some value h gives the same result as f (g h). result of applying g to h.

(.)       :: (b -> c) -> (a -> b) -> a -> c
(f . g) x =  f (g x)

The functor composition law states that mapping function g over a list, and then mapping f over the result, is the same as mapping f . g over the original list. In JavaScript syntax that would mean list.map(g).map(f) gives the same answer as list.map(compose(f, g)).

map f (map g list)  ==  map (f . g) list

How do we prove that? When we proved sum, we began by stating the function for n+1. When dealing with lists, we state the definition for the list plus one more element, or x : list in Haskell notation.

    map f (map g (x : list))

Now we attempt to rewrite this until it’s in a form we want. The definition of map says that map f (x:xs) = f x : map f xs, and so we can rewrite the inner term as g x : map g list:

    map f (g x : map g list)

The outer term is now in the form map f (x:xs) and we can rewrite it:

    f (g x) : map f (map g list)

Now comes the inductive step: we assume that map f (map g list) == map (f . g) list, so the above equals:

    f (g x) : map (f . g) list

The first term f (g x) is just the definition of (f . g) x so we can again rewrite that term:

    (f . g) x : map (f . g) list

Now by the definition of map, this is the same as map (f . g) (x : list), and so be assuming the functor composition law is true for list, we have proven it for list with one more element:

    map f (map g (x : list)) == map (f . g) (x : list)

We just need a find a base case where the law is true, and then we know it’s true for all lists longer than that. And indeed, the empty list works: map f [] = [] by definition of map, for any f, so the composition law is trivially true in that case.

These proofs are only possible because of our recursive definition, and indeed this technique underlies most if not all systems of proof for program correctness, including type systems. In a procedural language, where these functions would be written using for-loops, we cannot do this. A for-loop is not a structure, it’s a procedure, it has state, we cannot say that it is equal to anything or give it a meaningful type. Whereas, just by shunting symbols around mechanically, a compiler for a functional language can prove things about it, because its functions are defined as recursive equations between structures.

I want to point out two aspects of these proofs. First, notice how when we replace a function with its definition, we just expand it one step, rather than evaluating it for the whole input list. This partial evaluation is important for performance, which we’ll discuss next.

Second, notice how sometimes we move in reverse, from the definition of a function back to its ‘unevaluated’ form, as in the final steps in the above proof. We’ll explore this notion of moving backwards in the final part of this series.