re: Rado's Sigma and the Halting Problem for Programs

From: Acme Diagnostics (LFinezapthis_at_partpostmark.net)
Date: 08/09/04 

Date: 9 Aug 2004 14:30:10 -0500

"r.e.s." <r.s@ZZmindspring.com> wrote:
>[sci.math added] In a different comp.theory thread,
>"Acme Diagnostics" <LFinezapthis@partpostmark.net> wrote ...
>
>> Is there any *linkable* proof of the Halting Problem for a
>> computer language that does not contrive a logic paradox and
>> require self-reference to make the proof?
>
>> I'm not interested in Turing Machines at all, but only the
>> proof "for a computer language." That distinction is
>> made explicit on this page:
>>
>> http://www.csee.umbc.edu/~squire/cs451_l26.html
>
>I doubt there's a proof that avoids reductio ad absurdum,
>but it's not necessary that the proof rely on programs that
>explicitly "call themselves". Here's an outline of one
>approach ...
>
>First define the halting problem for a given programming
>model M (which is to include i/o conventions) -- this will
>remain imprecise until the model M is fully specified:
>
>Definition. The M-Halting Problem is the question
>"Given an arbitrary M-program P, and arbitrary finite
>input I, does P eventually halt if started with input I?"
>
>If the M-Halting Problem is unsolvable by an M-program,
>a proof might be possible by exploiting the following kind
>of function (again, imprecise until model M is specified):
>
>Definition of the function Sigma_M:
>Suppose there are definitions for program length and
>output size, as well as some fixed standard input.
>Let Sigma_M(n) be the maximum output size among length-n
>M-programs that halt, assuming all programs start with the
>same standard input. (Sigma_M generalizes Rado's Sigma.)
>
>Theorem. If (1) Sigma_M is not M-computable,
> and (2) there exists a universal M-program,
> then no M-program solves the M-Halting Problem.
>-----
>Proof (sketch -- imprecise until model M is specified):
>For reductio ad absurdum, suppose the M-Halting Problem
>is solvable by M-program P. Then from P there can be
>constructed an M-program Q that checks all finitely-many
>length-n M-programs started on the standard input, and
>determines which of these halt. Furthermore, since, by
>(2) there exists a universal M-program, say U, it can be
>incorporated into Q to simulate each of the M-programs
>determined to halt, and to track the maximum output size.
>That is, Q computes Sigma_M(n) for n in N. Since this
>contradicts (1), the supposition (that there exists an
>M-program that solves the M-halting Problem) is false.
>Q.E.D.
>-----
>
>A very detailed simple constructive proof of (1) both for
>TMs and for my favorite "toy" programming model, which I
>call F (it's a BrainF*** deviant ;o), is at
>http://r.s.home.mindspring.com/F/Rado_Sigma.txt
>
>It's amusing that unlike Sigma_TM (i.e. Rado's Sigma,
>for which Sigma(6) > 10**865), Sigma_F instead grows very
>slowly at first -- the first few dozen terms being in the
>pattern 1,1,2,2,3,3,4,4,...-- yet eventually it too grows
>faster than any computable function.
>
>A proof of (2) for the F model is implicit in the program
>that simulates a Turing-complete tag-system, described at
>http://r.s.home.mindspring.com/F/f_tag.txt
>
>(Since F is Turing-complete, (1) & (2) indirectly serve
>to prove that no Turing machine can solve the TM-Halting
>Problem, and also that Sigma_F is not Turing-computable.)
>
>--r.e.s.

I suspect your post is only nominally addressed to me, with
the crosspost and higher math. But thanks anyway. I hoped
a mathematician would have jumped in by now to say that
this represents an alternative proof of the Halting Problem
"for a computer program/language" and possibly explain
why to a non-mathematician. In case that's because anyone
awaits a reply from me, I'm getting myself out of the way.

I (trivially) could not find a computer program in your links
to demonstrate such a proof. As programmer and not a
mathematician, I would probably need that, but might still
be befuddled by the math.

I am confused over the definition "Given an arbitrary M-program P."
That seems to narrow the problem compared to the Halting
Problem for a computer language/program in the link at the top.

Larry

Relevant Pages