Bar recursion

Bar recursion is a generalized form of recursion developed by 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. 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 a constant element of R.
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 in ^[2].)

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 (ed.). Recursive Function Theory: Proc. Symoposia in Pure Mathematics. Vol. 5. American Mathematical Society. pp. 1–27.
^ "Selection functions, Bar recursion, and Backwards Induction" (PDF). Math. Struct. in Comp.Science. {{cite journal}}: Unknown parameter |authors= ignored (help)

[1] 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 (ed.). Recursive Function Theory: Proc. Symoposia in Pure Mathematics. Vol. 5. American Mathematical Society. pp. 1–27.

[2] "Selection functions, Bar recursion, and Backwards Induction" (PDF). Math. Struct. in Comp.Science. {{cite journal}}: Unknown parameter |authors= ignored (help)

[1]

[2]