Turing-completeness of Real PCF

A Turing-completeness result for Real PCF is proved in [26]. It says that every computable mathematical entity in the universe of discourse of Real PCF is denoted by at least one program. Thus, one can be reassured that no relevant construction has been unadvertly omitted from the language. Of course, for efficiency or simplicity reasons, one can introduce more constructions, as it is done in [47].

An invariance result was also proved. Essentially, it shows that one hasn't made any mistake in the choice of the effective presentation of the interval domain. It was previously proved by Kanda and Park in 1980 that in general it is possible to effectively present the same domain in different ways that give different sets of computable elements [53,32]. One thus wonders whether the standard presentation of the interval domain, namely Cantor's enumeration of the rational intervals, is a good choice, or whether there can be cleverer choices that give more computable elements. Let's say that an effective presentation is reasonable if it is makes the four basic operations computable and the inequality relation semidecidable. Cantor's presentation is certainly reasonable in this sense. But can we say more? It is proved that any two reasonable effective presentations are equivalent, in the sense that one can effectively translate between them.