Bar recursion
Encyclopedia
Bar recursion is a generalized form of recursion developed by 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
.
, and i be any natural number, representing a sequence of parameters taken from V. Then the function sequence f of functions fn from Vi+n → R to O is defined by bar recursion from the functions Ln : R → O and B with Bn : ((Vi+n → R) x (Vn → 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.
(This definition is based on the one in .)
Provided that for every sufficiently long function (λα)r of type Vi → R, there is some n with Ln(r) = Bn((λα)r, (λx:V)Ln+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 though 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.
Bar induction
Bar induction is a reasoning principle used in intuitionistic mathematics, introduced by L.E.J. Brouwer.It is useful in giving constructive versions of classical results.It is based on an inductive argument....
in the same fashion that primitive recursion is related to ordinary induction
Induction
-General use:* Induction , induction of childbirth* Rite of passage** Introduction of an individual into a body such as the armed forces** Formal introduction of a priest into possession of the position to which she or he has been presented and instituted...
, or transfinite recursion is related to transfinite induction
Transfinite induction
Transfinite induction is an extension of mathematical induction to well-ordered sets, for instance to sets of ordinal numbers or cardinal numbers.- Transfinite induction :Let P be a property defined for all ordinals α...
.
Technical Definition
Let V, R, and O be typesType theory
In mathematics, logic and computer science, type theory is any of several formal systems that can serve as alternatives to naive set theory, or the study of such formalisms in general...
, and i be any natural number, representing a sequence of parameters taken from V. Then the function sequence f of functions fn from Vi+n → R to O is defined by bar recursion from the functions Ln : R → O and B with Bn : ((Vi+n → R) x (Vn → R)) → O if:
- fn((λα:Vi+n)r) = Ln(r) for any r long enough that Ln+k on any extension of r equals Ln. Asusming L is a continuous sequence, there must be such r, because a continuous function can use only finitely much data.
- fn(p) = Bn(p, (λx:V)fn+1(cat(p, x))) for any p in Vi+n → R.
Here "cat" is the concatenation
Concatenation
In computer programming, string concatenation is the operation of joining two character strings end-to-end. For example, the strings "snow" and "ball" may be concatenated to give "snowball"...
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 .)
Provided that for every sufficiently long function (λα)r of type Vi → R, there is some n with Ln(r) = Bn((λα)r, (λx:V)Ln+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 though 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.