Re: Rado's Sigma and the Halting Problem for Programs
From: peter_douglass (baisly_at_gis.net)
Date: 08/11/04
- Next message: Jyrki Lahtonen: "Re: representation of C[x]"
- Previous message: Ken Pledger: "Re: Reference for a cubic with a double root?"
- In reply to: r.e.s.: "Rado's Sigma and the Halting Problem for Programs"
- Next in thread: r.e.s.: "Re: Rado's Sigma and the Halting Problem for Programs"
- Reply: r.e.s.: "Re: Rado's Sigma and the Halting Problem for Programs"
- Messages sorted by: [ date ] [ thread ]
Date: 11 Aug 2004 13:35:30 -0700
"Acme Diagnostics" <LFinezapthis@partpostmark.net
<mailto:LFinezapthis@partpostmark.net>> wrote ...
AD > Is there any *linkable* proof of the Halting Problem for a
AD > computer language that does not contrive a logic paradox
AD > and require self-reference to make the proof?
AD > I'm not interested in Turing Machines at all, but only the
AD > proof "for a computer language."
to which
"r.e.s." <r.s@ZZmindspring.com <mailto:r.s@ZZmindspring.com>> in
message <news:5VxRc.13662$cK.1818@newsread2.news.pas.earthlink.net>...
responded:
RES > I doubt there's a proof that avoids reductio ad absurdum...
I'm not sure what a *linkable* proof is. However, I believe the
Halting Theorem may be proven without recourse to reductio
ad absurdum. Here is my stab at it.
Assume as given the following:
G :: N -> TM, G' :: TM -> N (an isomorphism between natural numbers
and Turing Machines)
<_,_> :: N x N -> N (a bijection between pairs of naturals and
naturals)
Eval :: TM x N -> N + _|_
( an evaluation function such that Eval(M,x) is the result of running
machine M on the input tape consisting of a representation of x.
We will assume that the result is converted to a natural number if the
computation halts, and is bottom, i.e. _|_ if the computation diverges
)
(Construction)
Assume that from a Turing Machine M we can construct a Turing Machine
M' such that the following holds:
Eval(M',x) == begin
if Eval(M, <G'(M'),x>) == "no"
then return "yes"
else loop_forever() ;
end
Definitions:
(Totality) Machine M is total
iff forall x, Eval(M,x) != _|_
(Partiality) Machine M is partial
iff There exists an x such that Eval(M,x) = _|_
(Halts)
Halts :: TM x N -> Bool . That is,
Halts(M,x) = True if the Turing Machine M halts when given
an input tape containing a representation of x
Halts(M,x) = False otherwise.
Note that Halts(M,x) is a well defined function.
It is not the hypothetical Turing machine "Halts" that
is proven not to exist by reductio ad absurdum in most
popular proofs of the Halting Theorem.
(Implements)
Machine M partially implements Halts
iff Eval(M,<x,y>) != _|_ <=> Eval(M,<x,y>) = Halts(G(x), y)
(That is, if M halts on input <x,y> then the value returned is
Halts(G(x),y)
CLAIM:
Our claim is that for any G and for any Turing Machine M
either M does not partially compute Halts, or M is not total.
Thus, there is no Turing Machine which totally computes
Halts. (This is a restatement of the Halting Theorem)
PROOF:
When M' (defined in Construction) is given G'(M') as input
it either halts or it diverges.
Case 1. Eval(M',G'(M')) != _|_ (i.e. halts)
(Construction) => Eval(M,<G'(M'),G'(M')>) = "no"
(Implements) => M does not partially implement Halts
Case 2. Eval(M',G'(M')) = _|_ (i.e. diverges)
(Construction) => either Eval(M,<G'(M'),G'(M')>) diverges
or Eval(M,<G'(M'),G'(M')>) returns a value != "no"
Case 2.a. Eval(M',G'(M')) = _|_ /\ Eval(M,<G'(M'),G'(M')>) = _|_
(Totality) => M is not total
Case 2.b. Eval(M',G(M')) = _|_
/\ Eval(M,<G'(M'),G'(M')>) returns value != "no"
(Implements) => M does not partially implement Halts
QED
- Next message: Jyrki Lahtonen: "Re: representation of C[x]"
- Previous message: Ken Pledger: "Re: Reference for a cubic with a double root?"
- In reply to: r.e.s.: "Rado's Sigma and the Halting Problem for Programs"
- Next in thread: r.e.s.: "Re: Rado's Sigma and the Halting Problem for Programs"
- Reply: r.e.s.: "Re: Rado's Sigma and the Halting Problem for Programs"
- Messages sorted by: [ date ] [ thread ]
Relevant Pages
|
