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;

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.


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.

  • $\begingroup$ I looked it up. It is in Troelstra and van Dalen's "Constructivism in mathematics, volume 2", section 6.10, page 500. I think I will put this up on my blog because it is awfully hard to find. $\endgroup$ – Andrej Bauer Jul 25 '11 at 6:53
  • $\begingroup$ Thanks! What is the $AC_{2,0}$ axiom? $\endgroup$ – Neel Krishnaswami Jul 25 '11 at 8:28
  • $\begingroup$ $AC(X,Y)$ is $(\forall x \in X \exists y \in Y . R(x,y)) \Rightarrow \exists f \in Y^X \forall x \in X . R(x, f(x))$, and then $AC_{2,0}$ is $AC(\mathbb{N}^{\mathbb{N}^\mathbb{N}}, \mathbb{N})$. $\endgroup$ – Andrej Bauer Jul 25 '11 at 19:33
  • $\begingroup$ Ok, here's half of the proof: math.andrej.com/2011/07/27/… $\endgroup$ – Andrej Bauer Jul 27 '11 at 19:22

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.