For we write to mean and to mean . “Converges,” “Diverges.”

, .

If we say if

(Symbol soup for they agree on convergence, and value if converges. Funext for partials.)

Recursive partial functions

Some -ary partial functions are “clearly” effectively calculable (you could imagine a computer doing these easily).

• Composition: if we already have two effectively calculable programs (functions), then composing them is trivial.

• For , let be . Let be . ( for successor.)

• For , let be the “-th projection”

• For , , , let

  Here we say is defined by substitution from .

Let be the family of partial functions . An additional rule:

• Recursion: let , . Define by and .

  More generally, for , , , define . For , take , and .

  Here we say that is defined by primitive recursion from and . If , then .

Proof. Use primitive recursion,

⁠ 

In the proof above, explicitly speaking, we chose . The choice of is also clear. Here , so given , a suitable choice is , since .

Beyond just satisfying the symbolic constraints we attempt to give an intuitive explanation for why this is a clear choice. We should interpret the -ary function as the familiar for loop. The first parameters constitute the vector , and the argument can be seen as the loop index . We should view as some immutable auxiliary data that the loop can access throughout its iterations. Indeed, notice that is passed unchanged throughout every recursive step of , , and .

The -ary function can be interpreted as an initial value at , and the -ary function is the loop body. The argument of is some value passed down from the previous iteration of the loop. The way I think about it is that at index of the loop, which is , we can pass on some value to the next iteration . We can therefore access the value passed to us by the previous iteration , which is why .

Once we digest primitive recursion from the for loop perspective, it becomes more palatable as a “primitive” form of recursion. Essentially, instead of a recursive function (in the colloquial sense) being able to arbitrarily call itself in its body, a primitive recursive function can only obtain the value of in its body, and the base case is guaranteed to be when . In this view, and are merely auxiliary functions to make the formalism work out.

Now the choice of is clear. For , we just need a for loop to add to , times. We don’t need the initial input , and we don’t need the index . So we use to choose the prior value of the “loop,” and then we add one to it (via the successor function). The initial value of the loop is clearly itself. Now the function defined by primitive recursion can be interpreted as a for loop with an accumulator variable initialized at , at each following iteration adding to the accumulator, running for a total of times. (The first iteration where is initialized is interpreted as , so the loop adds one to a total of times, computing in the end.)

Primitive recursion for partials: for partial functions , , the function defined by primitive recursion from and is given by

Just means that when working with partials we need to take care of convergence.

• Let , . Define by

  If , we’ll put . Notation: .

  We say that is defined from by minimization.

  In the partial case, for , define by

Equivalently, is recursive iff it can be defined from , , , using finitely many applications of substitution, primitive recursion, and minimization.

Non-mathematical claim: recursive functions are effectively calculable. If you believe in the Church-Turing Thesis, then recursive functions are exactly the functions which can be computed by effective methods (e.g. Python-computation).