Realizers

A function 32#32 realizes a function 33#33 if

34#34

as illustrated in the following diagram:

35#35

Of course, here we are interested in computable realizers. The realizer lives at the operational level, whereas the function that it realizes lives at the denotational level. As we discussed above, a necessary (but not sufficient) condition for a function 32#32 being computable is that finite subsequences of 36#36 depend only on finite subsequences of 11#11. In this case we say that 22#22 is of finite character. We state as a proposition a fact that we already discussed in the previous chapter (where D is topologized as in Chapter 5).

Proposition 6.1   A function 32#32 is of finite character iff it is continuous.

This is the first link between computability and continuity, at an operational level. To get a link at the denotational level, we state the following.

Proposition 6.2   The surjection 37#37 is a topological quotient map.

38#38
By a basic property of topological quotient maps, we get the following.

Corollary 6.3   A function 2#2 with a realizer 32#32 of finite character is necessarily continuous.

Unfortunately, the converse is not true.

Proposition 6.4   There are continuous functions 2#2 with no realizer of finite character, for example f(x)=3x/10.

39#39
This is of course independent of the choice of a base--but different counter-examples are needed for different bases. The argument of Proposition 6.4 is a topological version of the computational argument already given in Chapter 3.