Reference for the undefinability of modulus of continuity functional in PCF?

Question

Can someone point me to the reference for the non-definability of the modulus of continuity functional in PCF? $\newcommand{\N}{\mathbb{N}}$ $\newcommand{\bool}{\mathsf{bool}}$

Andrej Bauer has written a very nice blog post exploring some of the issues in more detail, but I'll summarize just a bit of his post to lend some context to this question. The Baire space $B$ is the set of natural number sequences, or equivalently the set of functions from naturals to naturals $\N \to \N$. For this question, we will restrict our attention only to the streams which are computable.

Now, a function $f : B \to \bool$ is continuous if for every $xs \in B$, the value of $f(xs)$ depends only a finite number of the elements of $xs$, and it's computably continuous if we can actually compute an upper bound on how many elements of $xs$ are needed. In some models of computation, it's actually possible to write a program $\mathsf{modulus} : (B \to \bool) \to B \to \N$ which takes a computable function on the Baire space and an element of the Baire space, and gives back the upper bound on the number of elements of the stream.

One trick for implementing this is to use local storage to record the maximum index into the stream seen:

let modulus f xs =
  let r = ref 0 in
  let ys = fun i -> (r := max i !r; xs i) in 
    f ys;
    !r

Of course, the ys argument is no longer a purely functional program. My interest in this program comes from the fact that it only makes use of local store, and is therefore extensionally pure. I work on (among other things) higher-order imperative programming, and am designing type theories which could classify this as a pure function.

There are more practical examples as well, involving things like memoization and connection pooling, but I find this a particularly beautiful example.

Answer 1

The proof is hidden somewhere in Troelstra and van Dalen, Constructivism in mathematics, volume 2, I suppose. More likely, it can be found in Troelstra's investigations, if you can lay your hands on it.

It goes like this. Suppose we could define the modulus of continuity in typed $\lambda$-calculus with fixpoint operators. Then we could interpret it in a domain-theoretic realizaiblity model, for example in $\mathsf{PER}(\mathcal{P}\omega)$ where $\mathcal{P}\omega$ is Scott's graph model. In this model the choice principle $AC_{2,0}$ is valid. But it is known that $AC_{2,0}$ together with extensionality of functions (which holds in every realizability model) is incompatible with existence of modulus of continuity. If I get a moment, I will fill in the details later.

See also M. Escardo, T. Streicher: In domain-realizability not all functionals are continuous, published in Mathematical Logic Quarterly, volume 48, issue Supplement 1, pages 41-44, 2002.