Bar recursion: Difference between revisions

Revision as of 03:24, 24 November 2010

Revision as of 23:22, 24 November 2010

Line 5:

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''_''n'' from '''V'''^''i''+''n'' → '''R''' to '''O''' is defined by bar recursion from the functions ''L''_''n'' : '''R''' → '''O''' and ''B'' with ''B''_''n'' : (('''V'''^''i''+''n'' → '''R''') x ('''V'''^''n'' → '''R''')) → '''O''' if:

* ''f''_''n''((λα:'''V'''^''i''+''n'')''r'') = ''L''_''n''(''r'') for any ''r'' along constantenough elementthat ''L''_''n''+''k'' on any extension of ''r'R' equals ''L''_''n''. Asusming ''L'' is a continuous sequence, there must be such ''r'', because a continuous function can use only finitely much data.

* ''f''_''n''(''p'') = ''B''_''n''(''p'', (λ''x'':'''V''')''f''_''n''+1(cat(''p'', ''x''))) for any ''p'' in '''V'''^''i''+''n'' → '''R'''.

Line 12:

(This definition is based on the one in <ref>{{cite journal|authors=Martín Escardó, Paulo Oliva|title=Selection functions, Bar recursion, and Backwards Induction|journal=Math. Struct. in Comp.Science|url=http://www.cs.bham.ac.uk/~mhe/papers/selection-escardo-oliva.pdf}}</ref>.)

Provided that for every constantsufficiently long function (λα)''r'' of type '''V'''^''i'' → '''R''', there is some ''n'' with ''L''_''n''(''r'') = ''B''_''n''((λα)''r'', (λ''x'':'''V''')''L''_''n''+1(''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 constantsufficiently 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 though a constantsufficiently long node: the same requirement that is needed to invoke a bar induction.

<ref>{{cite book|authors=[[Jeremy Avigad]], [[Solomon Feferman]]|chapter=VI: Godel's functional ("Dialectica") interpretation|title=''Handbook of Proof Theory''|editor=[[S. R. Buss]]|year=1999|url=http://math.stanford.edu/~feferman/papers/dialectica.pdf}}</ref>