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
In computability theory, a primitive recursive function is, roughly speaking, a function that can be computed by a computer program whose loops are all "for" loops (that is, an upper bound of the number of iterations of every loop is fixed befor ...
is related to ordinary
induction, or
transfinite recursion
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 ...
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
Type may refer to:
Science and technology Computing
* Typing, producing text via a keyboard, typewriter, etc.
* Data type, collection of values used for computations.
* File type
* TYPE (DOS command), a command to display contents of a file.
* Ty ...
, and ''i'' be any
natural number
In mathematics, the natural numbers are the numbers 0, 1, 2, 3, and so on, possibly excluding 0. Some start counting with 0, defining the natural numbers as the non-negative integers , while others start with 1, defining them as the positive in ...
, 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
In mathematics, a continuous function is a function such that a small variation of the argument induces a small variation of the value of the function. This implies there are no abrupt changes in value, known as '' discontinuities''. More preci ...
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 theory and computer programming, string concatenation is the operation of joining character strings end-to-end. For example, the concatenation of "snow" and "ball" is "snowball". In certain formalizations of concatenati ...
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 choice
In mathematics, the axiom of dependent choice, denoted by \mathsf , is a weak form of the axiom of choice ( \mathsf ) that is still sufficient to develop much of real analysis. It was introduced by Paul Bernays in a 1942 article in reverse mathema ...
s.
References
Recursion
{{mathematics-stub