Brouwer's statement "all functions are continuous" can be formulated without reference to topology as follows.
Definition: A functional
f : (N → N) → N
is continuous ata : N → N
when there existsm : N
such that, for allb : N → N
, if∀ k < m, a k = b k
thenf a = f b
.
This says that the value of f a
depends only on the initial segment a 0
, a 1
, ...,
a (m-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) → N
such that, for allf : (N → N) → N
anda, b : N → N
, if∀ k < μ f a . a k = b k
thenf a = f b
.
Essentially μ f a
computes how much of a
is needed to compute f a
.
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.
Pretend that int
is the type of natural numbers
type nat = int
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
However:
- We should at least require that
f
be hereditarily total (it terminates on totala
). - Can
f
use its own local references? If yes, then we can breakmu_ref
. If no, is that not too restrictive? - How do we formulate the exact preconditions on
f
anda
? - What is the theorem that needs to be proved, and how is it proved?
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
However:
- What if
f
catchesAbort
? May it do so? What is the contract onf
? - Would local exceptions help? If so, can
f
use 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
f
to 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 elsef
has access to them.
The proofs should be actual proofs, not hand-wavy arguments.