Axiomatizing computability in order to prove Church's thesis

5 views
Skip to first unread message

tc...@lsa.umich.edu

unread,
Nov 17, 2002, 1:53:55 PM11/17/02
to
[Note cross-posting.]

Recently there was some discussion on comp.theory as to whether there
exist axioms for the notion of a "computable function" from which one
can prove that the computable functions are the recursive functions,
instead of simply assuming Church's thesis outright. (See

http://groups.google.com/groups?selm=aqml12%24t7t%241%40galois.mit.edu

for a slightly more detailed explanation of the above question.)

Browsing in the bookstore today, I saw an interesting sentence in
Shoenfield's little book _Recursion_Theory_. Shoenfield said that
there has been intensive effort on the above question, but that there
has been only limited success. Unfortunately he gave no specific
references. Any guesses as to what Shoenfield was referring to?

Barb Knox made one suggestion: `How about "reverse engineering" Scott's
denotational semantics for the lambda calculus to produce a set of axioms
that generate an equivalent model?' Has anyone worked this out in detail?
--
Tim Chow tchow-at-alum-dot-mit-dot-edu
The range of our projectiles---even ... the artillery---however great, will
never exceed four of those miles of which as many thousand separate us from
the center of the earth. ---Galileo, Dialogues Concerning Two New Sciences

William Mueller

unread,
Nov 18, 2002, 12:50:39 PM11/18/02
to
> Browsing in the bookstore today, I saw an interesting sentence in
> Shoenfield's little book _Recursion_Theory_. Shoenfield said that
> there has been intensive effort on the above question, but that there
> has been only limited success. Unfortunately he gave no specific
> references. Any guesses as to what Shoenfield was referring to?

I was Shoenfield's graduate student at Duke. What he was referring to was
mostly his own work. I know this, because I asked him the same question.
Unfortunately, the work was never completed before he passed away, and he
did not publish it. He had *very* high standards for what he put into print.

Shoenfield was interested in the axiomatic approach taken by Kurt Mehlhorn
in the second half of his paper: Polynomial and abstract subrecursive
classes; Journal of Computer and System Sciences, 12:147-178, 1976. He had
me working on an extension of this system in my dissertation. I know that he
was interested in doing something similar for general complexity classes.

I'm not aware of anyone else having taken this approach since Mehlhorn, but
there may very well be recent papers of which I am unaware.

Anything less than a simple, extremely elegant system would not have been of
much interest to Shoenfield. If he had partial results in this direction,
I'm afraid we will never know. Too bad. Everything Shoenfield did write had
crystalline clarity.

Bill Mueller
The MathWorks


Charlie-Boo

unread,
Nov 18, 2002, 10:41:18 PM11/18/02
to
> Recently there was some discussion on comp.theory as to whether there
> exist axioms for the notion of a "computable function" from which one
> can prove that the computable functions are the recursive functions,
> instead of simply assuming Church's thesis outright.
>
> Browsing in the bookstore today, I saw an interesting sentence in
> Shoenfield's little book _Recursion_Theory_. Shoenfield said that
> there has been intensive effort on the above question, but that there
> has been only limited success.

In http://www.arxiv.org/html/cs.lo/0003071 I give a small set of
formal axioms and rules of inference (they are represented by
predicate calculus wffs) from which I derive a number of theorems of
the Theory of Computation, including the unsolvability of the halting
problem and the membership problem, and the fact that the set of
programs that halts yes on itself is recursively enumerable.

I also show how these same rules can be used to solve the problem of
program synthesis, both of mathematical programs and of database
programs.

This is further developed in
http://www.mathpreprints.com/math/Preprint/CharlieVolkstorf/20021008.1/1
.

Charlie Volkstorf
Cambridge, MA

Cagdas Ozgenc

unread,
Nov 19, 2002, 6:46:45 AM11/19/02
to
You are curious all of a sudden. Have I done you a bad thing by infecting
your mind with this stuff :) ? Unfortunately, I was too busy to investigate
the issue further, but I will read the discussions if people happen to
contribute.

<tc...@lsa.umich.edu> wrote in message news:ar8ok3$9g2$1...@galois.mit.edu...

Mike Stannett

unread,
Nov 21, 2002, 10:07:13 PM11/21/02
to
I've come to this discussion late, so sorry if I've misunderstood somewhere
along the way.

There are an increasing number of examples of 'physically reasonable'
systems whose behaviour is known to be non-recursive, so the idea that you
could prove Church's Thesis (at least, as outlined in the link referred to
in the original post, below) would need serious emendation. Examples include
analog recursive neural networks (Siegelmann et al, last few years), but go
right back to the 1960s (Pour-El and Richard demonstrated a solution to the
wave equation, with recursive initial conditions, which becomes
non-recursive at a recursively identified location after a recursive amount
of time).

At the very least you'd have to deny the Axiom of Choice ... here's why.

This is a non-recursive system anyone can build with access to school-lab
radioactive supplies; it is guaranteed to generate a truly-random integer of
unbounded size, so cannot be recursive by Konig's Lemma (the program tree,
which is finitely branching, would have infinitely many leaves, one for each
potential outcome, yet would not contain an infinite chain, because such a
chain would violate the guarantee of termination). To overcome this you need
to "remove" Konig's Lemma, i.e. (since this is equiv to AC in ZF) deny AC.

To build the system you take a radioactive sample and a container. Ensure
the sample is large enough that when all of it has decayed the weight loss
will be easily measurable. Set a threshold value of half this amount. Weight
until the threshold amount of mass has been lost; the number of complete
seconds that have passed so far is your random integer. You'd *expect* the
threshold to be crossed after just one half-life, but there's nothing in
physics that says this *has* to happen. In theory, the unstable particles
could take as long as they wanted before actually decaying. Consequently,
any integer could potentially be returned by the device. On the other hand,
most theories of physics assume that every unstable particle must eventually
decay. Consequently, the threshold *will* eventually be passed, it's just
you can't predict when this will happen.

(There are philosophical niceties about the validity of physicists'
assumptions that particles eventually decay, so while my argument above is
(I hope) compelling, it is not absolutely positive - but then nothing is.
This will be appearing in a paper in Minds and Machines later this year, in
a special issue on Hypercomputation).

Mike.


<tc...@lsa.umich.edu> wrote in message news:ar8ok3$9g2$1...@galois.mit.edu...

Reply all
Reply to author
Forward
0 new messages