Content deleted Content added
→Technical Definition: connect to bar induction. |
→Technical Definition: more info. |
||
Line 13:
Provided that for every constant 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 constant 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 though a constant node: the same requirement that is needed to invoke a bar induction.
==References==
| |||