Bar recursion: Difference between revisions

Revision as of 10:23, 22 December 2011

Revision as of 15:32, 24 September 2012

Line 1:

'''Bar recursion''' is a generalized form of recursion developed by 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. Symoposia 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 Definition==

Line 10:

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 .<ref>{{cite journal|authors=Martín Escardó, 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.