Mathematics and Computation

A blog about mathematics for computers

Definability and extensionality of the modulus of continuity functional

In an earlier post I talked about the modulus of continuity functional, where I stated that it cannot be defined without using some form of computational effects. It is a bit hard to find the proof of this fact so I am posting it on my blog in two parts, for Google and everyone else to find more easily. In the first part I show that there is no extensional modulus of continuity. In the second part I will show that every functional that is defined in PCF (simply-typed $\lambda$-calculus with natural numbers and recursion) is extensional. 

The original reference for the first part is Troelstra and van Dalen, Constructivism in mathematics, volume 2, Sections 9.6.10 and 9.6.11, page 500. I transformed the proof to make the main idea a bit more transparent.

Define the finite type hierarchy $N_0, N_1, N_2, \ldots$ over the natural numbers $\mathtt{nat}$ by $$N_0 = \mathtt{nat}$$ and $$N_{k+1} = N_k \to \mathtt{nat}.$$ The elements of $N_k$ are known as the type $k$ functionals. Let us keep the exact meaning of $\mathtt{nat}$ and $\to$ a bit unspecified. We might interpret $\mathtt{nat}$ as the set of natural numbers, or as a domain, or as a datatype in a programming language. We require that $\mathbb{N} \subseteq N_0$, i.e., each number has a representation, but there might be extra elements in $\mathtt{nat}$, such as the undefined value $\perp$. The arrow $\to$ may represent the function type in a programming language, or an exponential in a cartesian-closed category. We will make things precise when we need to.

For each $k$ we define the (hereditarily) total functionals $T_k$ by $T_0 = \mathbb{N}$ and
$$T_{k+1} = \lbrace f \in N_{k+1} \mid \forall x \in T_k . f x \in T_0 \rbrace.$$
We call $T_0, T_1, T_2, \ldots$ the total hierachy derived from $N_0, N_1, N_2, \ldots$. When $N_k = T_k$ for all $k$, we say that the hierarchy $N_0, N_1, N_2, \ldots$ is total.

We also need the notion of extensionality. For each $k$ define the relation $\approx_k$ on $T_k$ by
$$n \approx_0 m \iff n = m$$
and
$$f \approx_{k+1} g \iff \forall x, y \in T_k . x \approx_k y \Rightarrow f(x) = g(y).$$
It can be shown easily that $\approx_k$ is symmetric and transitive, but it need not be reflexive. We say that $f \in N_k$ is extensional when $f \approx_k f$.

After this barrage of definitions some examples will hopefully make things a bit clearer. It is easy to come up with non-total functions, just write down something that cycles. A total function which is not extensional would be the following type 3 functional u, implemented in ocaml:

let u f =
  let k = ref 0 in
  let a n = (k := 1 ; 0) in
    ignore (f a) ;
    !k

The functional u returns 1 if its argument f evaluates its argument, and 0 otherwise. It is not extensional:

# u (fun a -> 0) ;;
- : int = 0
# u (fun a -> 0 * a 0) ;;
- : int = 1

As you can see, u uses local references. Exercise: write a total non-extensional functional using some other computational effect, such as exceptions or continuations.

To avoid writing down lots of ugly types, we preassign types to the following variables:

We need one further piece of notation. Given a total function $\alpha$, let $\overline{\alpha}(k) = [\alpha(0), \alpha(1), \ldots, \alpha(k-1)]$ be the finite list of the first $k$ values of $\alpha$.

A total type 2 functional $F$ is continuous at a total $\alpha$ if the value $F(\alpha)$ depends only on a finite prefix $\overline{\alpha}(k)$: $$\forall \beta \in T_1 . \overline{\beta}(k) = \overline{\alpha}(k) \Rightarrow F(\alpha) = F(\beta).$$
You should convince yourself that this definition of continuity coincides with the usual one for metric spaces if we equip $\mathbf{N}$ with the usual metric $d(i,j) = |i - j|$ and $T_1$  with the comparison metric $$d(\alpha, \beta) = 2^{-\min \lbrace k \mid \alpha(k) \neq \beta(k) \rbrace}.$$ We would expect every computable total functional to be continuous because, intuitively speaking, in order for an algorithm to compute $F(\alpha)$ in finitely many steps it can only inspect finitely many values of $\alpha$. Of course, this assumes that an algorithm cannot do anything other than test $\alpha$ at various values. There are theorems in computability theory which say that, provided $F$ is extensional (see below), an algorithm cannot really do much else, even if it has the source code of $\alpha$ at its disposal. (Exercise: which theorems?)

To keep things simple we shall concentrate on continuity at the zero sequence $o = \lambda n . 0$. Thus a functional $F$ is continuous at $o$ if there exists $k$ such that $\forall \beta \in T_1. \overline{\beta}(k) = \overline{o}(k) \Rightarrow F(\beta) = F(o)$. We say that $k$ is a modulus of continuity for $F$ at $o$.

It is natural to ask whether we can compute a modulus of continuity $k$ from the total functional $F$, i.e., whether there is a modulus of continuity functional $\Phi$ of type 3 such that $$\forall F \in T_2. \forall \beta \in T_1. \overline{\beta}(\Phi(F)) = \overline{o}(\Phi(F)) \Rightarrow F(\beta) = F(o).$$ The existence of $\Phi$ implies that all type 2 functionals are continuous. So clearly we cannot expect to have one in a setting where discontinuous functional can be defined, such as the category of sets.

But how about defining $\Phi$ in a programming language? Well, you can do it in ocaml by using local references:

let phi f =
  let k = ref (-1) in
  let o i = (k := max !k i ; 0) in
    ignore (f o) ;
    !k + 1

We expect phi to compute a modulus of continuity if f is extensional, but I would really like to see a carefully written proof of this fact.

The modulus of continuity phi defined above is not extensional, since it returns different values for extensionally equal functionals:

# phi (fun alpha -> 0) ;;
- : int = 0
# phi (fun alpha -> 0 * alpha 41) ;;
- : int = 42

Can we have an extensional modulus of continuity? Suppose $\Psi$ were one. Let $n = \Psi (\lambda \alpha . 0)$ and consider the type 2 functional $H$ defined by
$$H(\beta) = \Psi (\lambda \alpha . \beta(\alpha(n))).$$
Because $\lambda \alpha . 0$ is extensionally equal to $\lambda \alpha . o(\alpha(n))$ we get by extensionality of $\Psi$ that
$$H(o) = \Psi(\lambda \alpha . o (\alpha(n))) = \Psi (\lambda \alpha . 0) = n.$$
On the other hand, if $\beta \neq o$ then the value $\beta(\alpha(n))$ cannot be determined by looking at $\alpha(0), \ldots, \alpha(n-1)$, therefore $H(\beta) = \Psi (\beta (\alpha (n))) > n$. This means that $H$ is not continuous at $o$, which contradicts existence of $\Psi$. We have shown:

Theorem: There is no extensional modulus of continuity functional.

The consequence of this is that we cannot define the modulus of continuity functional in a programming language in which all total functionals are extensional. Next time we will see that PCF is such a language.

Comments

Bob Harper

Hi Andrej,

It seems that the modulus of continuity is a property of the algorithm, not the function, so why would one even expect that there is a extensional modulus of continuity functional? Your proof shows that it doesn't exist, but it doesn't even seem plausible on the face of it that it would exist. Or else I am confused or wrong about something.

Andrej Bauer

@Bob: you are not confused, and I do not find it surprising that you do not find it suprising that there is no modulus of continuity. Nevertheless, non-existence of an extensional modulus of continuity still deserves a proof, or do you think the average person in Wean Hall (or wherever you people live these days) could come up with a proof on the spot? Anyhow, this is just a first step to the thing I really want to prove, namely that a modulus of continuity cannot be defined in a pure functional language (PCF).

Andrej Bauer

By the way, I really would like to see a careful proof of the fact that the functional phi is a modulus of continuity (in PCF with local references or some such).

Dawid Toton

The definition of (hereditarily) total functionals doesn't typecheck. I believe it should have $f \in N_{k+1}$. Also, the definition of $\approx_k$ should probably have $g(y)$ at the end.

Andrej Bauer

@David: Fixed, thanks!

Martin Escardo

Nice post, Andrej. Of course, you know that the extensional modulus of uniform continuity of a function $(\mathbb{N} \to 2) \to \mathbb{N}$ exists and can be defined in PCF as shown by Berger in 1990, and depends on the function rather than the algorithm, where $2 = \lbrace 0,1 \rbrace$. This has been vastly generalized in recent years, with a complete answer of when the modulus of uniform continuity exists and can be defined in PCF (even without parallel features). I like to see what you explain in your post as simply saying that the modulus of continuity is not continuous. Or, more precisely, no extensional modulus of continuity functional can be continuous. I am looking forward to the second part of the post.

Andrej Bauer

@Martin: Thanks for commenting on the modulus of continuity for the Cantor space. I wanted to mention that in my post, but then forgot about it. I am still debating whether the second part should go via domain theory or via operational semantics.

Martin Escardo

Forget the debate. Go for both!

How to comment on this blog: At present comments are disabled because the relevant script died. If you comment on this post on Mastodon and mention andrejbauer@mathstodon.xyz, I will gladly respond. You are also welcome to contact me directly.