Bar recursion: Difference between revisions

Revision as of 04:33, 23 February 2013

Latest revision as of 14:54, 10 July 2025

(8 intermediate revisions by 8 users not shown)

Line 1:

{{Short description|Generalized form of recursion}}

'''Bar recursion''' is a generalized form of recursion developed by C. Spector in his 1962 paper.<ref>{{cite book|author=C. Spector|chapter=Provably recursive functionals of analysis: a consistency proof of analysis by an extension of principles in current intuitionistic mathematics|editor=F. D. E. Dekker|title=Recursive Function Theory: Proc. SymoposiaSymposia in Pure Mathematics|volume=5|pages=1–27|year=1962|publisher=[[American Mathematical Society]]}}</ref> It is related to [[bar induction]] in the same fashion that [[primitive recursion]] is related to ordinary [[Mathematical induction|induction]], or [[transfinite recursion]] is related to [[transfinite induction]].

==Technical Definitiondefinition==

Let '''V''', '''R''', and '''O''' be [[type theory|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''. AsusmingAssuming ''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]] 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 inby Escardó and Oliva.<ref>{{cite journal|authorsauthor=Martín Escardó, |author2=Paulo Oliva|title=Selection functions, Bar recursion, and Backwards Induction|journal=Math. Struct. in Comp.Science|url=http://www.cs.bham.ac.uk/~mhe/papers/selection-escardo-oliva.pdf}}</ref>)

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 thoughthrough 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]]s.<ref>{{cite book|authorsauthor=[[Jeremy Avigad]],|author-link=Jeremy [[Avigad|author2=Solomon Feferman|author2-link=Solomon Feferman]]|chapter=VI: Gödel's functional ("Dialectica") interpretation|title=''Handbook of Proof Theory''|editor=[[S. R. Buss]]|editor-link=S. R. Buss|year=1999|url=http://math.stanford.edu/~feferman/papers/dialectica.pdf}}</ref>

==References==

Line 23 ⟶ 24:

{{DEFAULTSORT:Bar Recursion}}

[[Category:Recursion]]

{{mathematics-stub}}