Path: ...!3.us.feeder.erje.net!3.eu.feeder.erje.net!feeder.erje.net!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail
From: Mikko <mikko.levanto@iki.fi>
Newsgroups: sci.logic
Subject: Re: Try and show how D correctly simulated by H reaches its own line 09
Date: Fri, 12 Jan 2024 10:22:07 +0200
Organization: -
Lines: 46
Message-ID: <unqsrf$3d3ma$1@dont-email.me>
References: <unotja$30rfb$3@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Info: dont-email.me; posting-host="4b758d744ba998db7183c3a839b06fa4";
	logging-data="3575498"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX18yP4uu1ZcO2wsw4+aS4ba+"
User-Agent: Unison/2.2
Cancel-Lock: sha1:bIMYTu2pnLvE3CbDKtXBNJNmToM=
Bytes: 2253

On 2024-01-11 14:22:34 +0000, olcott said about
"Try and show how D correctly simulated by H reaches its own line 09":

> 04 int D(ptr x)
> 05 {
> 06   int Halt_Status = H(x, x);
> 07   if (Halt_Status)
> 08     HERE: goto HERE;
> 09   return Halt_Status;
> 10 }
> 11
> 12 void main()
> 13 {
> 14   H(D,D);
> 15 }
> 
> *Execution Trace*
> Line 14: main() invokes H(D,D);
> 
> *keeps repeating* (unless aborted)
> Line 06: simulated D(D) invokes simulated H(D,D) that simulates D(D)
> 
> *Simulation invariant*
> *D correctly simulated by H cannot possibly reach past its own line 06*

What the correct simulation trace is, and in particular whether it
reaches the line 09, depends on what H does.

Assuming H is a buggy halt decider (i.e., H determines correctly for
some but incorrectly for other inputs whether the conputation ever
halts) that returns false for the specific input D, D, the execution
trace; and also assuming that H correctly traces what it (correctly
or otherwise) simulates:

//// start of simulation of D(D) by H
04 int D(ptr x) //// enter D, x = D
05 {
06   int Halt_Status = H(x, x); //// call H, x == D, returning 0
        //// code of H is not simulated
07   if (Halt_Status) //// Halt_Status is 0
09   return Halt_Status; //// return 0
//// end of simulation of D(D) by H

Mikko