@MSGID: 1@dont-email.me> 94361a53
@REPLY: 5@dont-email.me> 6a1a47b3
@REPLYADDR Mikko <mikko.levanto@iki.fi>
@REPLYTO 2:5075/128 Mikko
@CHRS: CP866 2
@RFC: 1 0
@RFC-Message-ID: 1@dont-email.me>
@RFC-References: 3@dont-email.me>
1@dont-email.me> 1@dont-email.me> 1@dont-email.me>
1@dont-email.me> 1@dont-email.me> 1@dont-email.me>
1@dont-email.me> 1@dont-email.me> 2@dont-email.me>
1@dont-email.me> 1@dont-email.me> 1@dont-email.me>
1@dont-email.me> 1@dont-email.me> 2@dont-email.me>
1@dont-email.me> 1@dont-email.me> 1@dont-email.me>
5@dont-email.me>
@TZUTC: 0300
@PID: Unison/2.2
@TID: FIDOGATE-5.12-ge4e8b94
On 2023-08-20 16:06:32 +0000, olcott said:

> On 8/20/2023 3:32 AM, Mikko wrote:
>> On 2023-08-19 23:02:11 +0000, olcott said:
>> 
>>> If D correctly simulated by H cannot possibly terminate normally then
>>> this proves that the actual behavior of the actual input is non-halting.
>> 
>> D correctly simulated by H does not even exist unless H correctly simulates
>> D. However, there is not need to say anything about "D correctly simulated
>> by H" because pain "D" is sufficient.
>> 
>> H`s simulation of D is another thing. It is not the same as D although
>> there is some similarity if H simulates correctly.
>> 
>>> A halt decider is required to report on the actual behavior of the
>>> actual input and it not allowed to report on any other behavior.
>> 
>> A decider is required to tell whether a text is of the kind that
>> the decider is required to identify. For a halt decider the requirement
>> is that the text is a description of a halting computation.
>> 
>> Mikko
>> 
> 
https://www.amazon.com/Introduction-Theory-Computation-Michael-Sipser/dp/1133187
79X 
> 
> 
> *Thu 10/13/2022 11:29 AM email from*
> MIT Professor Michael Sipser has agreed that the following verbatim 
> words are correct (he has not agreed to anything else):

> If simulating halt decider H correctly simulates its input D until H
> correctly determines that its simulated D would never stop running unless
> aborted then H can abort its simulation of D and correctly report that D
> specifies a non-halting sequence of configurations.

His opinion is that this statement is true. However, his opinion is not
a definition. If you want prove something, you must start with definitons,
not with opinions.

Mikko

--- Unison/2.2
 * Origin: - (2:5075/128)
SEEN-BY: 5001/100 5005/49 5015/255 5019/40 5020/715
848 1042 4441 12000
SEEN-BY: 5030/49 1081 5058/104 5075/128
@PATH: 5075/128 5020/1042 4441