Thinking that EVAL is a function is a type error. It is the trap of the ``metacircular evaluator.'' People in this course are falling into that trap about the lambda calculus, thinking that LT is the same thing as a subclass of the ML functions. But LT is just ``syntax.'' To make sure you do not make the mistake, I will say some ``shocking'' things that are consistent with the type theory we have been using.
Possibility 1: Recall that in our type theory are the computable functions from
to
. I claim that we can imagine this is an
uncountable type.
Possibility 2: Church's Thesis is false.
You might object that you can prove that is countable; name let
be a list of
all ML programs. Let
be the sublist of those whose
type is
. This sublist is countable and
is the set we want.
But notice that this argument is just like the following one - a
metamathematical argument. Consider the set of all
functions from to
. Let
be all names of objects in our
theory of mathematics (say ZF). Let
be the subset
of those which name functions from
to
.
You reply that this argument assumes that all functions can be named
which is not in fact the case. I claim that the same mistaken
assumption was made in the enumeration . It might
be false that all computable functions can be named in ML. Perhaps no
fixed computation system is enough. Also note that by the
Lowenheim-Skolem Theorem, ZF has a countable model. In that model
is countable.
Church's Thesis
Notice that Church's Thesis says that the effectively computable
functions from to
are equal to the Turing
computable ones. This notion of effective computability is a concept
of mathematics. As such it has been axiomatized or studied
intuitively. Such studies need not adopt axioms consistent with
Church's Thesis, and indeed some computability theories contradict the
Extended Church's Thesis which says that the effectively computable
partial functions from
to
are the partial
(Turing) computable functions. Call this the ECT. We will show later
how easy it is to contradict it (indeed Nuprl does).
In reply to Possibility 2, you might reply that we know from
computability theory that any computation system will be equivalent to
ML because ML is universal. I claim that is an additional
assumption that we did not make explicitly as an axiom of type theory.
It is a metamathematical principle, not a mathematical one. It
is like the belief that any function can
be defined in ZF. This is not a widely held belief because we can
imagine new ways of defining functions. We do not want to close
or limit our system of all functions for obvious reasons.
One must ask them why we would want to close our system of computable functions. If we add a limiting assumption about all computable functions might prevent us from using out theory in places where it is applicable. Notice that such an assumption is negative, it says what cannot happen. It allows us to prove certain negative results because we have limited the notion of all. The theories of computability in mathematics as opposed to logic have not done that.