UPDF AI

On bar recursive interpretations of analysis

Thomas Powell

2013 · DBLP: phd/ethos/Powell13
13 Citations

TLDR

It is proved that modified bar recursion (in the form of the implicitly controlled product of selection functions), open recursion, update recursion and the Berardi-BezemCoquand realizer for countable choice are all primitive recursively equivalent in the model of continuous functionals.