Are all functions continuous?
Brouwer's statement "all functions are continuous" can be formulated without reference to topology as follows.
Definition: A functional
f : (N → N) → Nis continuous at
a : N → Nwhen there exists
m : Nsuch that, for all
b : N → N, if
∀ k < m, a k = b kthen
f a = f b.
This says that the value of
f a depends only on the initial segment
a 1, ...,
The statement all functionals are continuous everywhere is valid in various models of intuitionistic mathematics, such as Kleene's number realizability and Kleene's function realizability. We can ask whether the statement is realized in any given functional programming language.
Definition: A modulus of continuity is a functional
μ : ((N → N) → N) → (N → N) → Nsuch that, for all
f : (N → N) → Nand
a, b : N → N, if
∀ k < μ f a . a k = b kthen
f a = f b.
μ f a computes how much of
a is needed to compute
Implementing the modulus of continuity
It is impossible to implement
μ in PCF and therefore also in Haskell. We necessarily
need additional abilities that let
μ inspect the workings of
f. Here are a few attempts.
int is the type of natural numbers
type nat = int
ML with references
Consider ML with references (and no other features). Then a possible
let mu_ref f a = let k = ref 0 in let a' n = (k := max !k n; a n) in f a' ; !k
- We should at least require that
fbe hereditarily total (it terminates on total
fuse its own local references? If yes, then we can break
mu_ref. If no, is that not too restrictive?
- How do we formulate the exact preconditions on
- What is the theorem that needs to be proved, and how is it proved?
ML with exceptions
With exceptions (and no other features) we can do it as follows:
exception Abort let mu_exc f x = let rec search k = try let y n = (if n < k then x n else raise Abort) in f y ; k with Abort -> search (k+1) in search 0
- What if
Abort? May it do so? What is the contract on
- Would local exceptions help? If so, can
fuse its own local exceptions?
In Haskell we could do everything inside a fixed monad. This is still not entirely easy, even if we figure out what it means for
fto be "pure" (whatever that means).
Moving to a total language is probably helpful. However, keep in mind that
μdoes not exist in pure λ-calculus, so straight Agda or some such is out of the question.
Other effects can be used to implement a candidate
μ, but it seems like they should be local (local references, local exceptions, delimited control) or else
fhas access to them.
A note on rigor
The proofs should be actual proofs, not hand-wavy arguments.