Liste des Groupes | Revenir à theory |
On 5/24/2025 4:59 AM, Fred. Zwarts wrote:All the information, the full specification of DD, including all functions it calls, which includes the code to abort, is present in the input.Op 24.mei.2025 om 02:30 schreef olcott:int main()On 5/23/2025 7:08 PM, Mike Terry wrote:>On 23/05/2025 19:37, Keith Thompson wrote:>Ben Bacarisse <ben@bsb.me.uk> writes:>Mike Terry <news.dead.person.stones@darjeeling.plus.com> writes:[...]And the big picture is that this can be done because false is the>
correct halting decision for some halting computations. He has said
this explicitly (as I have posted before) but he has also explained it
in words:
>
| When-so-ever a halt decider correctly determines that its input would
| never halt unless forced to halt by this halt decider this halt
| decider has made a correct not-halting determination.
Hmm. I don't read that the way you do. Did I miss something?
>
It assumes that the input is a non-halting computation ("its input
would never halt") and asserts that, in certain circumstances,
his mythical halt decider correctly determines that the input
is non-halting.
>
When his mythical halt decider correctly determines that its input
doesn't halt, it has made a correct non-halting determination.
It's just a tautology.
You're reading it the way most people would, and in the way I said Sipser would be interpreting the oft-quoted "Sipser quote". I don't think you've missed anything particularly.
>
I suppose Ben quoted PO saying this, because PO /uses/ it to justify that a particular /halting/ computation will never halt, PO's HHH simulates DDD (which halts) but before DDD halts it spots a pattern in the simulation, and announces non-halting.
In other words you expect that the HHH that DD calls
to report on the behavior of its caller?
>
How the f-ck can it do that?
All information is present in the input specification,
{
DD; // How the f-ck do you expect HHH called by DD to report
} // on the behavior of its caller?
// How can HHH even know that DD is its caller?
Les messages affichés proviennent d'usenet.