Bar recursion is a generalized form of recursion developed by C. Spector in his 1962 paper. It is related to

bar induction Bar induction is a reasoning principle used in intuitionistic mathematics, introduced by L. E. J. Brouwer. Bar induction's main use is the intuitionistic derivation of the fan theorem, a key result used in the derivation of the uniform continuity ...

in the same fashion that primitive recursion is related to ordinary

induction Induction, Inducible or Inductive may refer to: Biology and medicine * Labor induction (birth/pregnancy) * Induction chemotherapy, in medicine * Induced stem cells, stem cells derived from somatic, reproductive, pluripotent or other cell t ...

, or transfinite recursion is related to

transfinite induction Transfinite induction is an extension of mathematical induction to well-ordered sets, for example to sets of ordinal numbers or cardinal numbers. Its correctness is a theorem of ZFC. Induction by cases Let P(\alpha) be a property defined for a ...

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 In formal language, formal language theory and computer programming, string concatenation is the operation of joining character string (computer science), character strings wikt:end-to-end, end-to-end. For example, the concatenation of "sno ...

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.) 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.

References

Recursion {{mathematics-stub