System T and the Product of Selection Functions

25th International Workshop/20th Annual Conference of the EACSL

Martín Escardó1 ; Paulo Oliva2 ; Thomas Powell2 ; 2 Queen Mary University of London

Others  :  http://drops.dagstuhl.de/opus/volltexte/2011/3234/pdf/21.pdf
PID  :  44643

来源: CEUR

【 摘 要 】

We show that the finite product of selection functions (for all finite types) is primitive recursively equivalent to Gödel’s higher-type recursor (for all finite types). The correspondence is shown to hold for similar restricted fragments of both systems: The recursor for type level n+1 is primitive recursively equivalent to the finite product of selection functions of type level n. Whereas the recursor directly interprets induction, we show that other classical arithmetical principles such as bounded collection and finite choice are more naturally interpreted via the product of selection functions.1998 ACM Subject Classification F.1.1 Models of Computation