Content deleted Content added
No edit summary |
No edit summary |
||
Line 3:
==Technical Definition==
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.
| |||