Content deleted Content added
Tom.Reding (talk | contribs) m →Technical Definition: Fix Category:CS1 maint: Uses authors parameter: vauthors/veditors or enumerate multiple authors/editors; WP:GenFixes on, enum'd 3 author/editor WLs, using AWB |
Link suggestions feature: 2 links added. |
||
| (4 intermediate revisions by 4 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. 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:
* ''f''<sub>''n''</sub>((λα:'''V'''<sup>''i''+''n''</sup>)''r'') = ''L''<sub>''n''</sub>(''r'') for any ''r'' long enough that ''L''<sub>''n''+''k''</sub> on any extension of ''r'' equals ''L''<sub>''n''</sub>. Assuming ''L'' is a continuous sequence, there must be such ''r'', because a [[continuous function]] can use only finitely much data.
* ''f''<sub>''n''</sub>(''p'') = ''B''<sub>''n''</sub>(''p'', (λ''x'':'''V''')''f''<sub>''n''+1</sub>(cat(''p'', ''x''))) for any ''p'' in '''V'''<sup>''i''+''n''</sup> → '''R'''.
Line 14 ⟶ 15:
Provided that for every sufficiently long function (λα)''r'' of type '''V'''<sup>''i''</sup> → '''R''', there is some ''n'' with ''L''<sub>''n''</sub>(''r'') = ''B''<sub>''n''</sub>((λα)''r'', (λ''x'':'''V''')''L''<sub>''n''+1</sub>(''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
The principles of bar induction and bar recursion are the intuitionistic equivalents of the axiom of [[dependent choice]]s.<ref>{{cite book|author=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>
Line 23 ⟶ 24:
{{DEFAULTSORT:Bar Recursion}}
[[Category:Recursion]]
{{mathematics-stub}}
| |||