Content deleted Content added
m →Technical Definition: typo and general fixes, replaced: pass though → pass through using AWB |
Clarityfiend (talk | contribs) m →Technical Definition: lowercase |
||
Line 1:
'''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. Symposia 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
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''<sub>''n''</sub> from '''V'''<sup>''i''+''n''</sup> → '''R''' to '''O''' is defined by bar recursion from the functions ''L''<sub>''n''</sub> : '''R''' → '''O''' and ''B'' with ''B''<sub>''n''</sub> : (('''V'''<sup>''i''+''n''</sup> → '''R''') x ('''V'''<sup>''n''</sup> → '''R''')) → '''O''' if:
| |||