Bar recursion
Bar recursion is a generalized form of recursion developed by C. Spector in his 1962 paper. 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" from V → R to O is defined by bar recursion from the functions "L" : R → O and "B" with "B" : ((V → R ) x (V → R)) → O if: Here "cat" is the concatenation function, sending "p", "x" to the sequence which starts with "p", and has "x" as its last term. Provided that for every sufficiently long function (λα)"r" of type V → R, there is some "n" with "L"("r") = "B"((λα)"r", (λ"x":V)"L"("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.