Content deleted Content added
Sammi Brie (talk | contribs) Adding short description: "Generalized form of recursion" |
Link suggestions feature: 2 links added. |
||
Line 4:
==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.
* ''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'''.
| |||