# Bar recursion

**Bar recursion** is a generalized form of recursion developed by C. Spector in his 1962 paper.^{[1]} It is related to bar induction in the same fashion that primitive recursion is related to ordinary induction, or transfinite recursion is related to transfinite induction.

## Technical definition

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**^{i+n} → **R** to **O** is defined by bar recursion from the functions *L*_{n} : **R** → **O** and *B* with *B*_{n} : ((**V**^{i+n} → **R**) x (**V**^{n} → **R**)) → **O** if:

*f*_{n}((λα:**V**^{i+n})*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**^{i+n}→**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**^{i} → **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]}

## References

- ↑ C. Spector (1962). "Provably recursive functionals of analysis: a consistency proof of analysis by an extension of principles in current intuitionistic mathematics". in F. D. E. Dekker.
*Recursive Function Theory: Proc. Symposia in Pure Mathematics*.**5**. American Mathematical Society. pp. 1–27. - ↑ Martín Escardó; Paulo Oliva. "Selection functions, Bar recursion, and Backwards Induction".
*Math. Struct. in Comp.Science*. http://www.cs.bham.ac.uk/~mhe/papers/selection-escardo-oliva.pdf. - ↑ Jeremy Avigad; Solomon Feferman (1999). "VI: Gödel's functional ("Dialectica") interpretation". in S. R. Buss. Handbook of Proof Theory. http://math.stanford.edu/~feferman/papers/dialectica.pdf.

Original source: https://en.wikipedia.org/wiki/Bar recursion.
Read more |