<p>The proof is hidden somewhere in Troelstra and van Dalen, Constructivism in mathematics, volume 2, I suppose. More likely, it can be found in <a href="http://books.google.si/books?id=cYcn1-6LP6oC&amp;lpg=PA443&amp;ots=B3xh-VrRsQ&amp;dq=troelstra%20investigations&amp;hl=en&amp;pg=PP1#v=onepage&amp;q=troelstra%20investigations&amp;f=false" rel="nofollow">Troelstra's investigations</a>, if you can lay your hands on it.</p>

<p>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.</p>

<p>See also M. Escardo, T. Streicher: <a href="http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.9.1915" rel="nofollow">In domain-realizability not all functionals are continuous</a>, published in <a href="http://onlinelibrary.wiley.com/doi/10.1002/1521-3870%28200210%2948:1+%3C41%3a%3aAID-MALQ41%3E3.0.CO;2-V/abstract" rel="nofollow">Mathematical Logic Quarterly, volume 48, issue Supplement 1, pages 41-44, 2002</a>.</p>

CC BY-SA 3.0
2011-07-25T06:53:05.547Z
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.
Andrej Bauer
CC BY-SA 3.0
2011-07-25T08:28:13.837Z
Thanks! What is the $AC_{2,0}$ axiom?
Neel Krishnaswami
CC BY-SA 3.0
2011-07-25T19:33:19.027Z
$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})$.
Andrej Bauer
CC BY-SA 3.0
2011-07-27T19:22:02.273Z
Ok, here's half of the proof: http://math.andrej.com/2011/07/27/definability-and-extensionality-of-the-modulus-of-continuity-functional/
Andrej Bauer
CC BY-SA 3.0
2011-07-22T14:51:11.340Z
2011-07-22T14:51:11.340Z
Andrej Bauer
<p>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}}$</p>

<p>Andrej Bauer has written <a href="http://math.andrej.com/2006/03/27/sometimes-all-functions-are-continuous/" rel="nofollow">a very nice blog post</a> 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.</p>

<p>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.</p>

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

<pre><code>let modulus f xs =
  let r = ref 0 in
  let ys = fun i -&gt; (r := max i !r; xs i) in 
    f ys;
    !r
</code></pre>

<p>Of course, the <code>ys</code> 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 <em>extensionally</em> pure. I work on (among other things) higher-order imperative programming, and am designing type theories which could classify this as a pure function. </p>

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

<pl.programming-languages><lambda-calculus><denotational-semantics><computing-over-reals>
Reference for the undefinability of modulus of continuity functional in PCF?
Neel Krishnaswami
# Reference for the undefinability of modulus of continuity functional in PCF?

(Asked by: username_0 on 2011-07-22)

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}}$
username_1 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.

**Tags:** pl.programming-languages, lambda-calculus, denotational-semantics, computing-over-reals


---

## 1 answers

### Answer by username_1 on 2011-07-22. Score: 4 | Accepted answer

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](http://books.google.si/books?id=cYcn1-6LP6oC&lpg=PA443&ots=B3xh-VrRsQ&dq=troelstra%20investigations&hl=en&pg=PP1#v=onepage&q=troelstra%20investigations&f=false), 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](http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.9.1915), published in [Mathematical Logic Quarterly, volume 48, issue Supplement 1, pages 41-44, 2002](http://onlinelibrary.wiley.com/doi/10.1002/1521-3870%28200210%2948:1+%3C41%3a%3aAID-MALQ41%3E3.0.CO;2-V/abstract).

> **Comments:**
> **username_1**: 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.  
> **username_0**: Thanks! What is the $AC_{2,0}$ axiom?  
> **username_1**: $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})$.  
> **username_1**: Ok, here's half of the proof: http://math.andrej.com/2011/07/27/definability-and-extensionality-of-the-modulus-of-continuity-functional/  

---

