Liste des Groupes | Revenir à c theory |
On 5/16/2025 3:21 AM, Mikko wrote:If HHH cannot report then that is more support that no correct HHH exists.On 2025-05-16 02:48:07 +0000, olcott said:When you try to encode that in a language like
>On 5/15/2025 1:55 AM, Mikko wrote:>On 2025-05-14 14:55:02 +0000, olcott said:>
>On 5/14/2025 2:15 AM, Mikko wrote:>On 2025-05-13 13:58:09 +0000, olcott said:>
>On 5/13/2025 2:46 AM, Mikko wrote:>On 2025-05-12 17:14:03 +0000, olcott said:>
>On 10/12/2022 6:49 PM, Keith Thompson wrote:>olcott <polcott2@gmail.com> writes:>On 10/12/2022 5:37 PM, Richard Damon wrote:>On 10/12/22 11:08 AM, olcott wrote:>Professor Michael Sipser of MIT said that this verbatim paragraph
looks correct:
<quoted email to professor Sipser>
Here is what I would like to say:
>
Professor Michael Sipser of MIT said that this verbatim paragraph
looks correct:
>
If H does correctly determine that its correct simulation
of D would never stop running unless aborted, would it be
correct for H to abort this simulation and report that D
specifies a non-halting sequence of configurations?
>
This validates the idea of a simulating halt decider referenced in
this paper.
>
Rebutting the Sipser Halting Problem Proof
https://www.researchgate.net/ publication/364302709_Rebutting_the_Sipser_Halting_Problem_Proof
>
Professor Sipser has not had the time to carefully review this paper
presented to him.
</quoted email to professor Sipser>
>
<quoted reply from professor Sipser>
Looks ok. Thanks for checking.
</quoted reply from professor Sipser>
>IF I drop by and ask him face to face, will he confirm this?>
Yes.
Would Professor Sipser agree that you have refuted his halting problem
proof?
>
If I understand this correctly, it does not support the idea that a
general "simulating halt decider" can actually exist.
>
In the above, let D be a program that may or may not halt, and let H be
an observer who attempts to determine whether or not D halts.
Concretely, let D be this C program or equivalent:
>
int main(void) { while (1) { } }
>
and I'll be H. I can observe D. I can simulate it until I get bored,
which won't take long (one iteration, two iterations, three iterations,
zzzzzzzzz). I can, while simulating it, conclude that it will never
halt, abort the simulation, and report that it never halts. It wouldn't
be difficult to automate the process in a way that works for this simple
case.
My scope is to prove that the "impossible"
input to all the halting problem proofs <is>
decidable.
As it is provably impossible it is not possible. The nearest you can hope
is to construct an oracle that can do what a Turing machine cannot do. It
would not be easy, just not yet proven imposssible.
Not at all. No one ever bothered to notice that
the contradictory part is unreachable code because
the counter-example input gets stuck in recursive
simulation. HHH simply sees this repeating pattern
and rejects DD.
As that does not identify any error in any proof it does not matter
whether that is noticed or not. What is soundly proven impossible
is impossible.
It is an error in the foundational basis of the proof.
When we assume that input DD can actually do the opposite
of whatever value that HHH reports then no HHH can correctly
report on the behavior of DD.
No. It does not point to a wrong word or clause or sentence in the
founcdational basis of the proof.
>No such DD can possibly exist.>
True but uninteresting. The important point is that no halt decider
exist. That a DD cannot be constructed from a non-existinghalt
decider is a rather obvious but not interesting.
There cannot possibly be any input D to a simulating
termination analyzer H that actually does the opposite
of whatever value that H returns.
For every decider there is a D that actually does halt if the
decider rejects and funs forever if the decider accepts.
>
C you will find that has always been a false
assumption.
int main()
{
DD(); // HHH cannot report on the behavior of its caller
}
int DD()
{
int Halt_Status = HHH(DD);
if (Halt_Status)
HERE: goto HERE;
return Halt_Status;
}
Les messages affichés proviennent d'usenet.