Bar recursion

Let V, R, and O be types, and i be any natural number, representing a sequence of parameters taken from V. Then the function sequence f of functions f_n from Vⁱ⁺ⁿ → R to O is defined by bar recursion from the functions L_n : R → O and B with B_n : ((Vⁱ⁺ⁿ → R) x (Vⁿ → R)) → O if:

• f_n((λα:Vⁱ⁺ⁿ)r) = L_n(r) for any r long enough that L_n+k on any extension of r equals L_n. Assuming L is a continuous sequence, there must be such r, because a continuous function can use only finitely much data.
• f_n(p) = B_n(p, (λx:V)f_n+1(cat(p, x))) for any p in Vⁱ⁺ⁿ → R.

Here "cat" is the concatenation function, sending p, x to the sequence which starts with p, and has x as its last term.

(This definition is based on the one by Escardó and Oliva.^[2])

Provided that for every sufficiently long function (λα)r of type Vⁱ → R, there is some n with L_n(r) = B_n((λα)r, (λx:V)L_n+1(r)), the bar induction rule ensures that f is well-defined.

The idea is that one extends the sequence arbitrarily, using the recursion term B to determine the effect, until a sufficiently long node of the tree of sequences over V is reached; then the base term L determines the final value of f. The well-definedness condition corresponds to the requirement that every infinite path must eventually pass through a sufficiently long node: the same requirement that is needed to invoke a bar induction.

The principles of bar induction and bar recursion are the intuitionistic equivalents of the axiom of dependent choices.^[3]