Rocksolid Light

Welcome to novaBBS (click a section below)

mail  files  register  nodelist  faq  login

Your computer account is overdrawn. Please reauthorize.


computers / comp.ai.philosophy / Re: It is known that a correct halt decider must return false (in this case)[V4](x86 as a formal language)

SubjectAuthor
* It is known that a correct halt decider must return false (in thisolcott
+* Re: It is known that a correct halt decider must return false (in this casolcott
|+* Re: It is known that a correct halt decider must return false (inMike Terry
||`* Re: It is known that a correct halt decider must return false (inolcott
|| +* Re: It is known that a correct halt decider must return false (inolcott
|| |`* Re: It is known that a correct halt decider must return false (in this casolcott
|| | `- Re: It is known that a correct halt decider must return false (in this casolcott
|| +* Re: It is known that a correct halt decider must return false (inolcott
|| |`- Re: It is known that a correct halt decider must return false (in this casolcott
|| `- Re: It is known that a correct halt decider must return false (inolcott
|`- Re: It is known that a correct halt decider must return false (inolcott
`* Re: It is known that a correct halt decider must return false (inolcott
 +- Re: It is known that a correct halt decider must return false (inolcott
 `* Re: It is known that a correct halt decider must return false (inolcott
  +* Re: It is known that a correct halt decider must return false (in this casolcott
  |+* Re: It is known that a correct halt decider must return false (in this casolcott
  ||`* Re: It is known that a correct halt decider must return false (inolcott
  || +- Re: It is known that a correct halt decider must return false (in this casolcott
  || +* Re: It is known that a correct halt decider must return false (in this casolcott
  || |`- Re: It is known that a correct halt decider must return false (in this casolcott
  || `* Re: It is known that a correct halt decider must return false (in this casolcott
  ||  +- Re: It is known that a correct halt decider must return false (in this casolcott
  ||  `- Re: It is known that a correct halt decider must return false (in this casolcott
  |`* Re: It is known that a correct halt decider must return false (inolcott
  | `* Re: It is known that a correct halt decider must return false (inolcott
  |  `* Re: It is known that a correct halt decider must return false (inolcott
  |   `* Re: It is known that a correct halt decider must return false (inolcott
  |    `* Re: It is known that a correct halt decider must return false (in this casolcott
  |     `* Re: It is known that a correct halt decider must return false (inolcott
  |      `* Re: It is known that a correct halt decider must return false (inolcott
  |       `* Re: It is known that a correct halt decider must return false (inolcott
  |        +* Re: It is known that a correct halt decider must return false (inolcott
  |        |`* Re: It is known that a correct halt decider must return false (inolcott
  |        | `* Re: It is known that a correct halt decider must return false (inolcott
  |        |  +- Re: It is known that a correct halt decider must return false (inolcott
  |        |  `* Re: It is known that a correct halt decider must return false (inolcott
  |        |   +* Re: It is known that a correct halt decider must return false (in this casolcott
  |        |   |`* Re: It is known that a correct halt decider must return false (inolcott
  |        |   | `* Re: It is known that a correct halt decider must return false (inolcott
  |        |   |  `* Re: It is known that a correct halt decider must return false (inolcott
  |        |   |   `- Re: It is known that a correct halt decider must return falseolcott
  |        |   +* Re: It is known that a correct halt decider must return false (inolcott
  |        |   |+- Re: It is known that a correct halt decider must return false (inolcott
  |        |   |`* Re: It is known that a correct halt decider must return false (in this casolcott
  |        |   | +* Re: It is known that a correct halt decider must return false (inolcott
  |        |   | |`* Re: It is known that a correct halt decider must return false (inolcott
  |        |   | | +- Re: It is known that a correct halt decider must return false (inolcott
  |        |   | | `- Re: It is known that a correct halt decider must return false (in this casolcott
  |        |   | `* Re: It is known that a correct halt decider must return false (inolcott
  |        |   |  `* Re: It is known that a correct halt decider must return false (in this casolcott
  |        |   |   `* Re: It is known that a correct halt decider must return false (inMr Flibble
  |        |   |    `- Re: It is known that a correct halt decider must return false (inolcott
  |        |   `- Re: It is known that a correct halt decider must return false (inolcott
  |        `* Re: _It_is_known_that_a_correct_halt_decider_must_return_false_(in_this_caolcott
  |         `* Re: _It_is_known_that_a_correct_halt_decider_must_returnolcott
  |          `* Re: _It_is_known_that_a_correct_halt_decider_must_returnolcott
  |           +* Re: _It_is_known_that_a_correct_halt_decider_must_return_false_(in_this_caolcott
  |           |+- Re: _It_is_known_that_a_correct_halt_decider_must_returnJeff Barnett
  |           |`- Re: It is known that a correct halt decider must return false (inolcott
  |           `- Re: _It_is_known_that_a_correct_halt_decider_must_returnolcott
  `* Re: It is known that a correct halt decider must return false (in this casolcott
   `* Re: It is known that a correct halt decider must return false (inolcott
    +* Re: It is known that a correct halt decider must return false (This is theolcott
    |`* Re: It is known that a correct halt decider must return false (Thisolcott
    | `* Re: It is known that a correct halt decider must return false (Thisolcott
    |  `- Re: It is known that a correct halt decider must return false (Thisolcott
    `* Re: It is known that a correct halt decider must return false (in this casolcott
     +* Re: It is known that a correct halt decider must return false (in this casolcott
     |`* Re: It is known that a correct halt decider must return false (in this casolcott
     | `- Re: It is known that a correct halt decider must return false (in this casolcott
     +- Re: It is known that a correct halt decider must return false (inolcott
     `* Re: It is known that a correct halt decider must return false (inolcott
      +- Re: It is known that a correct halt decider must return false (inolcott
      `* Re: It is known that a correct halt decider must return false (inolcott
       `* Re: It is known that a correct halt decider must return false (in this casolcott
        +- Re: It is known that a correct halt decider must return false (inolcott
        +- Re: It is known that a correct halt decider must return false (in this casolcott
        `* Re: It is known that a correct halt decider must return false (inolcott
         +* Re: It is known that a correct halt decider must return false (in this casolcott
         |`* Re: It is known that a correct halt decider must return false (in this casolcott
         | `- Re: It is known that a correct halt decider must return false (in this casolcott
         `- Re: It is known that a correct halt decider must return false (inolcott

Pages:1234
Subject: Re: It is known that a correct halt decider must return false (This is the whole thing)
From: olcott
Newsgroups: comp.theory, comp.ai.philosophy, comp.software-eng
Date: Wed, 25 Nov 2020 05:12 UTC
References: 1 2 3 4 5 6 7 8 9 10 11 12 13 14
Path: i2pn2.org!i2pn.org!weretis.net!feeder6.news.weretis.net!news.snarked.org!border2.nntp.dca1.giganews.com!nntp.giganews.com!buffer2.nntp.dca1.giganews.com!news.giganews.com.POSTED!not-for-mail
NNTP-Posting-Date: Tue, 24 Nov 2020 23:12:29 -0600
Subject: Re: It is known that a correct halt decider must return false (This
is the whole thing)
Newsgroups: comp.theory,comp.ai.philosophy,comp.software-eng
References: <TqWdnXCuh8jFkibCnZ2dnUU7-QfNnZ2d@giganews.com>
<he6dnVxcwNcfviHCnZ2dnUU78IfNnZ2d@brightview.co.uk>
<ndKdnaIe-v9PtCHCnZ2dnUU7-XPNnZ2d@giganews.com>
<5eGdndmbxcGA1iHCnZ2dnUU78enNnZ2d@brightview.co.uk>
<WcCdncOumL5JyCHCnZ2dnUU7-Y3NnZ2d@giganews.com> <87im9vpg0e.fsf@bsb.me.uk>
<qoGdnW1Lz5qmByHCnZ2dnUU7-UPNnZ2d@giganews.com> <87sg8yah0c.fsf@bsb.me.uk>
<Weqdnbjny8LJqSDCnZ2dnUU7-d_NnZ2d@giganews.com> <87tute8f4h.fsf@bsb.me.uk>
<2aidnV9e3qQaOCDCnZ2dnUU7-c3NnZ2d@giganews.com>
<wVkvH.8783$OP2.1118@fx18.iad>
<n_udnTA2IcmUfCDCnZ2dnUU7-LfNnZ2d@giganews.com>
<FrlvH.13948$lo15.12878@fx35.iad>
From: NoO...@NoWhere.com (olcott)
Date: Tue, 24 Nov 2020 23:12:33 -0600
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:78.0) Gecko/20100101
Thunderbird/78.5.0
MIME-Version: 1.0
In-Reply-To: <FrlvH.13948$lo15.12878@fx35.iad>
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Language: en-US
Content-Transfer-Encoding: 8bit
Message-ID: <sK2dnVNE0sAgeiDCnZ2dnUU7-QXNnZ2d@giganews.com>
Lines: 101
X-Usenet-Provider: http://www.giganews.com
X-Trace: sv3-PiZ9iHe8kPe2jZXZpb0ZDlzxaVBkTkcZuKm1YaEp4Z1Stfa0fhCUfUBmBzAp+3bELznCRff2xb6Np+Y!KGhQgocc2rZShrpTrrl5ETi6e7bgJg3+D0D6gQOLJgeSOOBJUIBdJOuSN6SH+tETocXsMLfMqknd!XA==
X-Complaints-To: abuse@giganews.com
X-DMCA-Notifications: http://www.giganews.com/info/dmca.html
X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers
X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint properly
X-Postfilter: 1.3.40
X-Original-Bytes: 5735
View all headers
On 11/24/2020 10:53 PM, Richard Damon wrote:
On 11/24/20 11:43 PM, olcott wrote:
On 11/24/2020 10:17 PM, Richard Damon wrote:
On 11/24/20 7:30 PM, olcott wrote:
On 11/24/2020 6:16 PM, Ben Bacarisse wrote:
olcott <NoOne@NoWhere.com> writes:

On 11/24/2020 9:53 AM, Ben Bacarisse wrote:
olcott <NoOne@NoWhere.com> writes:

On 11/23/2020 9:53 PM, Ben Bacarisse wrote:
olcott <NoOne@NoWhere.com> writes:

All that I have right now is a DebugTrace() of all the user
specified
code. This provides a very obvious basis for a halt decider's
correct
halting decision of the H_Hat code specified in this execution
trace.

Gosh.  Is that a lie, or is that just very, very stupid?  Lying or
dumb,
dumb or lying?  I can never quite tell.

Having only the code that loops around the single stepping
DebugTrace()
(presumably a simple modification to someone else's emulator) is
exactly
the wrong basis for a halt decider.  Its the version that makes the
"Hat" computation non-finite BY NOT BEING A DECIDER.  The "HAT"
computation you are analysing is irrelevant because it's not built
on a
finite decider.

Only when you add the impossible "abort if needed" code would you
have
anything that even resembles a decider.  But it's not a halt
decider,
because that code has ITS OWN "HAT" computation which it decides
incorrectly.

No it does not and you know that it does not.

If you dare post the code, I'll show you, explicitly (again).

The simplified code that I posted never has been the actual code. The
actual code is far too complex to use as an example.

Line 14 requires an enormously complex set up to enable x86utm to be a
multi-tasking operating system. This was the most difficult part of
the development whole x86utm operating system.

(And line 15 is harder still.  It's either impossible or it must get an
infinity of cases wrong.  Curiously, though, it doesn't matter.  I am
happy to assume that it is 100% accurate -- no false positives or
negatives.)

08 bool Halts(u32 P, u32 I)
09 {
10   bool Halted  = false;
11   bool Aborted = false;
12   while (!Halted && !Aborted)
13   {
14     Halted  = DebugStep(P, I);
15     Aborted = Needs_To_Be_Aborted();
16   }
17   return !Aborted;
18 }

Given

     void Confound_Halts(u32 P) { if (Halts(P, P)) while (1); }

The confounding example for Halts is the computation
Confound_Halts(Confound_Halts) whose halting status is not correctly
determined by the function call Halts(Confound_Halts, Confound_Halts).

Halts(Confound_Halts, Confound_Halts) returns false.

At which point the if skips the while loop and the machine halts, so the
decider was wrong.

Only because we change the question from:

Does the input halt on its input?
    to
Must the input be aborted to prevent its otherwise infinite execution?

Are the key counter-examples of the HP proofs made halting decidable.


But, as has been shown, this are truly exact opposites,

A program that only halts if it is aborted has opposite halting behavior to a program that halts without being aborted.

--
Copyright 2020 Pete Olcott

"Great spirits have always encountered violent opposition from mediocre minds." Einstein


Subject: Re: It is known that a correct halt decider must return false (This is the whole thing)
From: olcott
Newsgroups: comp.theory, comp.ai.philosophy, comp.software-eng
Date: Wed, 25 Nov 2020 14:17 UTC
References: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16
Path: i2pn2.org!i2pn.org!weretis.net!feeder6.news.weretis.net!news.snarked.org!border2.nntp.dca1.giganews.com!nntp.giganews.com!buffer2.nntp.dca1.giganews.com!buffer1.nntp.dca1.giganews.com!news.giganews.com.POSTED!not-for-mail
NNTP-Posting-Date: Wed, 25 Nov 2020 08:17:12 -0600
Subject: Re: It is known that a correct halt decider must return false (This
is the whole thing)
Newsgroups: comp.theory,comp.ai.philosophy,comp.software-eng
References: <TqWdnXCuh8jFkibCnZ2dnUU7-QfNnZ2d@giganews.com>
<he6dnVxcwNcfviHCnZ2dnUU78IfNnZ2d@brightview.co.uk>
<ndKdnaIe-v9PtCHCnZ2dnUU7-XPNnZ2d@giganews.com>
<5eGdndmbxcGA1iHCnZ2dnUU78enNnZ2d@brightview.co.uk>
<WcCdncOumL5JyCHCnZ2dnUU7-Y3NnZ2d@giganews.com> <87im9vpg0e.fsf@bsb.me.uk>
<qoGdnW1Lz5qmByHCnZ2dnUU7-UPNnZ2d@giganews.com> <87sg8yah0c.fsf@bsb.me.uk>
<Weqdnbjny8LJqSDCnZ2dnUU7-d_NnZ2d@giganews.com> <87tute8f4h.fsf@bsb.me.uk>
<2aidnV9e3qQaOCDCnZ2dnUU7-c3NnZ2d@giganews.com>
<wVkvH.8783$OP2.1118@fx18.iad>
<n_udnTA2IcmUfCDCnZ2dnUU7-LfNnZ2d@giganews.com>
<FrlvH.13948$lo15.12878@fx35.iad>
<sK2dnVNE0sAgeiDCnZ2dnUU7-QXNnZ2d@giganews.com>
<IfsvH.106027$1R4.16061@fx44.iad>
From: NoO...@NoWhere.com (olcott)
Date: Wed, 25 Nov 2020 08:17:17 -0600
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:78.0) Gecko/20100101
Thunderbird/78.5.0
MIME-Version: 1.0
In-Reply-To: <IfsvH.106027$1R4.16061@fx44.iad>
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Language: en-US
Content-Transfer-Encoding: 8bit
Message-ID: <N6adnVpAzJ_1-iPCnZ2dnUU7-T_NnZ2d@giganews.com>
Lines: 60
X-Usenet-Provider: http://www.giganews.com
X-Trace: sv3-SVnKxWGz9sYnj86PoKOYjWCW3by+hzDjrobGBuAkCZfGP8eoK+2r0FvpBNXTNxGop04GxWXYVhDESL2!hmMpKrBk3/hGW7L8qS7dGQtAr6E1QwI+CXev17teejJuyRt+Gt+50Izsr6fTRv1AyAuii5KAl1U/!eA==
X-Complaints-To: abuse@giganews.com
X-DMCA-Notifications: http://www.giganews.com/info/dmca.html
X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers
X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint properly
X-Postfilter: 1.3.40
X-Original-Bytes: 4127
View all headers
On 11/25/2020 6:39 AM, Richard Damon wrote:
On 11/25/20 12:12 AM, olcott wrote:
On 11/24/2020 10:53 PM, Richard Damon wrote:
On 11/24/20 11:43 PM, olcott wrote:

Only because we change the question from:

Does the input halt on its input?
     to
Must the input be aborted to prevent its otherwise infinite execution?

Are the key counter-examples of the HP proofs made halting decidable.


But, as has been shown, this are truly exact opposites,

A program that only halts if it is aborted has opposite halting behavior
to a program that halts without being aborted.

Yes, a program that ONLY halts if it is aborted is the opposite of a
pogrmam that halts without being aborted.

A program that haltes because it was aborted is something very
different. It might have halted anyway if given more time.

There are a set of programs that can be determined in advance to never halt. Here is one of them:

int main()
{
   HERE: goto HERE;
}

The key words here are things like MUST and ONLY. Just because you come
up with some 'logical' justification that make it seems like it needs to
be. The REAL test is to actually run it and see. If the actual program
when run does halt, then the logic has been proved to be unsound.

There are a set of computations that can be determined in advance that will never halt and this can be determined with 100% logical certainty.

Yes, proving a given computation is indeed non-halting can be difficult,
even impossible (otherwise we COULD have halting deciders), but very

This kind of pure speculation is no sort of counter-example proof of undecidability.

many cases can be proven with a few simple rules. Things like repeating
state or loops with no way out (absolutely no way out, not even an OS
monetering them with the ability to abort them), so we can answer many
cases, and in particular, if we can find the halting behavior, we can
disprove the non-halting determination.



--
Copyright 2020 Pete Olcott

"Great spirits have always encountered violent opposition from mediocre minds." Einstein


Subject: Re: It is known that a correct halt decider must return false (This is the whole thing)
From: olcott
Newsgroups: comp.theory, comp.ai.philosophy, comp.software-eng
Date: Wed, 25 Nov 2020 15:52 UTC
References: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18
Path: i2pn2.org!i2pn.org!weretis.net!feeder6.news.weretis.net!news.snarked.org!border2.nntp.dca1.giganews.com!nntp.giganews.com!buffer2.nntp.dca1.giganews.com!buffer1.nntp.dca1.giganews.com!news.giganews.com.POSTED!not-for-mail
NNTP-Posting-Date: Wed, 25 Nov 2020 09:52:49 -0600
Subject: Re: It is known that a correct halt decider must return false (This
is the whole thing)
Newsgroups: comp.theory,comp.ai.philosophy,comp.software-eng
References: <TqWdnXCuh8jFkibCnZ2dnUU7-QfNnZ2d@giganews.com>
<he6dnVxcwNcfviHCnZ2dnUU78IfNnZ2d@brightview.co.uk>
<ndKdnaIe-v9PtCHCnZ2dnUU7-XPNnZ2d@giganews.com>
<5eGdndmbxcGA1iHCnZ2dnUU78enNnZ2d@brightview.co.uk>
<WcCdncOumL5JyCHCnZ2dnUU7-Y3NnZ2d@giganews.com> <87im9vpg0e.fsf@bsb.me.uk>
<qoGdnW1Lz5qmByHCnZ2dnUU7-UPNnZ2d@giganews.com> <87sg8yah0c.fsf@bsb.me.uk>
<Weqdnbjny8LJqSDCnZ2dnUU7-d_NnZ2d@giganews.com> <87tute8f4h.fsf@bsb.me.uk>
<2aidnV9e3qQaOCDCnZ2dnUU7-c3NnZ2d@giganews.com>
<wVkvH.8783$OP2.1118@fx18.iad>
<n_udnTA2IcmUfCDCnZ2dnUU7-LfNnZ2d@giganews.com>
<FrlvH.13948$lo15.12878@fx35.iad>
<sK2dnVNE0sAgeiDCnZ2dnUU7-QXNnZ2d@giganews.com>
<IfsvH.106027$1R4.16061@fx44.iad>
<N6adnVpAzJ_1-iPCnZ2dnUU7-T_NnZ2d@giganews.com>
<3xuvH.199083$oL7.71453@fx06.iad>
From: NoO...@NoWhere.com (olcott)
Date: Wed, 25 Nov 2020 09:52:54 -0600
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:78.0) Gecko/20100101
Thunderbird/78.5.0
MIME-Version: 1.0
In-Reply-To: <3xuvH.199083$oL7.71453@fx06.iad>
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Language: en-US
Content-Transfer-Encoding: 8bit
Message-ID: <uO6dnXXxyv1M4CPCnZ2dnUU7-YXNnZ2d@giganews.com>
Lines: 152
X-Usenet-Provider: http://www.giganews.com
X-Trace: sv3-So396wvNWB2Ltzn+UDyFk8p6u6M1GZmRrAO+uEMGewTT/joT9aKgRg7LaaQcQpFenD/IjStG6oRNmrN!mq4/A03ZNL6iIMGTxwWL2kfGU0ioj0bATfscPx+c21KMogtbLrlZK3o0uhm7lwBEh9LjcrUUBJS5!Pw==
X-Complaints-To: abuse@giganews.com
X-DMCA-Notifications: http://www.giganews.com/info/dmca.html
X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers
X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint properly
X-Postfilter: 1.3.40
X-Original-Bytes: 7094
View all headers
On 11/25/2020 9:14 AM, Richard Damon wrote:
On 11/25/20 9:17 AM, olcott wrote:
On 11/25/2020 6:39 AM, Richard Damon wrote:
On 11/25/20 12:12 AM, olcott wrote:
On 11/24/2020 10:53 PM, Richard Damon wrote:
On 11/24/20 11:43 PM, olcott wrote:

Only because we change the question from:

Does the input halt on its input?
      to
Must the input be aborted to prevent its otherwise infinite execution?

Are the key counter-examples of the HP proofs made halting decidable.


But, as has been shown, this are truly exact opposites,

A program that only halts if it is aborted has opposite halting behavior
to a program that halts without being aborted.

Yes, a program that ONLY halts if it is aborted is the opposite of a
pogrmam that halts without being aborted.

A program that haltes because it was aborted is something very
different. It might have halted anyway if given more time.

There are a set of programs that can be determined in advance to never
halt. Here is one of them:

int main()
{
   HERE: goto HERE;
}


Never denied that.

The key words here are things like MUST and ONLY. Just because you come
up with some 'logical' justification that make it seems like it needs to
be. The REAL test is to actually run it and see. If the actual program
when run does halt, then the logic has been proved to be unsound.

There are a set of computations that can be determined in advance that
will never halt and this can be determined with 100% logical certainty.


Never denied that, there is a set of computation that can be determined
in adanced that will never halt. That set might not include every
computation that WILL not halt. (in fact, because the halting problem
HAS been proved to be unsolvable, we know that there will be members in
the set of non-halting computations that can not be proven to be
non-halting).

(1)I did correctly show how to decide halting for the x86utm computational equivalent of a simplified form of the Linz Ĥ.

(2) This simplified form of the Linz H_Hat is the basis for all of the conventional halting problem proofs.

∴ I have proved that none of these conventional proofs (including Linz) have any basis for their conclusion.

void H_Hat(u32 P)
{
   u32 Aborted = DebugTrace(P, P);
   if (Aborted)
     HALT
   else
     HERE: goto HERE;
}

All of the current rebuttals take the form that because Halts() does correct decide its input and it is common knowledge that this is impossible therefore Halts must be incorrect.


Yes, proving a given computation is indeed non-halting can be difficult,
even impossible (otherwise we COULD have halting deciders), but very

This kind of pure speculation is no sort of counter-example proof of
undecidability.

Until you can PROVE that you can decide EVERY case correctly, you don't
have ground to stand on. I can stand on the grounds of Linz (and
others_, and say the statement is proven.

Yes if you ignore the verified fact that the above code is decided correctly you can bury your head in the sand and say that Linz still applies.

Since we have a case that your machine still does not decide correctly,
by the criteria of the classical halting problem, which by your
arguments, you seem to be working on, you counter proof is disproved.

We have no such case. You said that Halts must be wrong BECAUSE it gets the correct answer.

The traces you have provided, in part because they are only partial
since you haven't finished, show one of two failures. Either you fail by
failing to proved the answer to the computation asking for it,

Simply ignoring my rebuttals is not any actual rebuttal at all, you seem to thinks that it is. I have asked you this at least three times and and you simply ignore my question.


What return value does H_Hat() receive from DebugTrace() ?
What return value does H_Hat() receive from DebugTrace() ?
What return value does H_Hat() receive from DebugTrace() ?
What return value does H_Hat() receive from DebugTrace() ?
What return value does H_Hat() receive from DebugTrace() ?
What return value does H_Hat() receive from DebugTrace() ?
What return value does H_Hat() receive from DebugTrace() ?
What return value does H_Hat() receive from DebugTrace() ?
What return value does H_Hat() receive from DebugTrace() ?
What return value does H_Hat() receive from DebugTrace() ?

int DebugTrace(u32 N, u32 M)
{
   return ((int(*)(int))N)(M);
   return 1;
}


void H_Hat(u32 P)
{
   u32 Aborted = DebugTrace(P, P);
   if (Aborted)
     HALT
   else
     HERE: goto HERE;
}


int main()
{
   u32 P = (u32)H_Hat;
   DebugTrace(P, P);
   HALT;
}






--
Copyright 2020 Pete Olcott

"Great spirits have always encountered violent opposition from mediocre minds." Einstein


Subject: Re: It is known that a correct halt decider must return false (in this case)[V4](Mike Terry said)
From: olcott
Newsgroups: comp.theory, comp.ai.philosophy, comp.software-eng
Date: Wed, 25 Nov 2020 17:18 UTC
References: 1 2 3 4 5 6 7 8 9
Path: i2pn2.org!i2pn.org!weretis.net!feeder8.news.weretis.net!news.uzoreto.com!tr2.eu1.usenetexpress.com!feeder.usenetexpress.com!tr3.iad1.usenetexpress.com!border1.nntp.dca1.giganews.com!nntp.giganews.com!buffer1.nntp.dca1.giganews.com!news.giganews.com.POSTED!not-for-mail
NNTP-Posting-Date: Wed, 25 Nov 2020 11:18:38 -0600
Subject: Re: It is known that a correct halt decider must return false (in this case)[V4](Mike Terry said)
Newsgroups: comp.theory,comp.ai.philosophy,comp.software-eng
References: <TqWdnXCuh8jFkibCnZ2dnUU7-QfNnZ2d@giganews.com> <CFEuH.1740$se1.1735@fx27.iad> <87v9dwsr1m.fsf@bsb.me.uk> <vNCdnT2ISMM4sCbCnZ2dnUU7-LPNnZ2d@giganews.com> <_tudndH2L5L_cSbCnZ2dnUU78W3NnZ2d@brightview.co.uk> <IvudnSrhmtzCbibCnZ2dnUU7-f_NnZ2d@giganews.com> <NPCdnfBnTvdIniHCnZ2dnUU78VvNnZ2d@brightview.co.uk> <cJidnYh0YfJImyHCnZ2dnUU7-R-dnZ2d@giganews.com> <2IOdnXOqUZnPGCPCnZ2dnUU78QGdnZ2d@brightview.co.uk>
From: NoO...@NoWhere.com (olcott)
Date: Wed, 25 Nov 2020 11:18:44 -0600
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:78.0) Gecko/20100101 Thunderbird/78.5.0
MIME-Version: 1.0
In-Reply-To: <2IOdnXOqUZnPGCPCnZ2dnUU78QGdnZ2d@brightview.co.uk>
Content-Type: text/plain; charset=windows-1252; format=flowed
Content-Language: en-US
Content-Transfer-Encoding: 8bit
Message-ID: <EOudnWgbKL1zDCPCnZ2dnUU7-SudnZ2d@giganews.com>
Lines: 127
X-Usenet-Provider: http://www.giganews.com
X-Trace: sv3-zPRRHvZTJKka22cqCkqvActU1iHgBg0k+h6NaepgSBtHKTtMXw6iRjvLxGNff2kea1XnsopxEeaKHMN!54spCd++kPkYIeMfl7uuHMwhJA06I0CHXmPRaW2qy4wWq7ZQm7pS+GiC/pbopqiKvS7bA7gCIfjP!1w==
X-Complaints-To: abuse@giganews.com
X-DMCA-Notifications: http://www.giganews.com/info/dmca.html
X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers
X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint properly
X-Postfilter: 1.3.40
X-Original-Bytes: 5420
View all headers
On 11/25/2020 10:24 AM, Mike Terry wrote:
On 23/11/2020 19:00, olcott wrote:
On 11/23/2020 12:47 PM, Mike Terry wrote:
On 23/11/2020 17:37, olcott wrote:
On 11/23/2020 11:07 AM, Mike Terry wrote:
On 23/11/2020 03:33, olcott wrote:
On 11/22/2020 9:14 PM, Ben Bacarisse wrote:
Richard Damon <Richard@Damon-Family.org> writes:

Maybe you have created a system that is a Halter, which will just
abort
any program that it determines will never halt. That might have some
use, but isn't the Halt Decider from Linz.

The irony is that that algorith -- the algorithm that determines if a
computation must be aborted -- is also impossible.  He's not written
it > yet

IT IS IN THE FIRST POST OF THIS THREAD.
This is my 2018-12-13 solution.

We merely scan the complete execution trace after each instruction is
executed and see if there have been any function calls to the same
function from the same address without any intervening conditional
branch instructions.

Here is what Mike said about correctly deciding H_Hat:

On 11/20/2020 9:30 PM, Mike Terry wrote:
input (H_Hat,H_Hat) is non-halting, assuming your Halts() is as
described.  This is all baby stuff.  [So the correct halting decision
for the input is non-halting].


STOP QUOTING ME OUT OF CONTEXT.

THE H_Hat OF THE POST TO WHICH YOU REFER IS A *COMPLETELY DIFFERENT*
H_Hat TO THE ONE IN THIS THREAD.  You are misrepresenting my position
to falsely support your own.

The two versions of H_Hat are computationally equivalent, thus your
claim that they are *COMPLETELY DIFFERENT*  is proved to be false.

Here is the one that you responded to:
On Friday, November 20, 2020 at 8:45:59 PM UTC-6, olcott wrote:
void H_Hat(u32 P)
{
  u32 Aborted = Halts(P, P);
  if (Aborted)
    HALT
  else
    HERE: goto HERE;
}


int main()
{
  u32 P = (u32)H_Hat;
  Halts(P, P);
  HALT;
}
https://groups.google.com/g/comp.theory/c/1uKuMgjxJTM/m/c3HEt-UWAAAJ

Ahem, you've "conveniently" omitted the important context of the
original thread.  Let me restore it for you:

This above link IS THE WHOLE MESSAGE NO DETAILS ARE MISSING.

Wrong.  There is stuff which was in earlier posts that had been snipped in earlier posts.  If you'd read a few lines further in my post it is perfectly clear what I was saying.

You're just being obstructive here.

Mike.



Here is the full context by direct cut-and-paste:

On 11/24/2020 8:04 PM, Mike Terry wrote:
 > On 24/11/2020 20:44, olcott wrote:
 >> int DebugTrace(u32 N, u32 M)
 >> {
 >>   return ((int(*)(int))N)(M);
 >> }
 >>
 >>
 >> void H_Hat(u32 P)
 >> {
 >>   u32 Aborted = DebugTrace(P, P);
 >>   if (Aborted)
 >>     HALT
 >>   else
 >>     HERE: goto HERE;
 >> }
 >>
 >>
 >> int main()
 >> {
 >>   u32 P = (u32)H_Hat;
 >>   DebugTrace(P, P);
 >>   HALT;
 >> }
 >>
 >>
 >> This proves the following:
 >> (2) H_Hat is infinitely recursive.
 >>
 > I don't think anyone would dispute that...
 > (I don't dispute it, and I'm "just this guy")
 >
 >> (3) The infinite recursion of H_Hat can be analytically
 >> be determined in advance.
 >
 > No, it *doesn't* prove that!



--
Copyright 2020 Pete Olcott

"Great spirits have always encountered violent opposition from mediocre minds." Einstein


Subject: Re: It is known that a correct halt decider must return false (in this case)[V4](infallible)
From: olcott
Newsgroups: comp.theory, comp.ai.philosophy, comp.software-eng
Date: Wed, 25 Nov 2020 17:21 UTC
References: 1 2 3 4 5 6 7 8 9
Path: i2pn2.org!i2pn.org!aioe.org!peer03.ams4!peer.am4.highwinds-media.com!peer03.iad!feed-me.highwinds-media.com!news.highwinds-media.com!border1.nntp.dca1.giganews.com!nntp.giganews.com!buffer1.nntp.dca1.giganews.com!buffer2.nntp.dca1.giganews.com!news.giganews.com.POSTED!not-for-mail
NNTP-Posting-Date: Wed, 25 Nov 2020 11:21:16 -0600
Subject: Re: It is known that a correct halt decider must return false (in
this case)[V4](infallible)
Newsgroups: comp.theory,comp.ai.philosophy,comp.software-eng
References: <TqWdnXCuh8jFkibCnZ2dnUU7-QfNnZ2d@giganews.com>
<he6dnVxcwNcfviHCnZ2dnUU78IfNnZ2d@brightview.co.uk>
<ndKdnaIe-v9PtCHCnZ2dnUU7-XPNnZ2d@giganews.com>
<5eGdndmbxcGA1iHCnZ2dnUU78enNnZ2d@brightview.co.uk>
<WcCdncOumL5JyCHCnZ2dnUU7-Y3NnZ2d@giganews.com>
<ToOdneeOqN8q6CHCnZ2dnUU78UfNnZ2d@brightview.co.uk>
<JuqdnaQGaYAtFCHCnZ2dnUU7-Q3NnZ2d@giganews.com>
<QrqdnS61EOtetCDCnZ2dnUU78TPNnZ2d@brightview.co.uk>
<qPCdnSYYdNW-FyPCnZ2dnUU78QHNnZ2d@brightview.co.uk>
From: NoO...@NoWhere.com (olcott)
Date: Wed, 25 Nov 2020 11:21:21 -0600
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:78.0) Gecko/20100101
Thunderbird/78.5.0
MIME-Version: 1.0
In-Reply-To: <qPCdnSYYdNW-FyPCnZ2dnUU78QHNnZ2d@brightview.co.uk>
Content-Type: text/plain; charset=windows-1252; format=flowed
Content-Language: en-US
Content-Transfer-Encoding: 8bit
Message-ID: <EOudnWsbKL0RDyPCnZ2dnUU7-SudnZ2d@giganews.com>
Lines: 87
X-Usenet-Provider: http://www.giganews.com
X-Trace: sv3-pd0/7PxJr/4Q7Hu6YjCF8Q0AV0q8/P2u89R1oiizaGe7nuvTL0OizmZwCWr+Sqcft5DforWo9OaWTVr!J1WkHO11R+5/cpmTRlBk/TnvlpxdMECU5CxlzNGdimkxI7p8sW2OhSteUV+czF4VAHLhS68oTHpU!zg==
X-Complaints-To: abuse@giganews.com
X-DMCA-Notifications: http://www.giganews.com/info/dmca.html
X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers
X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint properly
X-Postfilter: 1.3.40
X-Original-Bytes: 4556
X-Received-Bytes: 4799
X-Received-Body-CRC: 1302515464
View all headers
On 11/25/2020 10:45 AM, Mike Terry wrote:
On 24/11/2020 15:41, Mike Terry wrote:
On 24/11/2020 04:18, olcott wrote:
<.. snip ..>

People can eventually look at all of my code and the thousands of lines
of code of the x86 emulator and they can look at the hundreds of pages
out output. It all boils down to this:

The simulator merely watches its simulation of the following
instructions until it sees a function call to 377 from 503 the second
time with no JCC (Jump-Condition_Code) in-between.


I have told you many times that your test must be UNSOUND.  You have
never responded to this, so I've assumed you don't really know whether
your test is sound or unsound (or probably, what that even means,
although I've also explained that to you before).

Now you are getting closer to actually coding the test (which you
claimed to have "fully coded" two years ago), you are finally giving
more details.

So...  what do you think.  Is the following test a SOUND test for
non-halting?

   TEST:  "monitor the simulation until there is a function
           call to 377 from 503 a second time, with no conditional
           branch inbetween"

Putting it more directly - if some calculation P(I) triggers the TEST
(so it contains two calls from 377 from 503, with no conditional branch
inbetween), does this genuinely imply that the calculation will never halt?

Bear in mind that the two calls in question do not necessarily occur in
the same "virtual address space", that is to say the two calls can [and
in the case of T_Hat(T_Hat) *do* ] occur at /different levels of
emulation/.   [Your trace notation obscures this simple fact, making
everything appear to be in one single virtual process, when it's not.]

What do you think?  This seems to be your primary intuition that
triggered all this "refuting" activity, BUT IS IT ACTUALLY CORRECT?

Of course, you will say "All my intuitions are correct by definition -
I'm never wrong" but that doesn't make it true!  :)

Is TEST *SOUND* ?


Noted: still no response to this basic question.

Mike.


int DebugTrace(u32 N, u32 M)
{
   return ((int(*)(int))N)(M);
}


void H_Hat(u32 P)
{
   u32 Aborted = DebugTrace(P, P);
   if (Aborted)
     HALT
   else
     HERE: goto HERE;
}


int main()
{
   u32 P = (u32)H_Hat;
   DebugTrace(P, P);
   HALT;
}

The determination that the above code specifies infinite recursion is infallible. People can have different meanings for the term "sound", infallible has only one meaning.

--
Copyright 2020 Pete Olcott

"Great spirits have always encountered violent opposition from mediocre minds." Einstein


Subject: Re: It is known that a correct halt decider must return false (in this case)[V4](impossibly incorrect)
From: olcott
Newsgroups: comp.theory, comp.ai.philosophy, comp.software-eng
Date: Wed, 25 Nov 2020 21:55 UTC
References: 1 2 3 4 5 6 7 8 9 10 11
Path: i2pn2.org!i2pn.org!weretis.net!feeder6.news.weretis.net!news.snarked.org!border2.nntp.dca1.giganews.com!nntp.giganews.com!buffer2.nntp.dca1.giganews.com!buffer1.nntp.dca1.giganews.com!news.giganews.com.POSTED!not-for-mail
NNTP-Posting-Date: Wed, 25 Nov 2020 15:55:09 -0600
Subject: Re: It is known that a correct halt decider must return false (in
this case)[V4](impossibly incorrect)
Newsgroups: comp.theory,comp.ai.philosophy,comp.software-eng
References: <TqWdnXCuh8jFkibCnZ2dnUU7-QfNnZ2d@giganews.com>
<he6dnVxcwNcfviHCnZ2dnUU78IfNnZ2d@brightview.co.uk>
<ndKdnaIe-v9PtCHCnZ2dnUU7-XPNnZ2d@giganews.com>
<5eGdndmbxcGA1iHCnZ2dnUU78enNnZ2d@brightview.co.uk>
<WcCdncOumL5JyCHCnZ2dnUU7-Y3NnZ2d@giganews.com>
<ToOdneeOqN8q6CHCnZ2dnUU78UfNnZ2d@brightview.co.uk>
<JuqdnaQGaYAtFCHCnZ2dnUU7-Q3NnZ2d@giganews.com>
<QrqdnS61EOtetCDCnZ2dnUU78TPNnZ2d@brightview.co.uk>
<qPCdnSYYdNW-FyPCnZ2dnUU78QHNnZ2d@brightview.co.uk>
<EOudnWsbKL0RDyPCnZ2dnUU7-SudnZ2d@giganews.com>
<M-GdnWrECtIvViPCnZ2dnUU78c_NnZ2d@brightview.co.uk>
From: NoO...@NoWhere.com (olcott)
Date: Wed, 25 Nov 2020 15:55:15 -0600
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:78.0) Gecko/20100101
Thunderbird/78.5.0
MIME-Version: 1.0
In-Reply-To: <M-GdnWrECtIvViPCnZ2dnUU78c_NnZ2d@brightview.co.uk>
Content-Type: text/plain; charset=windows-1252; format=flowed
Content-Language: en-US
Content-Transfer-Encoding: 8bit
Message-ID: <ZridnafptIUjTyPCnZ2dnUU7-UXNnZ2d@giganews.com>
Lines: 111
X-Usenet-Provider: http://www.giganews.com
X-Trace: sv3-oBNV+b/SbeZXAk1qy5oaBV8rsNHczUMG46WYvj9s8w4/6qJfeXlmvSpoIzwdvDX7uQPVqGvd7f/I/9J!OrxwRE8DU9D4l9Es9KTJ2Nox+34fx9SCrcfkKVKyJOcwCK+lofO8eDmd+sKeLzl2Dl7KuHY9aBXQ!Ug==
X-Complaints-To: abuse@giganews.com
X-DMCA-Notifications: http://www.giganews.com/info/dmca.html
X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers
X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint properly
X-Postfilter: 1.3.40
X-Original-Bytes: 6294
View all headers
On 11/25/2020 3:25 PM, Mike Terry wrote:
On 25/11/2020 17:21, olcott wrote:
On 11/25/2020 10:45 AM, Mike Terry wrote:
On 24/11/2020 15:41, Mike Terry wrote:
On 24/11/2020 04:18, olcott wrote:
<.. snip ..>

People can eventually look at all of my code and the thousands of lines
of code of the x86 emulator and they can look at the hundreds of pages
out output. It all boils down to this:

The simulator merely watches its simulation of the following
instructions until it sees a function call to 377 from 503 the second
time with no JCC (Jump-Condition_Code) in-between.


I have told you many times that your test must be UNSOUND.  You have
never responded to this, so I've assumed you don't really know whether
your test is sound or unsound (or probably, what that even means,
although I've also explained that to you before).

Now you are getting closer to actually coding the test (which you
claimed to have "fully coded" two years ago), you are finally giving
more details.

So...  what do you think.  Is the following test a SOUND test for
non-halting?

   TEST:  "monitor the simulation until there is a function
           call to 377 from 503 a second time, with no conditional
           branch inbetween"

Putting it more directly - if some calculation P(I) triggers the TEST
(so it contains two calls from 377 from 503, with no conditional branch
inbetween), does this genuinely imply that the calculation will never
halt?

Bear in mind that the two calls in question do not necessarily occur in
the same "virtual address space", that is to say the two calls can [and
in the case of T_Hat(T_Hat) *do* ] occur at /different levels of
emulation/.   [Your trace notation obscures this simple fact, making
everything appear to be in one single virtual process, when it's not.]

What do you think?  This seems to be your primary intuition that
triggered all this "refuting" activity, BUT IS IT ACTUALLY CORRECT?

Of course, you will say "All my intuitions are correct by definition -
I'm never wrong" but that doesn't make it true!  :)

Is TEST *SOUND* ?


Noted: still no response to this basic question.

Mike.

<.. snip non-response to question ..>

I'm not sure if that non-response was deliberate.  I didn't ask whether one specified implementation of [whatever] exhibits infinite recursion!

In case it was just a misreading, here is the question again.


   So...  what do you think.  Is the following test a SOUND test for
   non-halting?

      TEST:  "monitor the simulation until there is a function
              call to 377 from 503 a second time, with no conditional
              branch in-between"

It is much more generic than that.
(1) Keep a global execution trace of every line of user code.

(2) Whenever any instruction is executed see if it is a function call.

(3) If it is a function call find the prior call to this same function from the current machine address (if any) searching backward through the global execution trace and counting conditional branch instructions.

(4) If found and conditional-branch-count == zero terminate the input.

Copyright 2020 Pete Olcott (I just wrote that algorithm right now).

I had been postponing this fun task until I had the tedious task of decoding the machine language of all control flow instructions completed

   Putting it more directly - if some calculation P(I) triggers
   the TEST (so it contains two calls from 377 from 503, with no
   conditional branch in-between), does this genuinely imply that
   the calculation will never halt?

The context for this is that TEST is what you've claimed to be the test within your emulation single-step loop that you use to break the loop, determining that the input (P,I) is non-halting.

If you don't like the word "sound" just ignore that word, and read the "putting it more directly" paragraph equivalent wording!


Mike.


I like impossibly incorrect the best.

--
Copyright 2020 Pete Olcott

"Great spirits have always encountered violent opposition from mediocre minds." Einstein


Subject: Re: It is known that a correct halt decider must return false (in this case)[V4](Step 1)
From: olcott
Newsgroups: comp.theory, comp.ai.philosophy, comp.software-eng
Date: Wed, 25 Nov 2020 22:25 UTC
References: 1 2 3 4 5 6 7 8 9 10 11 12
Path: i2pn2.org!i2pn.org!aioe.org!peer01.ams4!peer.am4.highwinds-media.com!news.highwinds-media.com!tr3.eu1.usenetexpress.com!feeder.usenetexpress.com!tr3.iad1.usenetexpress.com!border1.nntp.dca1.giganews.com!nntp.giganews.com!buffer1.nntp.dca1.giganews.com!news.giganews.com.POSTED!not-for-mail
NNTP-Posting-Date: Wed, 25 Nov 2020 16:25:19 -0600
Subject: Re: It is known that a correct halt decider must return false (in this case)[V4](Step 1)
Newsgroups: comp.theory,comp.ai.philosophy,comp.software-eng
References: <TqWdnXCuh8jFkibCnZ2dnUU7-QfNnZ2d@giganews.com> <he6dnVxcwNcfviHCnZ2dnUU78IfNnZ2d@brightview.co.uk> <ndKdnaIe-v9PtCHCnZ2dnUU7-XPNnZ2d@giganews.com> <5eGdndmbxcGA1iHCnZ2dnUU78enNnZ2d@brightview.co.uk> <WcCdncOumL5JyCHCnZ2dnUU7-Y3NnZ2d@giganews.com> <87im9vpg0e.fsf@bsb.me.uk> <qoGdnW1Lz5qmByHCnZ2dnUU7-UPNnZ2d@giganews.com> <87sg8yah0c.fsf@bsb.me.uk> <Weqdnbjny8LJqSDCnZ2dnUU7-d_NnZ2d@giganews.com> <87tute8f4h.fsf@bsb.me.uk> <2aidnV9e3qQaOCDCnZ2dnUU7-c3NnZ2d@giganews.com> <87zh355bfu.fsf@bsb.me.uk>
From: NoO...@NoWhere.com (olcott)
Date: Wed, 25 Nov 2020 16:25:25 -0600
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:78.0) Gecko/20100101 Thunderbird/78.5.0
MIME-Version: 1.0
In-Reply-To: <87zh355bfu.fsf@bsb.me.uk>
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Language: en-US
Content-Transfer-Encoding: 7bit
Message-ID: <6Y6dnaUGHOdNRCPCnZ2dnUU7-fPNnZ2d@giganews.com>
Lines: 112
X-Usenet-Provider: http://www.giganews.com
X-Trace: sv3-YxIKEdnL6mJhbxZC1h2DYLCMh6OVl0DZ3kjGkILXmehUCWhFPlChhRdjN7j6BYDeU8G0yIomcION/D1!qRXPRxjFY4aPF+oebFqmdXwyuNPpby60whqaG/q9Mr7n8ku6Jnus3Vixfw9hmI1bXhPC6vEqTOi3!aA==
X-Complaints-To: abuse@giganews.com
X-DMCA-Notifications: http://www.giganews.com/info/dmca.html
X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers
X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint properly
X-Postfilter: 1.3.40
X-Original-Bytes: 5438
X-Received-Bytes: 5589
X-Received-Body-CRC: 725950246
View all headers
On 11/25/2020 4:16 PM, Ben Bacarisse wrote:
olcott <NoOne@NoWhere.com> writes:

On 11/24/2020 6:16 PM, Ben Bacarisse wrote:
olcott <NoOne@NoWhere.com> writes:

On 11/24/2020 9:53 AM, Ben Bacarisse wrote:
olcott <NoOne@NoWhere.com> writes:

On 11/23/2020 9:53 PM, Ben Bacarisse wrote:
olcott <NoOne@NoWhere.com> writes:

All that I have right now is a DebugTrace() of all the user specified
code. This provides a very obvious basis for a halt decider's correct
halting decision of the H_Hat code specified in this execution trace.

Gosh.  Is that a lie, or is that just very, very stupid?  Lying or dumb,
dumb or lying?  I can never quite tell.

Having only the code that loops around the single stepping DebugTrace()
(presumably a simple modification to someone else's emulator) is exactly
the wrong basis for a halt decider.  Its the version that makes the
"Hat" computation non-finite BY NOT BEING A DECIDER.  The "HAT"
computation you are analysing is irrelevant because it's not built on a
finite decider.

Only when you add the impossible "abort if needed" code would you have
anything that even resembles a decider.  But it's not a halt decider,
because that code has ITS OWN "HAT" computation which it decides
incorrectly.

No it does not and you know that it does not.

If you dare post the code, I'll show you, explicitly (again).

The simplified code that I posted never has been the actual code. The
actual code is far too complex to use as an example.

Line 14 requires an enormously complex set up to enable x86utm to be a
multi-tasking operating system. This was the most difficult part of
the development whole x86utm operating system.

(And line 15 is harder still.  It's either impossible or it must get an
infinity of cases wrong.  Curiously, though, it doesn't matter.  I am
happy to assume that it is 100% accurate -- no false positives or
negatives.)

08 bool Halts(u32 P, u32 I)
09 {
10   bool Halted  = false;
11   bool Aborted = false;
12   while (!Halted && !Aborted)
13   {
14     Halted  = DebugStep(P, I);
15     Aborted = Needs_To_Be_Aborted();
16   }
17   return !Aborted;
18 }

Given

    void Confound_Halts(u32 P) { if (Halts(P, P)) while (1); }

The confounding example for Halts is the computation
Confound_Halts(Confound_Halts) whose halting status is not correctly
determined by the function call Halts(Confound_Halts, Confound_Halts).

Halts(Confound_Halts, Confound_Halts) returns false.

But Confound_Halts(Confound_Halts) is a finite computation, so that's
the wrong answer (as you know perfectly well).


You start with the assumption: "Pete is wrong".
Based on this assumption you conclude that Pete is wrong".
You make sure to always skip all the steps in-between.

The first step of proof that "Pete is right" is understanding that H_Hat() never receives a return value from DebugStep().


int DebugTrace(u32 N, u32 M)
{
   ((int(*)(int))N)(M);
   return 1;
}


void H_Hat(u32 P)
{
   u32 Aborted = DebugTrace(P, P);
   if (Aborted)
     HALT
   else
     HERE: goto HERE;
}


int main()
{
   u32 P = (u32)H_Hat;
   DebugTrace(P, P);
   HALT;
}



--
Copyright 2020 Pete Olcott

"Great spirits have always encountered violent opposition from mediocre minds." Einstein


Subject: Re: It is known that a correct halt decider must return false (in this case)[V4](impossibly incorrect)
From: olcott
Newsgroups: comp.theory, comp.ai.philosophy, comp.software-eng
Date: Wed, 25 Nov 2020 23:47 UTC
References: 1 2 3 4 5 6 7 8 9 10 11 12 13
Path: i2pn2.org!i2pn.org!aioe.org!peer03.ams4!peer.am4.highwinds-media.com!peer02.iad!feed-me.highwinds-media.com!news.highwinds-media.com!border1.nntp.dca1.giganews.com!nntp.giganews.com!buffer1.nntp.dca1.giganews.com!buffer2.nntp.dca1.giganews.com!news.giganews.com.POSTED!not-for-mail
NNTP-Posting-Date: Wed, 25 Nov 2020 17:47:34 -0600
Subject: Re: It is known that a correct halt decider must return false (in
this case)[V4](impossibly incorrect)
Newsgroups: comp.theory,comp.ai.philosophy,comp.software-eng
References: <TqWdnXCuh8jFkibCnZ2dnUU7-QfNnZ2d@giganews.com>
<he6dnVxcwNcfviHCnZ2dnUU78IfNnZ2d@brightview.co.uk>
<ndKdnaIe-v9PtCHCnZ2dnUU7-XPNnZ2d@giganews.com>
<5eGdndmbxcGA1iHCnZ2dnUU78enNnZ2d@brightview.co.uk>
<WcCdncOumL5JyCHCnZ2dnUU7-Y3NnZ2d@giganews.com>
<ToOdneeOqN8q6CHCnZ2dnUU78UfNnZ2d@brightview.co.uk>
<JuqdnaQGaYAtFCHCnZ2dnUU7-Q3NnZ2d@giganews.com>
<QrqdnS61EOtetCDCnZ2dnUU78TPNnZ2d@brightview.co.uk>
<qPCdnSYYdNW-FyPCnZ2dnUU78QHNnZ2d@brightview.co.uk>
<EOudnWsbKL0RDyPCnZ2dnUU7-SudnZ2d@giganews.com>
<M-GdnWrECtIvViPCnZ2dnUU78c_NnZ2d@brightview.co.uk>
<ZridnafptIUjTyPCnZ2dnUU7-UXNnZ2d@giganews.com>
<zIudnVpmqcfEdCPCnZ2dnUU78aOdnZ2d@brightview.co.uk>
From: NoO...@NoWhere.com (olcott)
Date: Wed, 25 Nov 2020 17:47:39 -0600
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:78.0) Gecko/20100101
Thunderbird/78.5.0
MIME-Version: 1.0
In-Reply-To: <zIudnVpmqcfEdCPCnZ2dnUU78aOdnZ2d@brightview.co.uk>
Content-Type: text/plain; charset=windows-1252; format=flowed
Content-Language: en-US
Content-Transfer-Encoding: 8bit
Message-ID: <_PidnS5eJ9eLcCPCnZ2dnUU7-LfNnZ2d@giganews.com>
Lines: 113
X-Usenet-Provider: http://www.giganews.com
X-Trace: sv3-t0ciQcy/2tZmkxoYl1RYW1eCOmmxmqip/N9pxsF7XqY5hIbbV4Mk77z/uU7JWLaF56FsPWf/Gj4ApIM!zqMgqGpJC10+1kYtdQYg3uT4lFaR6YhexSZUWZZxy6WxiT9UR7zneNEOr283q587TPc+bYXIrEAj!0w==
X-Complaints-To: abuse@giganews.com
X-DMCA-Notifications: http://www.giganews.com/info/dmca.html
X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers
X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint properly
X-Postfilter: 1.3.40
X-Original-Bytes: 6489
X-Received-Bytes: 6732
X-Received-Body-CRC: 1272012187
View all headers
On 11/25/2020 5:31 PM, Mike Terry wrote:
On 25/11/2020 21:55, olcott wrote:
On 11/25/2020 3:25 PM, Mike Terry wrote:
On 25/11/2020 17:21, olcott wrote:
On 11/25/2020 10:45 AM, Mike Terry wrote:
On 24/11/2020 15:41, Mike Terry wrote:
On 24/11/2020 04:18, olcott wrote:
<.. snip ..>

People can eventually look at all of my code and the thousands of
lines
of code of the x86 emulator and they can look at the hundreds of
pages
out output. It all boils down to this:

The simulator merely watches its simulation of the following
instructions until it sees a function call to 377 from 503 the second
time with no JCC (Jump-Condition_Code) in-between.


I have told you many times that your test must be UNSOUND.  You have
never responded to this, so I've assumed you don't really know whether
your test is sound or unsound (or probably, what that even means,
although I've also explained that to you before).

Now you are getting closer to actually coding the test (which you
claimed to have "fully coded" two years ago), you are finally giving
more details.

So...  what do you think.  Is the following test a SOUND test for
non-halting?

   TEST:  "monitor the simulation until there is a function
           call to 377 from 503 a second time, with no conditional
           branch inbetween"

Putting it more directly - if some calculation P(I) triggers the TEST
(so it contains two calls from 377 from 503, with no conditional
branch
inbetween), does this genuinely imply that the calculation will never
halt?

Bear in mind that the two calls in question do not necessarily
occur in
the same "virtual address space", that is to say the two calls can
[and
in the case of T_Hat(T_Hat) *do* ] occur at /different levels of
emulation/.   [Your trace notation obscures this simple fact, making
everything appear to be in one single virtual process, when it's not.]

What do you think?  This seems to be your primary intuition that
triggered all this "refuting" activity, BUT IS IT ACTUALLY CORRECT?

Of course, you will say "All my intuitions are correct by definition -
I'm never wrong" but that doesn't make it true!  :)

Is TEST *SOUND* ?


Noted: still no response to this basic question.

Mike.

<.. snip non-response to question ..>

I'm not sure if that non-response was deliberate.  I didn't ask
whether one specified implementation of [whatever] exhibits infinite
recursion!

In case it was just a misreading, here is the question again.


   So...  what do you think.  Is the following test a SOUND test for
   non-halting?

      TEST:  "monitor the simulation until there is a function
              call to 377 from 503 a second time, with no conditional
              branch in-between"

It is much more generic than that.
(1) Keep a global execution trace of every line of user code.

(2) Whenever any instruction is executed see if it is a function call.

(3) If it is a function call find the prior call to this same function
from the current machine address (if any) searching backward through the
global execution trace and counting conditional branch instructions.

(4) If found and conditional-branch-count == zero terminate the input.

Copyright 2020 Pete Olcott (I just wrote that algorithm right now).

OK, I always imagined the test would be more general than just checking specifically for calls to 377 from 503.  :)  No problem on that front.

I'm thinking this is probably the basis of your initial intuition that you could actually detect and handle the type of recursion in your fledgeling (at that time) halt decider design.

It is good that you've clarified the test, and yet it seems you're reluctant to plainly say that you believe the test works!

logical necessity speaks for itself it doesn't need me for a cheerleader.

--
Copyright 2020 Pete Olcott

"Great spirits have always encountered violent opposition from mediocre minds." Einstein


Subject: Re: It is known that a correct halt decider must return false (in this case)[V4](Step 1)
From: olcott
Newsgroups: comp.theory, comp.ai.philosophy, comp.software-eng
Date: Wed, 25 Nov 2020 23:59 UTC
References: 1 2 3 4 5 6 7 8 9 10 11 12 13 14
Path: i2pn2.org!i2pn.org!aioe.org!news.uzoreto.com!tr3.eu1.usenetexpress.com!feeder.usenetexpress.com!tr2.iad1.usenetexpress.com!border1.nntp.dca1.giganews.com!nntp.giganews.com!buffer1.nntp.dca1.giganews.com!buffer2.nntp.dca1.giganews.com!news.giganews.com.POSTED!not-for-mail
NNTP-Posting-Date: Wed, 25 Nov 2020 17:59:08 -0600
Subject: Re: It is known that a correct halt decider must return false (in this case)[V4](Step 1)
Newsgroups: comp.theory,comp.ai.philosophy,comp.software-eng
References: <TqWdnXCuh8jFkibCnZ2dnUU7-QfNnZ2d@giganews.com> <he6dnVxcwNcfviHCnZ2dnUU78IfNnZ2d@brightview.co.uk> <ndKdnaIe-v9PtCHCnZ2dnUU7-XPNnZ2d@giganews.com> <5eGdndmbxcGA1iHCnZ2dnUU78enNnZ2d@brightview.co.uk> <WcCdncOumL5JyCHCnZ2dnUU7-Y3NnZ2d@giganews.com> <87im9vpg0e.fsf@bsb.me.uk> <qoGdnW1Lz5qmByHCnZ2dnUU7-UPNnZ2d@giganews.com> <87sg8yah0c.fsf@bsb.me.uk> <Weqdnbjny8LJqSDCnZ2dnUU7-d_NnZ2d@giganews.com> <87tute8f4h.fsf@bsb.me.uk> <2aidnV9e3qQaOCDCnZ2dnUU7-c3NnZ2d@giganews.com> <87zh355bfu.fsf@bsb.me.uk> <6Y6dnaUGHOdNRCPCnZ2dnUU7-fPNnZ2d@giganews.com> <0TBvH.159998$gR8.40967@fx45.iad>
From: NoO...@NoWhere.com (olcott)
Date: Wed, 25 Nov 2020 17:59:11 -0600
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:78.0) Gecko/20100101 Thunderbird/78.5.0
MIME-Version: 1.0
In-Reply-To: <0TBvH.159998$gR8.40967@fx45.iad>
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Language: en-US
Content-Transfer-Encoding: 8bit
Message-ID: <edGdnZFDhqBRciPCnZ2dnUU7-fnNnZ2d@giganews.com>
Lines: 154
X-Usenet-Provider: http://www.giganews.com
X-Trace: sv3-kC3xBIBwWARGWfJawGaHm4q0OTmo68Aiq49N3rrVsbI1ADZOEKTlOdms9yafQ3oNtOakHGzUHPikLRH!+q/KuCWcIoNbv19q8I1f+lxUwe1jzxcTErk4Ha0A3dY1H0qwhzjfFSPFQUFFfI51BXS+DT2VcJMc!rQ==
X-Complaints-To: abuse@giganews.com
X-DMCA-Notifications: http://www.giganews.com/info/dmca.html
X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers
X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint properly
X-Postfilter: 1.3.40
X-Original-Bytes: 7138
View all headers
On 11/25/2020 5:35 PM, Richard Damon wrote:
On 11/25/20 5:25 PM, olcott wrote:
On 11/25/2020 4:16 PM, Ben Bacarisse wrote:
olcott <NoOne@NoWhere.com> writes:

On 11/24/2020 6:16 PM, Ben Bacarisse wrote:
olcott <NoOne@NoWhere.com> writes:

On 11/24/2020 9:53 AM, Ben Bacarisse wrote:
olcott <NoOne@NoWhere.com> writes:

On 11/23/2020 9:53 PM, Ben Bacarisse wrote:
olcott <NoOne@NoWhere.com> writes:

All that I have right now is a DebugTrace() of all the user
specified
code. This provides a very obvious basis for a halt decider's
correct
halting decision of the H_Hat code specified in this execution
trace.

Gosh.  Is that a lie, or is that just very, very stupid?  Lying
or dumb,
dumb or lying?  I can never quite tell.

Having only the code that loops around the single stepping
DebugTrace()
(presumably a simple modification to someone else's emulator) is
exactly
the wrong basis for a halt decider.  Its the version that makes the
"Hat" computation non-finite BY NOT BEING A DECIDER.  The "HAT"
computation you are analysing is irrelevant because it's not
built on a
finite decider.

Only when you add the impossible "abort if needed" code would
you have
anything that even resembles a decider.  But it's not a halt
decider,
because that code has ITS OWN "HAT" computation which it decides
incorrectly.

No it does not and you know that it does not.

If you dare post the code, I'll show you, explicitly (again).

The simplified code that I posted never has been the actual code. The
actual code is far too complex to use as an example.

Line 14 requires an enormously complex set up to enable x86utm to be a
multi-tasking operating system. This was the most difficult part of
the development whole x86utm operating system.

(And line 15 is harder still.  It's either impossible or it must get an
infinity of cases wrong.  Curiously, though, it doesn't matter.  I am
happy to assume that it is 100% accurate -- no false positives or
negatives.)

08 bool Halts(u32 P, u32 I)
09 {
10   bool Halted  = false;
11   bool Aborted = false;
12   while (!Halted && !Aborted)
13   {
14     Halted  = DebugStep(P, I);
15     Aborted = Needs_To_Be_Aborted();
16   }
17   return !Aborted;
18 }

Given

     void Confound_Halts(u32 P) { if (Halts(P, P)) while (1); }

The confounding example for Halts is the computation
Confound_Halts(Confound_Halts) whose halting status is not correctly
determined by the function call Halts(Confound_Halts, Confound_Halts).

Halts(Confound_Halts, Confound_Halts) returns false.

But Confound_Halts(Confound_Halts) is a finite computation, so that's
the wrong answer (as you know perfectly well).


You start with the assumption: "Pete is wrong".
Based on this assumption you conclude that Pete is wrong".
You make sure to always skip all the steps in-between.

The counter does NOT start with the assumption of Pete is wrong, the

Both Ben and Jeff start with the assumption that "Pete is wrong" and from this assumption they conclude that "Pete is wrong" making sure to avoid any reasoning in-between.

counter starts with the knowledge that we have a test we can run to see
what happens, (And happens to know one that this Halts will fail), and
then runs the test and sees the failure.

In your case my examples were not written clearly enough.


The first step of proof that "Pete is right" is understanding that
H_Hat() never receives a return value from DebugStep().


But it isn't Confounds_Halts problem that Halts never gave its answer in

Again I tell you that the relationship between Halts() and H_Hat is the same as the relationship between DebugTrace() and H_Hat.

H_Hat never gets any answer from either one of them entirely on the basis the a fault of H_Hat.

its emulation to those that needed it for Halts to figure the answer. It
is Halts problem to figure out how to do it, and it did it wrong.

Yes, you 'proof' seems to start with the (baseless) assumption that you
have the right answer, but never establishes that there even is one.


int DebugTrace(u32 N, u32 M)
{
   ((int(*)(int))N)(M);
   return 1;
}


void H_Hat(u32 P)
{
   u32 Aborted = DebugTrace(P, P);
   if (Aborted)
     HALT
   else
     HERE: goto HERE;
}


int main()
{
   u32 P = (u32)H_Hat;
   DebugTrace(P, P);
   HALT;
}






--
Copyright 2020 Pete Olcott

"Great spirits have always encountered violent opposition from mediocre minds." Einstein


Subject: Re: It is known that a correct halt decider must return false (in this case)[V4](Step 1)
From: olcott
Newsgroups: comp.theory, comp.ai.philosophy, comp.software-eng
Date: Thu, 26 Nov 2020 00:09 UTC
References: 1 2 3 4 5 6 7 8 9 10 11 12 13 14
Path: i2pn2.org!i2pn.org!weretis.net!feeder6.news.weretis.net!news.snarked.org!border2.nntp.dca1.giganews.com!nntp.giganews.com!buffer2.nntp.dca1.giganews.com!news.giganews.com.POSTED!not-for-mail
NNTP-Posting-Date: Wed, 25 Nov 2020 18:09:05 -0600
Subject: Re: It is known that a correct halt decider must return false (in
this case)[V4](Step 1)
Newsgroups: comp.theory,comp.ai.philosophy,comp.software-eng
References: <TqWdnXCuh8jFkibCnZ2dnUU7-QfNnZ2d@giganews.com>
<he6dnVxcwNcfviHCnZ2dnUU78IfNnZ2d@brightview.co.uk>
<ndKdnaIe-v9PtCHCnZ2dnUU7-XPNnZ2d@giganews.com>
<5eGdndmbxcGA1iHCnZ2dnUU78enNnZ2d@brightview.co.uk>
<WcCdncOumL5JyCHCnZ2dnUU7-Y3NnZ2d@giganews.com> <87im9vpg0e.fsf@bsb.me.uk>
<qoGdnW1Lz5qmByHCnZ2dnUU7-UPNnZ2d@giganews.com> <87sg8yah0c.fsf@bsb.me.uk>
<Weqdnbjny8LJqSDCnZ2dnUU7-d_NnZ2d@giganews.com> <87tute8f4h.fsf@bsb.me.uk>
<2aidnV9e3qQaOCDCnZ2dnUU7-c3NnZ2d@giganews.com> <87zh355bfu.fsf@bsb.me.uk>
<6Y6dnaUGHOdNRCPCnZ2dnUU7-fPNnZ2d@giganews.com>
<a96f0b13-00c4-482d-8069-06194379e897n@googlegroups.com>
From: NoO...@NoWhere.com (olcott)
Date: Wed, 25 Nov 2020 18:09:10 -0600
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:78.0) Gecko/20100101
Thunderbird/78.5.0
MIME-Version: 1.0
In-Reply-To: <a96f0b13-00c4-482d-8069-06194379e897n@googlegroups.com>
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Language: en-US
Content-Transfer-Encoding: 7bit
Message-ID: <bImdncgVvYW8byPCnZ2dnUU7-IfNnZ2d@giganews.com>
Lines: 74
X-Usenet-Provider: http://www.giganews.com
X-Trace: sv3-NQfauFpq3Qp56WuA+NY0fgWetxAwMoM+6lNKmZ//qAOqTQzryFSruZN/yxbA6Ej3vVXGRR/NxOFKvgm!pZoZxKRbt/HpkWuI1baB+OnRGFzkuh5L8P/AXq243u96KfB7FXH6DotDGy1/qtmAf6z08cI35lsJ!MA==
X-Complaints-To: abuse@giganews.com
X-DMCA-Notifications: http://www.giganews.com/info/dmca.html
X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers
X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint properly
X-Postfilter: 1.3.40
X-Original-Bytes: 3583
View all headers
On 11/25/2020 5:53 PM, dklei...@gmail.com wrote:
On Wednesday, November 25, 2020 at 2:25:27 PM UTC-8, olcott wrote:
You start with the assumption: "Pete is wrong".
Based on this assumption you conclude that Pete is wrong".
You make sure to always skip all the steps in-between.

The first step of proof that "Pete is right" is understanding that
H_Hat() never receives a return value from DebugStep().

That's true in any empty way. Is DebugStep a thinko for DebufTrace?


I can't make out what you are saying.

That H_Hat() never gets a return value fro DebugTrace() is true in a logical necessity kind of way.

int DebugTrace(u32 N, u32 M)
{
((int(*)(int))N)(M);
return 1;
}
  // So DebugTrace always returns 1 regardless of its inputs.

Only if its input ever halts.

void H_Hat(u32 P)
{
u32 Aborted = DebugTrace(P, P);

// Setting initial value of Aborted to 1

if (Aborted)
HALT


// Execution always reaches here but I don't know what "HALT" signifies. Perhaps I am using the wrong version of C

Execution NEVER reaches here
#define HALT __asm hlt  // Force the program to Halt

else
HERE: goto HERE;

// Never happens.

}


int main()
{
u32 P = (u32)H_Hat;
DebugTrace(P, P);
HALT;


// I still don't know what HALT does.
#define HALT __asm hlt  // Force the program to Halt


}

The code is infinitely recursive.
It calls DebugTrace() to call H_Hat
to call  DebugTrace() to call H_Hat...



--
Copyright 2020 Pete Olcott

"Great spirits have always encountered violent opposition from mediocre minds." Einstein


Subject: Re: It is known that a correct halt decider must return false (in this case)[V4](impossibly incorrect)
From: olcott
Newsgroups: comp.theory, comp.ai.philosophy, comp.software-eng
Date: Thu, 26 Nov 2020 00:51 UTC
References: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15
Path: i2pn2.org!i2pn.org!weretis.net!feeder6.news.weretis.net!news.snarked.org!border2.nntp.dca1.giganews.com!nntp.giganews.com!buffer2.nntp.dca1.giganews.com!buffer1.nntp.dca1.giganews.com!news.giganews.com.POSTED!not-for-mail
NNTP-Posting-Date: Wed, 25 Nov 2020 18:51:47 -0600
Subject: Re: It is known that a correct halt decider must return false (in
this case)[V4](impossibly incorrect)
Newsgroups: comp.theory,comp.ai.philosophy,comp.software-eng
References: <TqWdnXCuh8jFkibCnZ2dnUU7-QfNnZ2d@giganews.com>
<he6dnVxcwNcfviHCnZ2dnUU78IfNnZ2d@brightview.co.uk>
<ndKdnaIe-v9PtCHCnZ2dnUU7-XPNnZ2d@giganews.com>
<5eGdndmbxcGA1iHCnZ2dnUU78enNnZ2d@brightview.co.uk>
<WcCdncOumL5JyCHCnZ2dnUU7-Y3NnZ2d@giganews.com>
<ToOdneeOqN8q6CHCnZ2dnUU78UfNnZ2d@brightview.co.uk>
<JuqdnaQGaYAtFCHCnZ2dnUU7-Q3NnZ2d@giganews.com>
<QrqdnS61EOtetCDCnZ2dnUU78TPNnZ2d@brightview.co.uk>
<qPCdnSYYdNW-FyPCnZ2dnUU78QHNnZ2d@brightview.co.uk>
<EOudnWsbKL0RDyPCnZ2dnUU7-SudnZ2d@giganews.com>
<M-GdnWrECtIvViPCnZ2dnUU78c_NnZ2d@brightview.co.uk>
<ZridnafptIUjTyPCnZ2dnUU7-UXNnZ2d@giganews.com>
<zIudnVpmqcfEdCPCnZ2dnUU78aOdnZ2d@brightview.co.uk>
<_PidnS5eJ9eLcCPCnZ2dnUU7-LfNnZ2d@giganews.com>
<Iqmdnbz55_xraiPCnZ2dnUU78V-dnZ2d@brightview.co.uk>
From: NoO...@NoWhere.com (olcott)
Date: Wed, 25 Nov 2020 18:51:53 -0600
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:78.0) Gecko/20100101
Thunderbird/78.5.0
MIME-Version: 1.0
In-Reply-To: <Iqmdnbz55_xraiPCnZ2dnUU78V-dnZ2d@brightview.co.uk>
Content-Type: text/plain; charset=windows-1252; format=flowed
Content-Language: en-US
Content-Transfer-Encoding: 8bit
Message-ID: <zf6dnTkZ6Pi-YSPCnZ2dnUU7-TudnZ2d@giganews.com>
Lines: 135
X-Usenet-Provider: http://www.giganews.com
X-Trace: sv3-0ce1IbMV/RTpAbF7XAsx5K1Z9ZAynVa0xgXtW9IA3T3U3lv06C2fgeQ82RQFgUCIx1Th//CvexQlRjL!j23x2TXKSwkIRxa1FpxWaOOKG8bDruM17QqanDYbWQyNT3tmpxkTxO8/NHiXbNseRrHDiVJknVLu!qQ==
X-Complaints-To: abuse@giganews.com
X-DMCA-Notifications: http://www.giganews.com/info/dmca.html
X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers
X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint properly
X-Postfilter: 1.3.40
X-Original-Bytes: 7235
View all headers
On 11/25/2020 6:33 PM, Mike Terry wrote:
On 25/11/2020 23:47, olcott wrote:
On 11/25/2020 5:31 PM, Mike Terry wrote:
On 25/11/2020 21:55, olcott wrote:
On 11/25/2020 3:25 PM, Mike Terry wrote:
On 25/11/2020 17:21, olcott wrote:
On 11/25/2020 10:45 AM, Mike Terry wrote:
On 24/11/2020 15:41, Mike Terry wrote:
On 24/11/2020 04:18, olcott wrote:
<.. snip ..>

People can eventually look at all of my code and the thousands of
lines
of code of the x86 emulator and they can look at the hundreds of
pages
out output. It all boils down to this:

The simulator merely watches its simulation of the following
instructions until it sees a function call to 377 from 503 the
second
time with no JCC (Jump-Condition_Code) in-between.


I have told you many times that your test must be UNSOUND.  You have
never responded to this, so I've assumed you don't really know
whether
your test is sound or unsound (or probably, what that even means,
although I've also explained that to you before).

Now you are getting closer to actually coding the test (which you
claimed to have "fully coded" two years ago), you are finally giving
more details.

So...  what do you think.  Is the following test a SOUND test for
non-halting?

   TEST:  "monitor the simulation until there is a function
           call to 377 from 503 a second time, with no conditional
           branch inbetween"

Putting it more directly - if some calculation P(I) triggers the
TEST
(so it contains two calls from 377 from 503, with no conditional
branch
inbetween), does this genuinely imply that the calculation will
never
halt?

Bear in mind that the two calls in question do not necessarily
occur in
the same "virtual address space", that is to say the two calls can
[and
in the case of T_Hat(T_Hat) *do* ] occur at /different levels of
emulation/.   [Your trace notation obscures this simple fact, making
everything appear to be in one single virtual process, when it's
not.]

What do you think?  This seems to be your primary intuition that
triggered all this "refuting" activity, BUT IS IT ACTUALLY CORRECT?

Of course, you will say "All my intuitions are correct by
definition -
I'm never wrong" but that doesn't make it true!  :)

Is TEST *SOUND* ?


Noted: still no response to this basic question.

Mike.

<.. snip non-response to question ..>

I'm not sure if that non-response was deliberate.  I didn't ask
whether one specified implementation of [whatever] exhibits infinite
recursion!

In case it was just a misreading, here is the question again.


   So...  what do you think.  Is the following test a SOUND test for
   non-halting?

      TEST:  "monitor the simulation until there is a function
              call to 377 from 503 a second time, with no conditional
              branch in-between"

It is much more generic than that.
(1) Keep a global execution trace of every line of user code.

(2) Whenever any instruction is executed see if it is a function call.

(3) If it is a function call find the prior call to this same function
from the current machine address (if any) searching backward through the
global execution trace and counting conditional branch instructions.

(4) If found and conditional-branch-count == zero terminate the input.

Copyright 2020 Pete Olcott (I just wrote that algorithm right now).

OK, I always imagined the test would be more general than just
checking specifically for calls to 377 from 503.  :)  No problem on
that front.

I'm thinking this is probably the basis of your initial intuition that
you could actually detect and handle the type of recursion in your
fledgeling (at that time) halt decider design.

It is good that you've clarified the test, and yet it seems you're
reluctant to plainly say that you believe the test works!

logical necessity speaks for itself it doesn't need me for a cheerleader.


LOL.  I knew you'd do something like that.

OK, so you are saying that if your test detects the behaviour described, then it's a "logical necessity" that the input being examined is non-halting?

Yes that is what I am saying.

Can you find a counter-example?



--
Copyright 2020 Pete Olcott

"Great spirits have always encountered violent opposition from mediocre minds." Einstein


Subject: Re: It is known that a correct halt decider must return false (in this case)[V4](Step 1)
From: olcott
Newsgroups: comp.theory, comp.ai.philosophy
Date: Thu, 26 Nov 2020 01:03 UTC
References: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16
Path: i2pn2.org!i2pn.org!paganini.bofh.team!news.dns-netz.com!news.freedyn.net!newsfeed.xs4all.nl!newsfeed7.news.xs4all.nl!tr2.eu1.usenetexpress.com!feeder.usenetexpress.com!tr1.iad1.usenetexpress.com!border1.nntp.dca1.giganews.com!nntp.giganews.com!buffer1.nntp.dca1.giganews.com!news.giganews.com.POSTED!not-for-mail
NNTP-Posting-Date: Wed, 25 Nov 2020 19:03:18 -0600
Subject: Re: It is known that a correct halt decider must return false (in this case)[V4](Step 1)
Newsgroups: comp.theory,comp.ai.philosophy
References: <TqWdnXCuh8jFkibCnZ2dnUU7-QfNnZ2d@giganews.com> <he6dnVxcwNcfviHCnZ2dnUU78IfNnZ2d@brightview.co.uk> <ndKdnaIe-v9PtCHCnZ2dnUU7-XPNnZ2d@giganews.com> <5eGdndmbxcGA1iHCnZ2dnUU78enNnZ2d@brightview.co.uk> <WcCdncOumL5JyCHCnZ2dnUU7-Y3NnZ2d@giganews.com> <87im9vpg0e.fsf@bsb.me.uk> <qoGdnW1Lz5qmByHCnZ2dnUU7-UPNnZ2d@giganews.com> <87sg8yah0c.fsf@bsb.me.uk> <Weqdnbjny8LJqSDCnZ2dnUU7-d_NnZ2d@giganews.com> <87tute8f4h.fsf@bsb.me.uk> <2aidnV9e3qQaOCDCnZ2dnUU7-c3NnZ2d@giganews.com> <87zh355bfu.fsf@bsb.me.uk> <6Y6dnaUGHOdNRCPCnZ2dnUU7-fPNnZ2d@giganews.com> <0TBvH.159998$gR8.40967@fx45.iad> <edGdnZFDhqBRciPCnZ2dnUU7-fnNnZ2d@giganews.com> <c2DvH.160002$gR8.79102@fx45.iad>
From: NoO...@NoWhere.com (olcott)
Date: Wed, 25 Nov 2020 19:03:24 -0600
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:78.0) Gecko/20100101 Thunderbird/78.5.0
MIME-Version: 1.0
In-Reply-To: <c2DvH.160002$gR8.79102@fx45.iad>
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Language: en-US
Content-Transfer-Encoding: 8bit
Message-ID: <0NmdnQTOBvJLYyPCnZ2dnUU7-YOdnZ2d@giganews.com>
Lines: 203
X-Usenet-Provider: http://www.giganews.com
X-Trace: sv3-9VmUhHu5Lvi9RVIh/33PIc9ONNO9Hj/KkB4XAAE0CLMbvmFkrmLoy1aOy+dM5KaZ2osDbq9M0AdIx+4!Xu+/KAS/S4a8eTBaND3PclFsypU30hayFRJgnCaygaVh/u/itPuof8Azbq3xlCeoDDbWRwT5dnMW!iQ==
X-Complaints-To: abuse@giganews.com
X-DMCA-Notifications: http://www.giganews.com/info/dmca.html
X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers
X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint properly
X-Postfilter: 1.3.40
X-Original-Bytes: 9395
View all headers
On 11/25/2020 6:55 PM, Richard Damon wrote:
On 11/25/20 6:59 PM, olcott wrote:
On 11/25/2020 5:35 PM, Richard Damon wrote:
On 11/25/20 5:25 PM, olcott wrote:
On 11/25/2020 4:16 PM, Ben Bacarisse wrote:
olcott <NoOne@NoWhere.com> writes:

On 11/24/2020 6:16 PM, Ben Bacarisse wrote:
olcott <NoOne@NoWhere.com> writes:

On 11/24/2020 9:53 AM, Ben Bacarisse wrote:
olcott <NoOne@NoWhere.com> writes:

On 11/23/2020 9:53 PM, Ben Bacarisse wrote:
olcott <NoOne@NoWhere.com> writes:

All that I have right now is a DebugTrace() of all the user
specified
code. This provides a very obvious basis for a halt decider's
correct
halting decision of the H_Hat code specified in this execution
trace.

Gosh.  Is that a lie, or is that just very, very stupid?  Lying
or dumb,
dumb or lying?  I can never quite tell.

Having only the code that loops around the single stepping
DebugTrace()
(presumably a simple modification to someone else's emulator) is
exactly
the wrong basis for a halt decider.  Its the version that
makes the
"Hat" computation non-finite BY NOT BEING A DECIDER.  The "HAT"
computation you are analysing is irrelevant because it's not
built on a
finite decider.

Only when you add the impossible "abort if needed" code would
you have
anything that even resembles a decider.  But it's not a halt
decider,
because that code has ITS OWN "HAT" computation which it decides
incorrectly.

No it does not and you know that it does not.

If you dare post the code, I'll show you, explicitly (again).

The simplified code that I posted never has been the actual code.
The
actual code is far too complex to use as an example.

Line 14 requires an enormously complex set up to enable x86utm to
be a
multi-tasking operating system. This was the most difficult part of
the development whole x86utm operating system.

(And line 15 is harder still.  It's either impossible or it must
get an
infinity of cases wrong.  Curiously, though, it doesn't matter.  I am
happy to assume that it is 100% accurate -- no false positives or
negatives.)

08 bool Halts(u32 P, u32 I)
09 {
10   bool Halted  = false;
11   bool Aborted = false;
12   while (!Halted && !Aborted)
13   {
14     Halted  = DebugStep(P, I);
15     Aborted = Needs_To_Be_Aborted();
16   }
17   return !Aborted;
18 }

Given

      void Confound_Halts(u32 P) { if (Halts(P, P)) while (1); }

The confounding example for Halts is the computation
Confound_Halts(Confound_Halts) whose halting status is not correctly
determined by the function call Halts(Confound_Halts,
Confound_Halts).

Halts(Confound_Halts, Confound_Halts) returns false.

But Confound_Halts(Confound_Halts) is a finite computation, so that's
the wrong answer (as you know perfectly well).


You start with the assumption: "Pete is wrong".
Based on this assumption you conclude that Pete is wrong".
You make sure to always skip all the steps in-between.

The counter does NOT start with the assumption of Pete is wrong, the

Both Ben and Jeff start with the assumption that "Pete is wrong" and
from this assumption they conclude that "Pete is wrong" making sure to
avoid any reasoning in-between.

But I am not they (not sure they really are starting that way either).

We all start KNOWING you are wrong, but the arguements aren't based on
that. Otherwise the response would just be Linz says your wrong.

counter starts with the knowledge that we have a test we can run to see
what happens, (And happens to know one that this Halts will fail), and
then runs the test and sees the failure.

In your case my examples were not written clearly enough.

Since ultimately, to my understand, you really only have one 'example'
of a Halting Decider you need to present, so all you really need to do
is show it.

A big part of the issue is that you want to try to first reason out with
people so they will accept your arguements before you want to let them
test you decider. The problem is that they don't need to accept your
logic to test it, the just need to know what it actually does.

Now, if you were to change your tack and accept that you are not
thinking of the same halting problem that everyone else uses, make that
clear to everyone, and by doing so accept that you results aren't
applicable to anything that wants the classic halting problem, then you
would need to explain your ideas about why and what and really define
the problem you are trying to solve.

One big piece of that is that if you are no longer working on the
classical halting problem, Linz can just go away if you define your
problem right. This sort of seems what you are trying to do, only you
aren't accepting that you are doing a different problem.

You CAN'T just define yourself around Linz and still be doing the
classical halting problem.



The first step of proof that "Pete is right" is understanding that
H_Hat() never receives a return value from DebugStep().


But it isn't Confounds_Halts problem that Halts never gave its answer in

Again I tell you that the relationship between Halts() and H_Hat is the
same as the relationship between DebugTrace() and H_Hat.

H_Hat never gets any answer from either one of them entirely on the
basis the a fault of H_Hat.

Since it is Halts responsibility to give an answer to any and every
quetion posed to it, it gets hard to blame the lowly input that just
came to be tested.


Clearly you have a fundamental lack of understanding of infinite recursion.


its emulation to those that needed it for Halts to figure the answer. It
is Halts problem to figure out how to do it, and it did it wrong.

Yes, you 'proof' seems to start with the (baseless) assumption that you
have the right answer, but never establishes that there even is one.


int DebugTrace(u32 N, u32 M)
{
    ((int(*)(int))N)(M);
    return 1;
}


void H_Hat(u32 P)
{
    u32 Aborted = DebugTrace(P, P);
    if (Aborted)
      HALT
    else
      HERE: goto HERE;
}


int main()
{
    u32 P = (u32)H_Hat;
    DebugTrace(P, P);
    HALT;
}









--
Copyright 2020 Pete Olcott

"Great spirits have always encountered violent opposition from mediocre minds." Einstein


Subject: Re: It is known that a correct halt decider must return false (in this case)[V4](impossibly incorrect)
From: olcott
Newsgroups: comp.theory, comp.ai.philosophy, comp.software-eng
Date: Thu, 26 Nov 2020 02:14 UTC
References: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17
Path: i2pn2.org!i2pn.org!aioe.org!peer01.ams4!peer.am4.highwinds-media.com!news.highwinds-media.com!newsfeed.xs4all.nl!newsfeed7.news.xs4all.nl!feeder5.feed.usenet.farm!feeder1.feed.usenet.farm!feed.usenet.farm!feeder.usenetexpress.com!tr3.iad1.usenetexpress.com!border1.nntp.dca1.giganews.com!nntp.giganews.com!buffer1.nntp.dca1.giganews.com!news.giganews.com.POSTED!not-for-mail
NNTP-Posting-Date: Wed, 25 Nov 2020 20:14:48 -0600
Subject: Re: It is known that a correct halt decider must return false (in this case)[V4](impossibly incorrect)
Newsgroups: comp.theory,comp.ai.philosophy,comp.software-eng
References: <TqWdnXCuh8jFkibCnZ2dnUU7-QfNnZ2d@giganews.com> <he6dnVxcwNcfviHCnZ2dnUU78IfNnZ2d@brightview.co.uk> <ndKdnaIe-v9PtCHCnZ2dnUU7-XPNnZ2d@giganews.com> <5eGdndmbxcGA1iHCnZ2dnUU78enNnZ2d@brightview.co.uk> <WcCdncOumL5JyCHCnZ2dnUU7-Y3NnZ2d@giganews.com> <ToOdneeOqN8q6CHCnZ2dnUU78UfNnZ2d@brightview.co.uk> <JuqdnaQGaYAtFCHCnZ2dnUU7-Q3NnZ2d@giganews.com> <QrqdnS61EOtetCDCnZ2dnUU78TPNnZ2d@brightview.co.uk> <qPCdnSYYdNW-FyPCnZ2dnUU78QHNnZ2d@brightview.co.uk> <EOudnWsbKL0RDyPCnZ2dnUU7-SudnZ2d@giganews.com> <M-GdnWrECtIvViPCnZ2dnUU78c_NnZ2d@brightview.co.uk> <ZridnafptIUjTyPCnZ2dnUU7-UXNnZ2d@giganews.com> <zIudnVpmqcfEdCPCnZ2dnUU78aOdnZ2d@brightview.co.uk> <_PidnS5eJ9eLcCPCnZ2dnUU7-LfNnZ2d@giganews.com> <Iqmdnbz55_xraiPCnZ2dnUU78V-dnZ2d@brightview.co.uk> <zf6dnTkZ6Pi-YSPCnZ2dnUU7-TudnZ2d@giganews.com> <OPKdncr_54uPmiLCnZ2dnUU78QednZ2d@brightview.co.uk>
From: NoO...@NoWhere.com (olcott)
Date: Wed, 25 Nov 2020 20:14:53 -0600
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:78.0) Gecko/20100101 Thunderbird/78.5.0
MIME-Version: 1.0
In-Reply-To: <OPKdncr_54uPmiLCnZ2dnUU78QednZ2d@brightview.co.uk>
Content-Type: text/plain; charset=windows-1252; format=flowed
Content-Language: en-US
Content-Transfer-Encoding: 8bit
Message-ID: <NfidnR1APKUFkiLCnZ2dnUU7-b_NnZ2d@giganews.com>
Lines: 198
X-Usenet-Provider: http://www.giganews.com
X-Trace: sv3-ggOkCAnsIKwJlawJsZgFYk3Dqix9kbPIc4izlheGEpBPqELMFEO3trt2ZvJhSUXrEJc9bp/bBKPNhLy!btpIyjavV7FyZMBvuElNDsN9EEaRwK7zG0bhsQfD370NlINvtL9JQshNB+3SKLEObqd7xzvFClsp!QA==
X-Complaints-To: abuse@giganews.com
X-DMCA-Notifications: http://www.giganews.com/info/dmca.html
X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers
X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint properly
X-Postfilter: 1.3.40
X-Original-Bytes: 9716
X-Received-Bytes: 9934
X-Received-Body-CRC: 3279782100
View all headers
On 11/25/2020 7:38 PM, Mike Terry wrote:
On 26/11/2020 00:51, olcott wrote:
On 11/25/2020 6:33 PM, Mike Terry wrote:
On 25/11/2020 23:47, olcott wrote:
On 11/25/2020 5:31 PM, Mike Terry wrote:
On 25/11/2020 21:55, olcott wrote:
On 11/25/2020 3:25 PM, Mike Terry wrote:
On 25/11/2020 17:21, olcott wrote:
On 11/25/2020 10:45 AM, Mike Terry wrote:
On 24/11/2020 15:41, Mike Terry wrote:
On 24/11/2020 04:18, olcott wrote:
<.. snip ..>

People can eventually look at all of my code and the thousands of
lines
of code of the x86 emulator and they can look at the hundreds of
pages
out output. It all boils down to this:

The simulator merely watches its simulation of the following
instructions until it sees a function call to 377 from 503 the
second
time with no JCC (Jump-Condition_Code) in-between.


I have told you many times that your test must be UNSOUND.  You
have
never responded to this, so I've assumed you don't really know
whether
your test is sound or unsound (or probably, what that even means,
although I've also explained that to you before).

Now you are getting closer to actually coding the test (which you
claimed to have "fully coded" two years ago), you are finally
giving
more details.

So...  what do you think.  Is the following test a SOUND test for
non-halting?

   TEST:  "monitor the simulation until there is a function
           call to 377 from 503 a second time, with no conditional
           branch inbetween"

Putting it more directly - if some calculation P(I) triggers the
TEST
(so it contains two calls from 377 from 503, with no conditional
branch
inbetween), does this genuinely imply that the calculation will
never
halt?

Bear in mind that the two calls in question do not necessarily
occur in
the same "virtual address space", that is to say the two calls can
[and
in the case of T_Hat(T_Hat) *do* ] occur at /different levels of
emulation/.   [Your trace notation obscures this simple fact,
making
everything appear to be in one single virtual process, when it's
not.]

What do you think?  This seems to be your primary intuition that
triggered all this "refuting" activity, BUT IS IT ACTUALLY
CORRECT?

Of course, you will say "All my intuitions are correct by
definition -
I'm never wrong" but that doesn't make it true!  :)

Is TEST *SOUND* ?


Noted: still no response to this basic question.

Mike.

<.. snip non-response to question ..>

I'm not sure if that non-response was deliberate.  I didn't ask
whether one specified implementation of [whatever] exhibits infinite
recursion!

In case it was just a misreading, here is the question again.


   So...  what do you think.  Is the following test a SOUND test for
   non-halting?

      TEST:  "monitor the simulation until there is a function
              call to 377 from 503 a second time, with no conditional
              branch in-between"

It is much more generic than that.
(1) Keep a global execution trace of every line of user code.

(2) Whenever any instruction is executed see if it is a function call.

(3) If it is a function call find the prior call to this same function
from the current machine address (if any) searching backward
through the
global execution trace and counting conditional branch instructions.

(4) If found and conditional-branch-count == zero terminate the input.

Copyright 2020 Pete Olcott (I just wrote that algorithm right now).

OK, I always imagined the test would be more general than just
checking specifically for calls to 377 from 503.  :)  No problem on
that front.

I'm thinking this is probably the basis of your initial intuition that
you could actually detect and handle the type of recursion in your
fledgeling (at that time) halt decider design.

It is good that you've clarified the test, and yet it seems you're
reluctant to plainly say that you believe the test works!

logical necessity speaks for itself it doesn't need me for a
cheerleader.


LOL.  I knew you'd do something like that.

OK, so you are saying that if your test detects the behaviour
described, then it's a "logical necessity" that the input being
examined is non-halting?

Yes that is what I am saying.

There - that wasn't so bad, was it?  :)


Can you find a counter-example?

Well, if it's a logical necessity I'm in for a hard time on that one...

But here's the point:  logical necessity absolutely /does/ need a cheerleader!  Loads of things are "logically necessary" in that they must logically be true, and yet they are not /obviously/ true.  That's why we have proofs.

This would be one of those scenarios, where even if your claim is correct, it's not trivially obvious that it's correct, right?

Here is what we're saying:

TEST:
    If a calculation P(I) has a trace of steps
    (s0, s1, s2, s3, .....) and there are two steps s_i
    and s_j, such that si and sj are both unconditional
    branches from A to B, and none of the steps in-between
    s_i and s_j are conditional branches, THEN calculation
    P(I) never halts.

Well that's certainly not a "trivial restatement of word meanings" or similar, and so is not seen to correct just on a casual glance.

So obviously where I'm going is : do you have a proof of this?

Now I know you're not one for proofs, and maybe during the course of discussion such a proof will fall out (provided the underlying logic is correct...)

So to start with, perhaps you can just give your thinking as to /why/ you believe it to be logically necessary?  [You clearly didn't wake up one day and think "hey, what about TEST - oh! it's a logical necessity, that's handy - I can use it in my halt decider!".  There was something that led you to consider TEST, and having considered it, you decided for whatever reason it was true...]


Mike.


Let's look at it a little simpler:
HERE:  // current location
   Instructions that cannot possibly exit a loop
THERE: goto HERE;

Can you see how this definitely loops?

The next step is to make a list of every instruction that can exit a loop.



--
Copyright 2020 Pete Olcott

"Great spirits have always encountered violent opposition from mediocre minds." Einstein


Subject: Re: It is known that a correct halt decider must return false (in this case)[V4](Step 1a)
From: olcott
Newsgroups: comp.theory, comp.ai.philosophy, comp.software-eng
Date: Thu, 26 Nov 2020 02:33 UTC
References: 1 2 3 4 5 6 7 8 9 10 11 12 13 14
Path: i2pn2.org!i2pn.org!weretis.net!feeder6.news.weretis.net!news.snarked.org!border2.nntp.dca1.giganews.com!nntp.giganews.com!buffer2.nntp.dca1.giganews.com!buffer1.nntp.dca1.giganews.com!news.giganews.com.POSTED!not-for-mail
NNTP-Posting-Date: Wed, 25 Nov 2020 20:33:40 -0600
Subject: Re: It is known that a correct halt decider must return false (in
this case)[V4](Step 1a)
Newsgroups: comp.theory,comp.ai.philosophy,comp.software-eng
References: <TqWdnXCuh8jFkibCnZ2dnUU7-QfNnZ2d@giganews.com>
<he6dnVxcwNcfviHCnZ2dnUU78IfNnZ2d@brightview.co.uk>
<ndKdnaIe-v9PtCHCnZ2dnUU7-XPNnZ2d@giganews.com>
<5eGdndmbxcGA1iHCnZ2dnUU78enNnZ2d@brightview.co.uk>
<WcCdncOumL5JyCHCnZ2dnUU7-Y3NnZ2d@giganews.com> <87im9vpg0e.fsf@bsb.me.uk>
<qoGdnW1Lz5qmByHCnZ2dnUU7-UPNnZ2d@giganews.com> <87sg8yah0c.fsf@bsb.me.uk>
<Weqdnbjny8LJqSDCnZ2dnUU7-d_NnZ2d@giganews.com> <87tute8f4h.fsf@bsb.me.uk>
<2aidnV9e3qQaOCDCnZ2dnUU7-c3NnZ2d@giganews.com> <87zh355bfu.fsf@bsb.me.uk>
<6Y6dnaUGHOdNRCPCnZ2dnUU7-fPNnZ2d@giganews.com> <87r1og6fd0.fsf@bsb.me.uk>
From: NoO...@NoWhere.com (olcott)
Date: Wed, 25 Nov 2020 20:33:41 -0600
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:78.0) Gecko/20100101
Thunderbird/78.5.0
MIME-Version: 1.0
In-Reply-To: <87r1og6fd0.fsf@bsb.me.uk>
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Language: en-US
Content-Transfer-Encoding: 7bit
Message-ID: <g4udnSi9pZyZiSLCnZ2dnUU7-VvNnZ2d@giganews.com>
Lines: 80
X-Usenet-Provider: http://www.giganews.com
X-Trace: sv3-1cD7RZ9BoDnqY4LP4dmtJljZDDhy2/US9Dh5L6YRpA30d06AkueEMfoYsqZhsGnlkNZNs1DB2BjjSuY!6NGpsCEPOZP2UdRUQsk4e3/W4eNonsKxokjbvuULiis4ZuozpYE3HLu05zEgvfxm+i8B7cef73SW!NA==
X-Complaints-To: abuse@giganews.com
X-DMCA-Notifications: http://www.giganews.com/info/dmca.html
X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers
X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint properly
X-Postfilter: 1.3.40
X-Original-Bytes: 3832
View all headers
On 11/25/2020 8:06 PM, Ben Bacarisse wrote:
olcott <NoOne@NoWhere.com> writes:

On 11/25/2020 4:16 PM, Ben Bacarisse wrote:
olcott <NoOne@NoWhere.com> writes:

On 11/24/2020 6:16 PM, Ben Bacarisse wrote:
olcott <NoOne@NoWhere.com> writes:

<cut>
08 bool Halts(u32 P, u32 I)
09 {
10   bool Halted  = false;
11   bool Aborted = false;
12   while (!Halted && !Aborted)
13   {
14     Halted  = DebugStep(P, I);
15     Aborted = Needs_To_Be_Aborted();
16   }
17   return !Aborted;
18 }

Given

     void Confound_Halts(u32 P) { if (Halts(P, P)) while (1); }

The confounding example for Halts is the computation
Confound_Halts(Confound_Halts) whose halting status is not correctly
determined by the function call Halts(Confound_Halts, Confound_Halts).

Halts(Confound_Halts, Confound_Halts) returns false.

But Confound_Halts(Confound_Halts) is a finite computation, so that's
the wrong answer (as you know perfectly well).

You start with the assumption: "Pete is wrong".

I start with the definition of what a halt decider is (in your model
using quasi-C): a function F such that F(P, I) is true iff P(I) is a
finite computation and false otherwise.


To actually understand me you have to start with the first step by understanding that in the following code DebugTrace() never returns a value to to H_Hat().

Richard has never actually gotten past this first step.


int DebugTrace(u32 P, u32 I)
{
   ((int(*)(int))P)(I);
   return 1;
}

void H_Hat(u32 P)
{
   u32 Aborted = DebugTrace(P, P);
   if (Aborted)
     HALT
   else
     HERE: goto HERE;
}

int main()
{
   u32 P = (u32)H_Hat;
   DebugTrace(P, P);
   HALT;
}





--
Copyright 2020 Pete Olcott

"Great spirits have always encountered violent opposition from mediocre minds." Einstein


Subject: Re: It is known that a correct halt decider must return false (in this case)[V4](Step 1)
From: olcott
Newsgroups: comp.theory, comp.ai.philosophy
Date: Thu, 26 Nov 2020 03:06 UTC
References: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18
Path: i2pn2.org!i2pn.org!aioe.org!peer03.ams4!peer.am4.highwinds-media.com!news.highwinds-media.com!tr2.eu1.usenetexpress.com!feeder.usenetexpress.com!tr1.iad1.usenetexpress.com!border1.nntp.dca1.giganews.com!nntp.giganews.com!buffer1.nntp.dca1.giganews.com!buffer2.nntp.dca1.giganews.com!news.giganews.com.POSTED!not-for-mail
NNTP-Posting-Date: Wed, 25 Nov 2020 21:06:15 -0600
Subject: Re: It is known that a correct halt decider must return false (in this case)[V4](Step 1)
Newsgroups: comp.theory,comp.ai.philosophy
References: <TqWdnXCuh8jFkibCnZ2dnUU7-QfNnZ2d@giganews.com> <he6dnVxcwNcfviHCnZ2dnUU78IfNnZ2d@brightview.co.uk> <ndKdnaIe-v9PtCHCnZ2dnUU7-XPNnZ2d@giganews.com> <5eGdndmbxcGA1iHCnZ2dnUU78enNnZ2d@brightview.co.uk> <WcCdncOumL5JyCHCnZ2dnUU7-Y3NnZ2d@giganews.com> <87im9vpg0e.fsf@bsb.me.uk> <qoGdnW1Lz5qmByHCnZ2dnUU7-UPNnZ2d@giganews.com> <87sg8yah0c.fsf@bsb.me.uk> <Weqdnbjny8LJqSDCnZ2dnUU7-d_NnZ2d@giganews.com> <87tute8f4h.fsf@bsb.me.uk> <2aidnV9e3qQaOCDCnZ2dnUU7-c3NnZ2d@giganews.com> <87zh355bfu.fsf@bsb.me.uk> <6Y6dnaUGHOdNRCPCnZ2dnUU7-fPNnZ2d@giganews.com> <0TBvH.159998$gR8.40967@fx45.iad> <edGdnZFDhqBRciPCnZ2dnUU7-fnNnZ2d@giganews.com> <c2DvH.160002$gR8.79102@fx45.iad> <0NmdnQTOBvJLYyPCnZ2dnUU7-YOdnZ2d@giganews.com> <TOEvH.65056$J92.17423@fx48.iad>
From: NoO...@NoWhere.com (olcott)
Date: Wed, 25 Nov 2020 21:06:21 -0600
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:78.0) Gecko/20100101 Thunderbird/78.5.0
MIME-Version: 1.0
In-Reply-To: <TOEvH.65056$J92.17423@fx48.iad>
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Language: en-US
Content-Transfer-Encoding: 7bit
Message-ID: <DdOdna35_s86hiLCnZ2dnUU7-ImdnZ2d@giganews.com>
Lines: 62
X-Usenet-Provider: http://www.giganews.com
X-Trace: sv3-evgF1m0aabUWCtzU6jMjKoNB1ZXziDLiBHk9XTuX/dWCkoy49+S0oQ677w3T+AXulQe3vo9Eh4+Q7MJ!3md8HOTDD20NNLWQwoCOvOqTV6qSg/uwleOjHFBLzeg/rEPQ6A97QjBsFTuVtLUJeh1SvlQ4bE/v!ag==
X-Complaints-To: abuse@giganews.com
X-DMCA-Notifications: http://www.giganews.com/info/dmca.html
X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers
X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint properly
X-Postfilter: 1.3.40
X-Original-Bytes: 3588
X-Received-Bytes: 3758
X-Received-Body-CRC: 1607819507
View all headers
On 11/25/2020 8:55 PM, Richard Damon wrote:
On 11/25/20 8:03 PM, olcott wrote:
On 11/25/2020 6:55 PM, Richard Damon wrote:


Since it is Halts responsibility to give an answer to any and every
quetion posed to it, it gets hard to blame the lowly input that just
came to be tested.


Clearly you have a fundamental lack of understanding of infinite recursion.

I have no problems understanding infinite recursion, what you seem to
miss is that when the halt decider is in the loop,it can be the need
break of the recursion that keeps H_Hat from being non-halting (and is
relying on the finite execution requirements on the Halt Decider).

It is the Halt Deciders problem with figuring out how to decide this
case that causing the issues.

An 'infinite recursion' that happens inside the 'must be finite' call to
the halt decider does NOT allow a higher level halts decider to call
this H_Hat non-halting.


Lets draw a simple execution nesting tree:

1) A call to Halts(P, I)

2) P(I) exeuctes, and in it

3) calls Halts(P1, I1)

4) P1(I1) executes, which maybe

5) calls Halts(P2, I2)
...

void H_Hat(u32 P)
{
   u32 Aborted = Halts(P, P);
   if (Aborted)
     HALT
   else
     HERE: goto HERE;
}

int main()
{
   u32 P = (u32)H_Hat;
   Halts(P, P);
   HALT;
}

There is only one reasonable choice here. The Halts in main() aborts H_Hat.


--
Copyright 2020 Pete Olcott

"Great spirits have always encountered violent opposition from mediocre minds." Einstein


Subject: Re: It is known that a correct halt decider must return false (in this case)[V4](Step 1a)
From: olcott
Newsgroups: comp.theory, comp.ai.philosophy
Date: Thu, 26 Nov 2020 03:08 UTC
References: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16
Path: i2pn2.org!i2pn.org!weretis.net!feeder6.news.weretis.net!news.snarked.org!border2.nntp.dca1.giganews.com!nntp.giganews.com!buffer2.nntp.dca1.giganews.com!news.giganews.com.POSTED!not-for-mail
NNTP-Posting-Date: Wed, 25 Nov 2020 21:08:18 -0600
Subject: Re: It is known that a correct halt decider must return false (in
this case)[V4](Step 1a)
Newsgroups: comp.theory,comp.ai.philosophy
References: <TqWdnXCuh8jFkibCnZ2dnUU7-QfNnZ2d@giganews.com>
<he6dnVxcwNcfviHCnZ2dnUU78IfNnZ2d@brightview.co.uk>
<ndKdnaIe-v9PtCHCnZ2dnUU7-XPNnZ2d@giganews.com>
<5eGdndmbxcGA1iHCnZ2dnUU78enNnZ2d@brightview.co.uk>
<WcCdncOumL5JyCHCnZ2dnUU7-Y3NnZ2d@giganews.com> <87im9vpg0e.fsf@bsb.me.uk>
<qoGdnW1Lz5qmByHCnZ2dnUU7-UPNnZ2d@giganews.com> <87sg8yah0c.fsf@bsb.me.uk>
<Weqdnbjny8LJqSDCnZ2dnUU7-d_NnZ2d@giganews.com> <87tute8f4h.fsf@bsb.me.uk>
<2aidnV9e3qQaOCDCnZ2dnUU7-c3NnZ2d@giganews.com> <87zh355bfu.fsf@bsb.me.uk>
<6Y6dnaUGHOdNRCPCnZ2dnUU7-fPNnZ2d@giganews.com> <87r1og6fd0.fsf@bsb.me.uk>
<g4udnSi9pZyZiSLCnZ2dnUU7-VvNnZ2d@giganews.com> <oTEvH.833$PP.527@fx07.iad>
From: NoO...@NoWhere.com (olcott)
Date: Wed, 25 Nov 2020 21:08:24 -0600
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:78.0) Gecko/20100101
Thunderbird/78.5.0
MIME-Version: 1.0
In-Reply-To: <oTEvH.833$PP.527@fx07.iad>
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Language: en-US
Content-Transfer-Encoding: 8bit
Message-ID: <DdOdnaz5_s--gSLCnZ2dnUU7-ImdnZ2d@giganews.com>
Lines: 50
X-Usenet-Provider: http://www.giganews.com
X-Trace: sv3-SGXCkKCXI+sZsgmkbNPr+BGK2t7W45xeMQeklkyrjLtyuyXYAWritIVFxBhvsj67zyouNbbUv2iUq28!IP/hjOuGCRU+CdsEQHpPPG4Qik7Fb/13Jn1kEJEjTtmKRjg+2eP0oWFNQNwI0sdjNcZuSolN0qXc!Bw==
X-Complaints-To: abuse@giganews.com
X-DMCA-Notifications: http://www.giganews.com/info/dmca.html
X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers
X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint properly
X-Postfilter: 1.3.40
X-Original-Bytes: 3037
View all headers
On 11/25/2020 9:00 PM, Richard Damon wrote:
On 11/25/20 9:33 PM, olcott wrote:

To actually understand me you have to start with the first step by
understanding that in the following code DebugTrace() never returns a
value to to H_Hat().

Richard has never actually gotten past this first step.


int DebugTrace(u32 P, u32 I)
{
   ((int(*)(int))P)(I);
   return 1;
}

void H_Hat(u32 P)
{
   u32 Aborted = DebugTrace(P, P);
   if (Aborted)
     HALT
   else
     HERE: goto HERE;
}

int main()
{
   u32 P = (u32)H_Hat;
   DebugTrace(P, P);
   HALT;
}


Does this mean that you admit that if I run as a real Turing Machine the
equivalent of

H_Hat(H_Hat) that you admit that DebugTrace does not answer in finite time?

And thus DebugTrace FAILS at being a proper Halt Decider?



No. It would maybe make me admit that you simply don't understand these things well enough.

--
Copyright 2020 Pete Olcott

"Great spirits have always encountered violent opposition from mediocre minds." Einstein


Subject: Re: It is known that a correct halt decider must return false (in this case)[V4](x86 as a formal language)
From: olcott
Newsgroups: comp.theory, comp.ai.philosophy, comp.software-eng
Date: Thu, 26 Nov 2020 04:39 UTC
References: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19
Path: i2pn2.org!i2pn.org!weretis.net!feeder6.news.weretis.net!news.snarked.org!border2.nntp.dca1.giganews.com!nntp.giganews.com!buffer2.nntp.dca1.giganews.com!news.giganews.com.POSTED!not-for-mail
NNTP-Posting-Date: Wed, 25 Nov 2020 22:39:06 -0600
Subject: Re: It is known that a correct halt decider must return false (in
this case)[V4](x86 as a formal language)
Newsgroups: comp.theory,comp.ai.philosophy,comp.software-eng
References: <TqWdnXCuh8jFkibCnZ2dnUU7-QfNnZ2d@giganews.com>
<he6dnVxcwNcfviHCnZ2dnUU78IfNnZ2d@brightview.co.uk>
<ndKdnaIe-v9PtCHCnZ2dnUU7-XPNnZ2d@giganews.com>
<5eGdndmbxcGA1iHCnZ2dnUU78enNnZ2d@brightview.co.uk>
<WcCdncOumL5JyCHCnZ2dnUU7-Y3NnZ2d@giganews.com>
<ToOdneeOqN8q6CHCnZ2dnUU78UfNnZ2d@brightview.co.uk>
<JuqdnaQGaYAtFCHCnZ2dnUU7-Q3NnZ2d@giganews.com>
<QrqdnS61EOtetCDCnZ2dnUU78TPNnZ2d@brightview.co.uk>
<qPCdnSYYdNW-FyPCnZ2dnUU78QHNnZ2d@brightview.co.uk>
<EOudnWsbKL0RDyPCnZ2dnUU7-SudnZ2d@giganews.com>
<M-GdnWrECtIvViPCnZ2dnUU78c_NnZ2d@brightview.co.uk>
<ZridnafptIUjTyPCnZ2dnUU7-UXNnZ2d@giganews.com>
<zIudnVpmqcfEdCPCnZ2dnUU78aOdnZ2d@brightview.co.uk>
<_PidnS5eJ9eLcCPCnZ2dnUU7-LfNnZ2d@giganews.com>
<Iqmdnbz55_xraiPCnZ2dnUU78V-dnZ2d@brightview.co.uk>
<zf6dnTkZ6Pi-YSPCnZ2dnUU7-TudnZ2d@giganews.com>
<OPKdncr_54uPmiLCnZ2dnUU78QednZ2d@brightview.co.uk>
<NfidnR1APKUFkiLCnZ2dnUU7-b_NnZ2d@giganews.com>
<-rSdnShOi6s1syLCnZ2dnUU78X_NnZ2d@brightview.co.uk>
From: NoO...@NoWhere.com (olcott)
Date: Wed, 25 Nov 2020 22:39:11 -0600
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:78.0) Gecko/20100101
Thunderbird/78.5.0
MIME-Version: 1.0
In-Reply-To: <-rSdnShOi6s1syLCnZ2dnUU78X_NnZ2d@brightview.co.uk>
Content-Type: text/plain; charset=windows-1252; format=flowed
Content-Language: en-US
Content-Transfer-Encoding: 8bit
Message-ID: <p7SdnUWV3YT3rCLCnZ2dnUU7-KnNnZ2d@giganews.com>
Lines: 240
X-Usenet-Provider: http://www.giganews.com
X-Trace: sv3-a0SL8c/5Ia3u9WLzWJtfoh3ChOTdaksVFRsYGNPfkjzaMe/acrOcQa/JMutM7Gkhe/7/ZjRDVc+KyeF!0WhFNqBDCIrVDNRz69DCoDvqqfRPodjCeZ3dqbazU91HEon/sY0ZX5TRoFO8Qa5I3Nz9sm1TSGJd!Ew==
X-Complaints-To: abuse@giganews.com
X-DMCA-Notifications: http://www.giganews.com/info/dmca.html
X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers
X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint properly
X-Postfilter: 1.3.40
X-Original-Bytes: 11375
View all headers
On 11/25/2020 10:27 PM, Mike Terry wrote:
On 26/11/2020 02:14, olcott wrote:
On 11/25/2020 7:38 PM, Mike Terry wrote:
On 26/11/2020 00:51, olcott wrote:
On 11/25/2020 6:33 PM, Mike Terry wrote:
On 25/11/2020 23:47, olcott wrote:
On 11/25/2020 5:31 PM, Mike Terry wrote:
On 25/11/2020 21:55, olcott wrote:
On 11/25/2020 3:25 PM, Mike Terry wrote:
On 25/11/2020 17:21, olcott wrote:
On 11/25/2020 10:45 AM, Mike Terry wrote:
On 24/11/2020 15:41, Mike Terry wrote:
On 24/11/2020 04:18, olcott wrote:
<.. snip ..>

People can eventually look at all of my code and the
thousands of
lines
of code of the x86 emulator and they can look at the
hundreds of
pages
out output. It all boils down to this:

The simulator merely watches its simulation of the following
instructions until it sees a function call to 377 from 503 the
second
time with no JCC (Jump-Condition_Code) in-between.


I have told you many times that your test must be UNSOUND.  You
have
never responded to this, so I've assumed you don't really know
whether
your test is sound or unsound (or probably, what that even
means,
although I've also explained that to you before).

Now you are getting closer to actually coding the test (which
you
claimed to have "fully coded" two years ago), you are finally
giving
more details.

So...  what do you think.  Is the following test a SOUND test
for
non-halting?

   TEST:  "monitor the simulation until there is a function
           call to 377 from 503 a second time, with no
conditional
           branch inbetween"

Putting it more directly - if some calculation P(I) triggers the
TEST
(so it contains two calls from 377 from 503, with no conditional
branch
inbetween), does this genuinely imply that the calculation will
never
halt?

Bear in mind that the two calls in question do not necessarily
occur in
the same "virtual address space", that is to say the two
calls can
[and
in the case of T_Hat(T_Hat) *do* ] occur at /different levels of
emulation/.   [Your trace notation obscures this simple fact,
making
everything appear to be in one single virtual process, when it's
not.]

What do you think?  This seems to be your primary intuition that
triggered all this "refuting" activity, BUT IS IT ACTUALLY
CORRECT?

Of course, you will say "All my intuitions are correct by
definition -
I'm never wrong" but that doesn't make it true!  :)

Is TEST *SOUND* ?


Noted: still no response to this basic question.

Mike.

<.. snip non-response to question ..>

I'm not sure if that non-response was deliberate.  I didn't ask
whether one specified implementation of [whatever] exhibits
infinite
recursion!

In case it was just a misreading, here is the question again.


   So...  what do you think.  Is the following test a SOUND test
for
   non-halting?

      TEST:  "monitor the simulation until there is a function
              call to 377 from 503 a second time, with no
conditional
              branch in-between"

It is much more generic than that.
(1) Keep a global execution trace of every line of user code.

(2) Whenever any instruction is executed see if it is a function
call.

(3) If it is a function call find the prior call to this same
function
from the current machine address (if any) searching backward
through the
global execution trace and counting conditional branch instructions.

(4) If found and conditional-branch-count == zero terminate the
input.

Copyright 2020 Pete Olcott (I just wrote that algorithm right now).

OK, I always imagined the test would be more general than just
checking specifically for calls to 377 from 503.  :)  No problem on
that front.

I'm thinking this is probably the basis of your initial intuition
that
you could actually detect and handle the type of recursion in your
fledgeling (at that time) halt decider design.

It is good that you've clarified the test, and yet it seems you're
reluctant to plainly say that you believe the test works!

logical necessity speaks for itself it doesn't need me for a
cheerleader.


LOL.  I knew you'd do something like that.

OK, so you are saying that if your test detects the behaviour
described, then it's a "logical necessity" that the input being
examined is non-halting?

Yes that is what I am saying.

There - that wasn't so bad, was it?  :)


Can you find a counter-example?

Well, if it's a logical necessity I'm in for a hard time on that one...

But here's the point:  logical necessity absolutely /does/ need a
cheerleader!  Loads of things are "logically necessary" in that they
must logically be true, and yet they are not /obviously/ true.  That's
why we have proofs.

This would be one of those scenarios, where even if your claim is
correct, it's not trivially obvious that it's correct, right?

Here is what we're saying:

TEST:
    If a calculation P(I) has a trace of steps
    (s0, s1, s2, s3, .....) and there are two steps s_i
    and s_j, such that si and sj are both unconditional
    branches from A to B, and none of the steps in-between
    s_i and s_j are conditional branches, THEN calculation
    P(I) never halts.

Well that's certainly not a "trivial restatement of word meanings" or
similar, and so is not seen to correct just on a casual glance.

So obviously where I'm going is : do you have a proof of this?

Now I know you're not one for proofs, and maybe during the course of
discussion such a proof will fall out (provided the underlying logic
is correct...)

So to start with, perhaps you can just give your thinking as to /why/
you believe it to be logically necessary?  [You clearly didn't wake up
one day and think "hey, what about TEST - oh! it's a logical
necessity, that's handy - I can use it in my halt decider!".  There
was something that led you to consider TEST, and having considered it,
you decided for whatever reason it was true...]


Mike.


Let's look at it a little simpler:
HERE:  // current location
  Instructions that cannot possibly exit a loop
THERE: goto HERE;

Can you see how this definitely loops?

I can - and if this was relevant there would be a straight forward proof that such code loops.

But this isn't like the scenario you are dealing with AT ALL!  What you are showing here is a kind of "in-process" loop detection.  What you need is some kind of recursive EMULATION detection.  (Emulation works differently in this respect.)

I'm pretty sure I explained the difference in a post a couple of weeks ago but you never responded.

We are trying to determine whether or not a specific sequence of x86 machine code bytes specify an infinite loop as if this machine code was a mathematical formalism.

The only thing that matters is: WHAT DO THE BYTES THEMSELVES SAY?



The next step is to make a list of every instruction that can exit a loop.

Yes, I see where you're going with that, but it's not going to work for the situation you need to cover...

But you are genuinely trying to answer my question, which I appreciate.

Mike.



--
Copyright 2020 Pete Olcott

"Great spirits have always encountered violent opposition from mediocre minds." Einstein


Subject: Re: It is known that a correct halt decider must return false (in this case)[V4](x86 as a formal language)
From: olcott
Newsgroups: comp.theory, comp.ai.philosophy, comp.software-eng
Date: Thu, 26 Nov 2020 16:07 UTC
References: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19
Path: i2pn2.org!i2pn.org!weretis.net!feeder6.news.weretis.net!news.snarked.org!border2.nntp.dca1.giganews.com!nntp.giganews.com!buffer2.nntp.dca1.giganews.com!news.giganews.com.POSTED!not-for-mail
NNTP-Posting-Date: Thu, 26 Nov 2020 10:07:33 -0600
Subject: Re: It is known that a correct halt decider must return false (in
this case)[V4](x86 as a formal language)
Newsgroups: comp.theory,comp.ai.philosophy,comp.software-eng
References: <TqWdnXCuh8jFkibCnZ2dnUU7-QfNnZ2d@giganews.com>
<5eGdndmbxcGA1iHCnZ2dnUU78enNnZ2d@brightview.co.uk>
<WcCdncOumL5JyCHCnZ2dnUU7-Y3NnZ2d@giganews.com>
<ToOdneeOqN8q6CHCnZ2dnUU78UfNnZ2d@brightview.co.uk>
<JuqdnaQGaYAtFCHCnZ2dnUU7-Q3NnZ2d@giganews.com>
<QrqdnS61EOtetCDCnZ2dnUU78TPNnZ2d@brightview.co.uk>
<qPCdnSYYdNW-FyPCnZ2dnUU78QHNnZ2d@brightview.co.uk>
<EOudnWsbKL0RDyPCnZ2dnUU7-SudnZ2d@giganews.com>
<M-GdnWrECtIvViPCnZ2dnUU78c_NnZ2d@brightview.co.uk>
<ZridnafptIUjTyPCnZ2dnUU7-UXNnZ2d@giganews.com>
<zIudnVpmqcfEdCPCnZ2dnUU78aOdnZ2d@brightview.co.uk>
<_PidnS5eJ9eLcCPCnZ2dnUU7-LfNnZ2d@giganews.com>
<Iqmdnbz55_xraiPCnZ2dnUU78V-dnZ2d@brightview.co.uk>
<zf6dnTkZ6Pi-YSPCnZ2dnUU7-TudnZ2d@giganews.com>
<OPKdncr_54uPmiLCnZ2dnUU78QednZ2d@brightview.co.uk>
<NfidnR1APKUFkiLCnZ2dnUU7-b_NnZ2d@giganews.com>
<-rSdnShOi6s1syLCnZ2dnUU78X_NnZ2d@brightview.co.uk>
<p7SdnUWV3YT3rCLCnZ2dnUU7-KnNnZ2d@giganews.com>
<G9ednQR63dvHUyLCnZ2dnUU78QnNnZ2d@brightview.co.uk>
From: NoO...@NoWhere.com (olcott)
Date: Thu, 26 Nov 2020 10:07:39 -0600
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:78.0) Gecko/20100101
Thunderbird/78.5.0
MIME-Version: 1.0
In-Reply-To: <G9ednQR63dvHUyLCnZ2dnUU78QnNnZ2d@brightview.co.uk>
Content-Type: text/plain; charset=windows-1252; format=flowed
Content-Language: en-US
Content-Transfer-Encoding: 8bit
Message-ID: <PfmdnUdnnqhYTyLCnZ2dnUU7-c3NnZ2d@giganews.com>
Lines: 274
X-Usenet-Provider: http://www.giganews.com
X-Trace: sv3-t3Z7UWeM0ArYW6ml8UQd7DE6P4r8C6hsOmBCBTML5XrewgOrRzzr4JZkQEYTWs3vvelTGSPErDwT2AW!+hJQd8qgdO44UqxAeHK/v3IKMK379f73NhYnvNsLWIqx3khI4txuHyGy2eSUm/HjDeR7dUnuP59c!tg==
X-Complaints-To: abuse@giganews.com
X-DMCA-Notifications: http://www.giganews.com/info/dmca.html
X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers
X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint properly
X-Postfilter: 1.3.40
X-Original-Bytes: 13109
View all headers
On 11/26/2020 9:48 AM, Mike Terry wrote:
On 26/11/2020 04:39, olcott wrote:
On 11/25/2020 10:27 PM, Mike Terry wrote:
On 26/11/2020 02:14, olcott wrote:
On 11/25/2020 7:38 PM, Mike Terry wrote:
On 26/11/2020 00:51, olcott wrote:
On 11/25/2020 6:33 PM, Mike Terry wrote:
On 25/11/2020 23:47, olcott wrote:
On 11/25/2020 5:31 PM, Mike Terry wrote:
On 25/11/2020 21:55, olcott wrote:
On 11/25/2020 3:25 PM, Mike Terry wrote:
On 25/11/2020 17:21, olcott wrote:
On 11/25/2020 10:45 AM, Mike Terry wrote:
On 24/11/2020 15:41, Mike Terry wrote:
On 24/11/2020 04:18, olcott wrote:
<.. snip ..>

People can eventually look at all of my code and the
thousands of
lines
of code of the x86 emulator and they can look at the
hundreds of
pages
out output. It all boils down to this:

The simulator merely watches its simulation of the following
instructions until it sees a function call to 377 from 503
the
second
time with no JCC (Jump-Condition_Code) in-between.


I have told you many times that your test must be UNSOUND.
You
have
never responded to this, so I've assumed you don't really know
whether
your test is sound or unsound (or probably, what that even
means,
although I've also explained that to you before).

Now you are getting closer to actually coding the test (which
you
claimed to have "fully coded" two years ago), you are finally
giving
more details.

So...  what do you think.  Is the following test a SOUND test
for
non-halting?

   TEST:  "monitor the simulation until there is a function
           call to 377 from 503 a second time, with no
conditional
           branch inbetween"

Putting it more directly - if some calculation P(I)
triggers the
TEST
(so it contains two calls from 377 from 503, with no
conditional
branch
inbetween), does this genuinely imply that the calculation
will
never
halt?

Bear in mind that the two calls in question do not necessarily
occur in
the same "virtual address space", that is to say the two
calls can
[and
in the case of T_Hat(T_Hat) *do* ] occur at /different
levels of
emulation/.   [Your trace notation obscures this simple fact,
making
everything appear to be in one single virtual process, when
it's
not.]

What do you think?  This seems to be your primary intuition
that
triggered all this "refuting" activity, BUT IS IT ACTUALLY
CORRECT?

Of course, you will say "All my intuitions are correct by
definition -
I'm never wrong" but that doesn't make it true!  :)

Is TEST *SOUND* ?


Noted: still no response to this basic question.

Mike.

<.. snip non-response to question ..>

I'm not sure if that non-response was deliberate.  I didn't ask
whether one specified implementation of [whatever] exhibits
infinite
recursion!

In case it was just a misreading, here is the question again.


   So...  what do you think.  Is the following test a SOUND test
for
   non-halting?

      TEST:  "monitor the simulation until there is a function
              call to 377 from 503 a second time, with no
conditional
              branch in-between"

It is much more generic than that.
(1) Keep a global execution trace of every line of user code.

(2) Whenever any instruction is executed see if it is a function
call.

(3) If it is a function call find the prior call to this same
function
from the current machine address (if any) searching backward
through the
global execution trace and counting conditional branch
instructions.

(4) If found and conditional-branch-count == zero terminate the
input.

Copyright 2020 Pete Olcott (I just wrote that algorithm right
now).

OK, I always imagined the test would be more general than just
checking specifically for calls to 377 from 503.  :)  No problem on
that front.

I'm thinking this is probably the basis of your initial intuition
that
you could actually detect and handle the type of recursion in your
fledgeling (at that time) halt decider design.

It is good that you've clarified the test, and yet it seems you're
reluctant to plainly say that you believe the test works!

logical necessity speaks for itself it doesn't need me for a
cheerleader.


LOL.  I knew you'd do something like that.

OK, so you are saying that if your test detects the behaviour
described, then it's a "logical necessity" that the input being
examined is non-halting?

Yes that is what I am saying.

There - that wasn't so bad, was it?  :)


Can you find a counter-example?

Well, if it's a logical necessity I'm in for a hard time on that one...

But here's the point:  logical necessity absolutely /does/ need a
cheerleader!  Loads of things are "logically necessary" in that they
must logically be true, and yet they are not /obviously/ true.  That's
why we have proofs.

This would be one of those scenarios, where even if your claim is
correct, it's not trivially obvious that it's correct, right?

Here is what we're saying:

TEST:
    If a calculation P(I) has a trace of steps
    (s0, s1, s2, s3, .....) and there are two steps s_i
    and s_j, such that si and sj are both unconditional
    branches from A to B, and none of the steps in-between
    s_i and s_j are conditional branches, THEN calculation
    P(I) never halts.

Well that's certainly not a "trivial restatement of word meanings" or
similar, and so is not seen to correct just on a casual glance.

So obviously where I'm going is : do you have a proof of this?

Now I know you're not one for proofs, and maybe during the course of
discussion such a proof will fall out (provided the underlying logic
is correct...)

So to start with, perhaps you can just give your thinking as to /why/
you believe it to be logically necessary?  [You clearly didn't wake up
one day and think "hey, what about TEST - oh! it's a logical
necessity, that's handy - I can use it in my halt decider!".  There
was something that led you to consider TEST, and having considered it,
you decided for whatever reason it was true...]


Mike.


Let's look at it a little simpler:
HERE:  // current location
  Instructions that cannot possibly exit a loop
THERE: goto HERE;

Can you see how this definitely loops?

I can - and if this was relevant there would be a straight forward
proof that such code loops.

But this isn't like the scenario you are dealing with AT ALL!  What
you are showing here is a kind of "in-process" loop detection.  What
you need is some kind of recursive EMULATION detection.  (Emulation
works differently in this respect.)

I'm pretty sure I explained the difference in a post a couple of weeks
ago but you never responded.

We are trying to determine whether or not a specific sequence of x86
machine code bytes specify an infinite loop as if this machine code was
a mathematical formalism.

The only thing that matters is: WHAT DO THE BYTES THEMSELVES SAY?


Well, I understand that the code bytes that you presented, if executed by a processor within one single logical thread of execution, would never terminate - there is an obvious loop.

But that's ignoring the issue of RECURSION, where behaviour is not so simple.  So what's the next step?  (So far what you've said is no justification for the RECUSION scenario, which is what you TEST is concerned with.)

Mike.


The sequences of instructions from HERE to THERE and HERE to HERE are from actual execution traces. The x86 emulator screens out all dead code and only shows us the code that is actually reached.

-HERE:  // current location
-   Instructions that cannot possibly exit a loop
-THERE: goto HERE;

To form a mathematical proof on the basis of the x86 language being construed as a formal language we only have to derive the complete list of every instruction that can possibly exit the above loop and if there are none of these between the labels HERE and THERE then we know that the loop is infinite.

The case for infinite recursion is similar.

-HERE: Call Function At Address X
-   Instructions that cannot possibly exit recursion
-HERE: Call Function At Address X

If there are no instructions that can possibly exit recursion between invocations of the same function from the same machine address, then recursion is infinite.


--
Copyright 2020 Pete Olcott

"Great spirits have always encountered violent opposition from mediocre minds." Einstein


Subject: Re: It is known that a correct halt decider must return false (in this case)[V4](x86 as a formal language)
From: olcott
Newsgroups: comp.theory, comp.ai.philosophy, comp.software-eng
Date: Thu, 26 Nov 2020 16:41 UTC
References: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19
Path: i2pn2.org!i2pn.org!aioe.org!peer01.ams4!peer.am4.highwinds-media.com!peer02.iad!feed-me.highwinds-media.com!news.highwinds-media.com!border1.nntp.dca1.giganews.com!nntp.giganews.com!buffer1.nntp.dca1.giganews.com!news.giganews.com.POSTED!not-for-mail
NNTP-Posting-Date: Thu, 26 Nov 2020 10:41:11 -0600
Subject: Re: It is known that a correct halt decider must return false (in
this case)[V4](x86 as a formal language)
Newsgroups: comp.theory,comp.ai.philosophy,comp.software-eng
References: <TqWdnXCuh8jFkibCnZ2dnUU7-QfNnZ2d@giganews.com>
<ToOdneeOqN8q6CHCnZ2dnUU78UfNnZ2d@brightview.co.uk>
<JuqdnaQGaYAtFCHCnZ2dnUU7-Q3NnZ2d@giganews.com>
<QrqdnS61EOtetCDCnZ2dnUU78TPNnZ2d@brightview.co.uk>
<qPCdnSYYdNW-FyPCnZ2dnUU78QHNnZ2d@brightview.co.uk>
<EOudnWsbKL0RDyPCnZ2dnUU7-SudnZ2d@giganews.com>
<M-GdnWrECtIvViPCnZ2dnUU78c_NnZ2d@brightview.co.uk>
<ZridnafptIUjTyPCnZ2dnUU7-UXNnZ2d@giganews.com>
<zIudnVpmqcfEdCPCnZ2dnUU78aOdnZ2d@brightview.co.uk>
<_PidnS5eJ9eLcCPCnZ2dnUU7-LfNnZ2d@giganews.com>
<Iqmdnbz55_xraiPCnZ2dnUU78V-dnZ2d@brightview.co.uk>
<zf6dnTkZ6Pi-YSPCnZ2dnUU7-TudnZ2d@giganews.com>
<OPKdncr_54uPmiLCnZ2dnUU78QednZ2d@brightview.co.uk>
<NfidnR1APKUFkiLCnZ2dnUU7-b_NnZ2d@giganews.com>
<-rSdnShOi6s1syLCnZ2dnUU78X_NnZ2d@brightview.co.uk>
<p7SdnUWV3YT3rCLCnZ2dnUU7-KnNnZ2d@giganews.com>
<G9ednQR63dvHUyLCnZ2dnUU78QnNnZ2d@brightview.co.uk>
<PfmdnUdnnqhYTyLCnZ2dnUU7-c3NnZ2d@giganews.com>
<U8ednVm41KijRSLCnZ2dnUU78c_NnZ2d@brightview.co.uk>
From: NoO...@NoWhere.com (olcott)
Date: Thu, 26 Nov 2020 10:41:17 -0600
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:78.0) Gecko/20100101
Thunderbird/78.5.0
MIME-Version: 1.0
In-Reply-To: <U8ednVm41KijRSLCnZ2dnUU78c_NnZ2d@brightview.co.uk>
Content-Type: text/plain; charset=windows-1252; format=flowed
Content-Language: en-US
Content-Transfer-Encoding: 8bit
Message-ID: <746dnWToYoc6RyLCnZ2dnUU7-N_NnZ2d@giganews.com>
Lines: 316
X-Usenet-Provider: http://www.giganews.com
X-Trace: sv3-zS1pwVCiNe9qh3OgAe0Q/ONdS/r4kJB5rBCUE8xlZAZdD7FEsjQF45e55UGV9H5ssriMz7I7AjUi8k7!0cPLmG7ih/0yc23hIoPFbmNJbykngdXxdI+wfePE7WIzsXwMsPudkoMDRf3stp6yD1bIYAbimHBm!CQ==
X-Complaints-To: abuse@giganews.com
X-DMCA-Notifications: http://www.giganews.com/info/dmca.html
X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers
X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint properly
X-Postfilter: 1.3.40
X-Original-Bytes: 14857
X-Received-Bytes: 15072
X-Received-Body-CRC: 1130320984
View all headers
On 11/26/2020 10:30 AM, Mike Terry wrote:
On 26/11/2020 16:07, olcott wrote:
On 11/26/2020 9:48 AM, Mike Terry wrote:
On 26/11/2020 04:39, olcott wrote:
On 11/25/2020 10:27 PM, Mike Terry wrote:
On 26/11/2020 02:14, olcott wrote:
On 11/25/2020 7:38 PM, Mike Terry wrote:
On 26/11/2020 00:51, olcott wrote:
On 11/25/2020 6:33 PM, Mike Terry wrote:
On 25/11/2020 23:47, olcott wrote:
On 11/25/2020 5:31 PM, Mike Terry wrote:
On 25/11/2020 21:55, olcott wrote:
On 11/25/2020 3:25 PM, Mike Terry wrote:
On 25/11/2020 17:21, olcott wrote:
On 11/25/2020 10:45 AM, Mike Terry wrote:
On 24/11/2020 15:41, Mike Terry wrote:
On 24/11/2020 04:18, olcott wrote:
<.. snip ..>

People can eventually look at all of my code and the
thousands of
lines
of code of the x86 emulator and they can look at the
hundreds of
pages
out output. It all boils down to this:

The simulator merely watches its simulation of the
following
instructions until it sees a function call to 377 from 503
the
second
time with no JCC (Jump-Condition_Code) in-between.


I have told you many times that your test must be UNSOUND.
You
have
never responded to this, so I've assumed you don't really
know
whether
your test is sound or unsound (or probably, what that even
means,
although I've also explained that to you before).

Now you are getting closer to actually coding the test
(which
you
claimed to have "fully coded" two years ago), you are
finally
giving
more details.

So...  what do you think.  Is the following test a SOUND
test
for
non-halting?

   TEST:  "monitor the simulation until there is a function
           call to 377 from 503 a second time, with no
conditional
           branch inbetween"

Putting it more directly - if some calculation P(I)
triggers the
TEST
(so it contains two calls from 377 from 503, with no
conditional
branch
inbetween), does this genuinely imply that the calculation
will
never
halt?

Bear in mind that the two calls in question do not
necessarily
occur in
the same "virtual address space", that is to say the two
calls can
[and
in the case of T_Hat(T_Hat) *do* ] occur at /different
levels of
emulation/.   [Your trace notation obscures this simple
fact,
making
everything appear to be in one single virtual process, when
it's
not.]

What do you think?  This seems to be your primary intuition
that
triggered all this "refuting" activity, BUT IS IT ACTUALLY
CORRECT?

Of course, you will say "All my intuitions are correct by
definition -
I'm never wrong" but that doesn't make it true!  :)

Is TEST *SOUND* ?


Noted: still no response to this basic question.

Mike.

<.. snip non-response to question ..>

I'm not sure if that non-response was deliberate.  I didn't ask
whether one specified implementation of [whatever] exhibits
infinite
recursion!

In case it was just a misreading, here is the question again.


   So...  what do you think.  Is the following test a SOUND
test
for
   non-halting?

      TEST:  "monitor the simulation until there is a function
              call to 377 from 503 a second time, with no
conditional
              branch in-between"

It is much more generic than that.
(1) Keep a global execution trace of every line of user code.

(2) Whenever any instruction is executed see if it is a function
call.

(3) If it is a function call find the prior call to this same
function
from the current machine address (if any) searching backward
through the
global execution trace and counting conditional branch
instructions.

(4) If found and conditional-branch-count == zero terminate the
input.

Copyright 2020 Pete Olcott (I just wrote that algorithm right
now).

OK, I always imagined the test would be more general than just
checking specifically for calls to 377 from 503.  :)  No
problem on
that front.

I'm thinking this is probably the basis of your initial intuition
that
you could actually detect and handle the type of recursion in
your
fledgeling (at that time) halt decider design.

It is good that you've clarified the test, and yet it seems
you're
reluctant to plainly say that you believe the test works!

logical necessity speaks for itself it doesn't need me for a
cheerleader.


LOL.  I knew you'd do something like that.

OK, so you are saying that if your test detects the behaviour
described, then it's a "logical necessity" that the input being
examined is non-halting?

Yes that is what I am saying.

There - that wasn't so bad, was it?  :)


Can you find a counter-example?

Well, if it's a logical necessity I'm in for a hard time on that
one...

But here's the point:  logical necessity absolutely /does/ need a
cheerleader!  Loads of things are "logically necessary" in that they
must logically be true, and yet they are not /obviously/ true.
That's
why we have proofs.

This would be one of those scenarios, where even if your claim is
correct, it's not trivially obvious that it's correct, right?

Here is what we're saying:

TEST:
    If a calculation P(I) has a trace of steps
    (s0, s1, s2, s3, .....) and there are two steps s_i
    and s_j, such that si and sj are both unconditional
    branches from A to B, and none of the steps in-between
    s_i and s_j are conditional branches, THEN calculation
    P(I) never halts.

Well that's certainly not a "trivial restatement of word meanings" or
similar, and so is not seen to correct just on a casual glance.

So obviously where I'm going is : do you have a proof of this?

Now I know you're not one for proofs, and maybe during the course of
discussion such a proof will fall out (provided the underlying logic
is correct...)

So to start with, perhaps you can just give your thinking as to /why/
you believe it to be logically necessary?  [You clearly didn't
wake up
one day and think "hey, what about TEST - oh! it's a logical
necessity, that's handy - I can use it in my halt decider!".  There
was something that led you to consider TEST, and having considered
it,
you decided for whatever reason it was true...]


Mike.


Let's look at it a little simpler:
HERE:  // current location
  Instructions that cannot possibly exit a loop
THERE: goto HERE;

Can you see how this definitely loops?

I can - and if this was relevant there would be a straight forward
proof that such code loops.

But this isn't like the scenario you are dealing with AT ALL!  What
you are showing here is a kind of "in-process" loop detection.  What
you need is some kind of recursive EMULATION detection.  (Emulation
works differently in this respect.)

I'm pretty sure I explained the difference in a post a couple of weeks
ago but you never responded.

We are trying to determine whether or not a specific sequence of x86
machine code bytes specify an infinite loop as if this machine code was
a mathematical formalism.

The only thing that matters is: WHAT DO THE BYTES THEMSELVES SAY?


Well, I understand that the code bytes that you presented, if executed
by a processor within one single logical thread of execution, would
never terminate - there is an obvious loop.

But that's ignoring the issue of RECURSION, where behaviour is not so
simple.  So what's the next step?  (So far what you've said is no
justification for the RECUSION scenario, which is what you TEST is
concerned with.)

Mike.


The sequences of instructions from HERE to THERE and HERE to HERE are
from actual execution traces. The x86 emulator screens out all dead code
and only shows us the code that is actually reached.

-HERE:  // current location
-   Instructions that cannot possibly exit a loop
-THERE: goto HERE;

To form a mathematical proof on the basis of the x86 language being
construed as a formal language we only have to derive the complete list
of every instruction that can possibly exit the above loop and if there
are none of these between the labels HERE and THERE then we know that
the loop is infinite.

Like I said, that is ok for a "contiguous thread of execution", i.e. if an x86 processor starts at HERE, and then steps its execution, executing the instructions, then the processor will go round and round the loop. The proof is easy.


The case for infinite recursion is similar.

No it's not.  The easy proof for the contiguous thread of execution does not work in the case where there is recursion.  Or, put more accurately, it works WITHIN A SINGLE CONTIGUOUS THREAD OF EXECUTION (the obvious proof still works for this), but *NOT WHEN THE TRACE ENTRIES CROSS RECURSION LEVELS*.


-HERE: Call Function At Address X
-   Instructions that cannot possibly exit recursion
-HERE: Call Function At Address X

If there are no instructions that can possibly exit recursion between
invocations of the same function from the same machine address, then
recursion is infinite.

That doesn't work with recursive emulation, BECAUSE THE EMULATION CAN BE BROKEN FROM OUTSIDE THE SET OF INSTRUCTIONS YOU ARE CONSIDERING.


Mike.


That doesn't count. We are only examining the execution that is specified by the actual x86 language bytes as a formal language of a formal system.

Click here to read the complete article
Subject: Re: It is known that a correct halt decider must return false (in this case)[V4](x86 as a formal language)
From: olcott
Newsgroups: comp.theory, comp.ai.philosophy, comp.software-eng
Date: Thu, 26 Nov 2020 17:34 UTC
References: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19
Path: i2pn2.org!i2pn.org!weretis.net!feeder6.news.weretis.net!news.snarked.org!border2.nntp.dca1.giganews.com!nntp.giganews.com!buffer2.nntp.dca1.giganews.com!buffer1.nntp.dca1.giganews.com!news.giganews.com.POSTED!not-for-mail
NNTP-Posting-Date: Thu, 26 Nov 2020 11:34:37 -0600
Subject: Re: It is known that a correct halt decider must return false (in
this case)[V4](x86 as a formal language)
Newsgroups: comp.theory,comp.ai.philosophy,comp.software-eng
References: <TqWdnXCuh8jFkibCnZ2dnUU7-QfNnZ2d@giganews.com>
<QrqdnS61EOtetCDCnZ2dnUU78TPNnZ2d@brightview.co.uk>
<qPCdnSYYdNW-FyPCnZ2dnUU78QHNnZ2d@brightview.co.uk>
<EOudnWsbKL0RDyPCnZ2dnUU7-SudnZ2d@giganews.com>
<M-GdnWrECtIvViPCnZ2dnUU78c_NnZ2d@brightview.co.uk>
<ZridnafptIUjTyPCnZ2dnUU7-UXNnZ2d@giganews.com>
<zIudnVpmqcfEdCPCnZ2dnUU78aOdnZ2d@brightview.co.uk>
<_PidnS5eJ9eLcCPCnZ2dnUU7-LfNnZ2d@giganews.com>
<Iqmdnbz55_xraiPCnZ2dnUU78V-dnZ2d@brightview.co.uk>
<zf6dnTkZ6Pi-YSPCnZ2dnUU7-TudnZ2d@giganews.com>
<OPKdncr_54uPmiLCnZ2dnUU78QednZ2d@brightview.co.uk>
<NfidnR1APKUFkiLCnZ2dnUU7-b_NnZ2d@giganews.com>
<-rSdnShOi6s1syLCnZ2dnUU78X_NnZ2d@brightview.co.uk>
<p7SdnUWV3YT3rCLCnZ2dnUU7-KnNnZ2d@giganews.com>
<G9ednQR63dvHUyLCnZ2dnUU78QnNnZ2d@brightview.co.uk>
<PfmdnUdnnqhYTyLCnZ2dnUU7-c3NnZ2d@giganews.com>
<U8ednVm41KijRSLCnZ2dnUU78c_NnZ2d@brightview.co.uk>
<746dnWToYoc6RyLCnZ2dnUU7-N_NnZ2d@giganews.com>
<_eCdnSZdT4qMfCLCnZ2dnUU78I_NnZ2d@brightview.co.uk>
From: NoO...@NoWhere.com (olcott)
Date: Thu, 26 Nov 2020 11:34:43 -0600
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:78.0) Gecko/20100101
Thunderbird/78.5.0
MIME-Version: 1.0
In-Reply-To: <_eCdnSZdT4qMfCLCnZ2dnUU78I_NnZ2d@brightview.co.uk>
Content-Type: text/plain; charset=windows-1252; format=flowed
Content-Language: en-US
Content-Transfer-Encoding: 8bit
Message-ID: <Q9ydnbikEfeweiLCnZ2dnUU7-R_NnZ2d@giganews.com>
Lines: 359
X-Usenet-Provider: http://www.giganews.com
X-Trace: sv3-TvZnvzwaYbWbrKMn0SzS0cI+46poZt1hs2rSh85Fm/9SsxvRI4fOvfrq6Rw2x2LHU/cytkZrA2WZS56!mNHhInY4VOvOpPCU3ugwPKV3rSI4ON2uE2EIf05N5jpSWGi5V2NDL3zIzSnhlyXWBx+sRv8NIQ44!SQ==
X-Complaints-To: abuse@giganews.com
X-DMCA-Notifications: http://www.giganews.com/info/dmca.html
X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers
X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint properly
X-Postfilter: 1.3.40
X-Original-Bytes: 16488
View all headers
On 11/26/2020 11:08 AM, Mike Terry wrote:
On 26/11/2020 16:41, olcott wrote:
On 11/26/2020 10:30 AM, Mike Terry wrote:
On 26/11/2020 16:07, olcott wrote:
On 11/26/2020 9:48 AM, Mike Terry wrote:
On 26/11/2020 04:39, olcott wrote:
On 11/25/2020 10:27 PM, Mike Terry wrote:
On 26/11/2020 02:14, olcott wrote:
On 11/25/2020 7:38 PM, Mike Terry wrote:
On 26/11/2020 00:51, olcott wrote:
On 11/25/2020 6:33 PM, Mike Terry wrote:
On 25/11/2020 23:47, olcott wrote:
On 11/25/2020 5:31 PM, Mike Terry wrote:
On 25/11/2020 21:55, olcott wrote:
On 11/25/2020 3:25 PM, Mike Terry wrote:
On 25/11/2020 17:21, olcott wrote:
On 11/25/2020 10:45 AM, Mike Terry wrote:
On 24/11/2020 15:41, Mike Terry wrote:
On 24/11/2020 04:18, olcott wrote:
<.. snip ..>

People can eventually look at all of my code and the
thousands of
lines
of code of the x86 emulator and they can look at the
hundreds of
pages
out output. It all boils down to this:

The simulator merely watches its simulation of the
following
instructions until it sees a function call to 377 from
503
the
second
time with no JCC (Jump-Condition_Code) in-between.


I have told you many times that your test must be UNSOUND.
You
have
never responded to this, so I've assumed you don't really
know
whether
your test is sound or unsound (or probably, what that even
means,
although I've also explained that to you before).

Now you are getting closer to actually coding the test
(which
you
claimed to have "fully coded" two years ago), you are
finally
giving
more details.

So...  what do you think.  Is the following test a SOUND
test
for
non-halting?

   TEST:  "monitor the simulation until there is a
function
           call to 377 from 503 a second time, with no
conditional
           branch inbetween"

Putting it more directly - if some calculation P(I)
triggers the
TEST
(so it contains two calls from 377 from 503, with no
conditional
branch
inbetween), does this genuinely imply that the calculation
will
never
halt?

Bear in mind that the two calls in question do not
necessarily
occur in
the same "virtual address space", that is to say the two
calls can
[and
in the case of T_Hat(T_Hat) *do* ] occur at /different
levels of
emulation/.   [Your trace notation obscures this simple
fact,
making
everything appear to be in one single virtual process,
when
it's
not.]

What do you think?  This seems to be your primary
intuition
that
triggered all this "refuting" activity, BUT IS IT ACTUALLY
CORRECT?

Of course, you will say "All my intuitions are correct by
definition -
I'm never wrong" but that doesn't make it true!  :)

Is TEST *SOUND* ?


Noted: still no response to this basic question.

Mike.

<.. snip non-response to question ..>

I'm not sure if that non-response was deliberate.  I
didn't ask
whether one specified implementation of [whatever] exhibits
infinite
recursion!

In case it was just a misreading, here is the question again.


   So...  what do you think.  Is the following test a SOUND
test
for
   non-halting?

      TEST:  "monitor the simulation until there is a
function
              call to 377 from 503 a second time, with no
conditional
              branch in-between"

It is much more generic than that.
(1) Keep a global execution trace of every line of user code.

(2) Whenever any instruction is executed see if it is a
function
call.

(3) If it is a function call find the prior call to this same
function
from the current machine address (if any) searching backward
through the
global execution trace and counting conditional branch
instructions.

(4) If found and conditional-branch-count == zero terminate
the
input.

Copyright 2020 Pete Olcott (I just wrote that algorithm right
now).

OK, I always imagined the test would be more general than just
checking specifically for calls to 377 from 503.  :)  No
problem on
that front.

I'm thinking this is probably the basis of your initial
intuition
that
you could actually detect and handle the type of recursion in
your
fledgeling (at that time) halt decider design.

It is good that you've clarified the test, and yet it seems
you're
reluctant to plainly say that you believe the test works!

logical necessity speaks for itself it doesn't need me for a
cheerleader.


LOL.  I knew you'd do something like that.

OK, so you are saying that if your test detects the behaviour
described, then it's a "logical necessity" that the input being
examined is non-halting?

Yes that is what I am saying.

There - that wasn't so bad, was it?  :)


Can you find a counter-example?

Well, if it's a logical necessity I'm in for a hard time on that
one...

But here's the point:  logical necessity absolutely /does/ need a
cheerleader!  Loads of things are "logically necessary" in that
they
must logically be true, and yet they are not /obviously/ true.
That's
why we have proofs.

This would be one of those scenarios, where even if your claim is
correct, it's not trivially obvious that it's correct, right?

Here is what we're saying:

TEST:
    If a calculation P(I) has a trace of steps
    (s0, s1, s2, s3, .....) and there are two steps s_i
    and s_j, such that si and sj are both unconditional
    branches from A to B, and none of the steps in-between
    s_i and s_j are conditional branches, THEN calculation
    P(I) never halts.

Well that's certainly not a "trivial restatement of word
meanings" or
similar, and so is not seen to correct just on a casual glance.

So obviously where I'm going is : do you have a proof of this?

Now I know you're not one for proofs, and maybe during the
course of
discussion such a proof will fall out (provided the underlying
logic
is correct...)

So to start with, perhaps you can just give your thinking as to
/why/
you believe it to be logically necessary?  [You clearly didn't
wake up
one day and think "hey, what about TEST - oh! it's a logical
necessity, that's handy - I can use it in my halt decider!".  There
was something that led you to consider TEST, and having considered
it,
you decided for whatever reason it was true...]


Mike.


Let's look at it a little simpler:
HERE:  // current location
  Instructions that cannot possibly exit a loop
THERE: goto HERE;

Can you see how this definitely loops?

I can - and if this was relevant there would be a straight forward
proof that such code loops.

But this isn't like the scenario you are dealing with AT ALL!  What
you are showing here is a kind of "in-process" loop detection.  What
you need is some kind of recursive EMULATION detection.  (Emulation
works differently in this respect.)

I'm pretty sure I explained the difference in a post a couple of
weeks
ago but you never responded.

We are trying to determine whether or not a specific sequence of x86
machine code bytes specify an infinite loop as if this machine code
was
a mathematical formalism.

The only thing that matters is: WHAT DO THE BYTES THEMSELVES SAY?


Well, I understand that the code bytes that you presented, if executed
by a processor within one single logical thread of execution, would
never terminate - there is an obvious loop.

But that's ignoring the issue of RECURSION, where behaviour is not so
simple.  So what's the next step?  (So far what you've said is no
justification for the RECUSION scenario, which is what you TEST is
concerned with.)

Mike.


The sequences of instructions from HERE to THERE and HERE to HERE are
from actual execution traces. The x86 emulator screens out all dead code
and only shows us the code that is actually reached.

-HERE:  // current location
-   Instructions that cannot possibly exit a loop
-THERE: goto HERE;

To form a mathematical proof on the basis of the x86 language being
construed as a formal language we only have to derive the complete list
of every instruction that can possibly exit the above loop and if there
are none of these between the labels HERE and THERE then we know that
the loop is infinite.

Like I said, that is ok for a "contiguous thread of execution", i.e.
if an x86 processor starts at HERE, and then steps its execution,
executing the instructions, then the processor will go round and round
the loop. The proof is easy.


The case for infinite recursion is similar.

No it's not.  The easy proof for the contiguous thread of execution
does not work in the case where there is recursion.  Or, put more
accurately, it works WITHIN A SINGLE CONTIGUOUS THREAD OF EXECUTION
(the obvious proof still works for this), but *NOT WHEN THE TRACE
ENTRIES CROSS RECURSION LEVELS*.


-HERE: Call Function At Address X
-   Instructions that cannot possibly exit recursion
-HERE: Call Function At Address X

If there are no instructions that can possibly exit recursion between
invocations of the same function from the same machine address, then
recursion is infinite.

That doesn't work with recursive emulation, BECAUSE THE EMULATION CAN

Click here to read the complete article
Subject: Re: It is known that a correct halt decider must return false (in this case)[V4](x86 as a formal language)
From: olcott
Newsgroups: comp.theory, comp.ai.philosophy, comp.software-eng
Date: Thu, 26 Nov 2020 19:58 UTC
References: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19
Path: i2pn2.org!i2pn.org!aioe.org!peer03.ams4!peer.am4.highwinds-media.com!peer01.iad!feed-me.highwinds-media.com!news.highwinds-media.com!border1.nntp.dca1.giganews.com!nntp.giganews.com!buffer1.nntp.dca1.giganews.com!buffer2.nntp.dca1.giganews.com!news.giganews.com.POSTED!not-for-mail
NNTP-Posting-Date: Thu, 26 Nov 2020 13:58:22 -0600
Subject: Re: It is known that a correct halt decider must return false (in
this case)[V4](x86 as a formal language)
Newsgroups: comp.theory,comp.ai.philosophy,comp.software-eng
References: <TqWdnXCuh8jFkibCnZ2dnUU7-QfNnZ2d@giganews.com>
<EOudnWsbKL0RDyPCnZ2dnUU7-SudnZ2d@giganews.com>
<M-GdnWrECtIvViPCnZ2dnUU78c_NnZ2d@brightview.co.uk>
<ZridnafptIUjTyPCnZ2dnUU7-UXNnZ2d@giganews.com>
<zIudnVpmqcfEdCPCnZ2dnUU78aOdnZ2d@brightview.co.uk>
<_PidnS5eJ9eLcCPCnZ2dnUU7-LfNnZ2d@giganews.com>
<Iqmdnbz55_xraiPCnZ2dnUU78V-dnZ2d@brightview.co.uk>
<zf6dnTkZ6Pi-YSPCnZ2dnUU7-TudnZ2d@giganews.com>
<OPKdncr_54uPmiLCnZ2dnUU78QednZ2d@brightview.co.uk>
<NfidnR1APKUFkiLCnZ2dnUU7-b_NnZ2d@giganews.com>
<-rSdnShOi6s1syLCnZ2dnUU78X_NnZ2d@brightview.co.uk>
<p7SdnUWV3YT3rCLCnZ2dnUU7-KnNnZ2d@giganews.com>
<G9ednQR63dvHUyLCnZ2dnUU78QnNnZ2d@brightview.co.uk>
<PfmdnUdnnqhYTyLCnZ2dnUU7-c3NnZ2d@giganews.com>
<U8ednVm41KijRSLCnZ2dnUU78c_NnZ2d@brightview.co.uk>
<746dnWToYoc6RyLCnZ2dnUU7-N_NnZ2d@giganews.com>
<_eCdnSZdT4qMfCLCnZ2dnUU78I_NnZ2d@brightview.co.uk>
<Q9ydnbikEfeweiLCnZ2dnUU7-R_NnZ2d@giganews.com>
<KJidnf6fW8cunl3CnZ2dnUU78aGdnZ2d@brightview.co.uk>
From: NoO...@NoWhere.com (olcott)
Date: Thu, 26 Nov 2020 13:58:28 -0600
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:78.0) Gecko/20100101
Thunderbird/78.5.0
MIME-Version: 1.0
In-Reply-To: <KJidnf6fW8cunl3CnZ2dnUU78aGdnZ2d@brightview.co.uk>
Content-Type: text/plain; charset=windows-1252; format=flowed
Content-Language: en-US
Content-Transfer-Encoding: 8bit
Message-ID: <7qWdnVHa8r1DlV3CnZ2dnUU7-VHNnZ2d@giganews.com>
Lines: 402
X-Usenet-Provider: http://www.giganews.com
X-Trace: sv3-pvB3UvOnwTylitpMD6PjGb1jIshKsRSlggNNpaZeKRFI8DxsJ8ujR3Jmx71YhqCjCsHeYxbfgQKRJK+!SHeFZUPlClV1tN4xCpqLQdNfL6J85a5SoM3NaiWwwCUp0wRIMY0IhUOQ7OpgZM8l2JXU2GRDva1l!Dw==
X-Complaints-To: abuse@giganews.com
X-DMCA-Notifications: http://www.giganews.com/info/dmca.html
X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers
X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint properly
X-Postfilter: 1.3.40
X-Original-Bytes: 18236
X-Received-Bytes: 18482
X-Received-Body-CRC: 2739665291
View all headers
On 11/26/2020 1:36 PM, Mike Terry wrote:
On 26/11/2020 17:34, olcott wrote:
On 11/26/2020 11:08 AM, Mike Terry wrote:
On 26/11/2020 16:41, olcott wrote:
On 11/26/2020 10:30 AM, Mike Terry wrote:
On 26/11/2020 16:07, olcott wrote:
On 11/26/2020 9:48 AM, Mike Terry wrote:
On 26/11/2020 04:39, olcott wrote:
On 11/25/2020 10:27 PM, Mike Terry wrote:
On 26/11/2020 02:14, olcott wrote:
On 11/25/2020 7:38 PM, Mike Terry wrote:
On 26/11/2020 00:51, olcott wrote:
On 11/25/2020 6:33 PM, Mike Terry wrote:
On 25/11/2020 23:47, olcott wrote:
On 11/25/2020 5:31 PM, Mike Terry wrote:
On 25/11/2020 21:55, olcott wrote:
On 11/25/2020 3:25 PM, Mike Terry wrote:
On 25/11/2020 17:21, olcott wrote:
On 11/25/2020 10:45 AM, Mike Terry wrote:
On 24/11/2020 15:41, Mike Terry wrote:
On 24/11/2020 04:18, olcott wrote:
<.. snip ..>

People can eventually look at all of my code and the
thousands of
lines
of code of the x86 emulator and they can look at the
hundreds of
pages
out output. It all boils down to this:

The simulator merely watches its simulation of the
following
instructions until it sees a function call to 377 from
503
the
second
time with no JCC (Jump-Condition_Code) in-between.


I have told you many times that your test must be
UNSOUND.
You
have
never responded to this, so I've assumed you don't
really
know
whether
your test is sound or unsound (or probably, what that
even
means,
although I've also explained that to you before).

Now you are getting closer to actually coding the test
(which
you
claimed to have "fully coded" two years ago), you are
finally
giving
more details.

So...  what do you think.  Is the following test a SOUND
test
for
non-halting?

   TEST:  "monitor the simulation until there is a
function
           call to 377 from 503 a second time, with no
conditional
           branch inbetween"

Putting it more directly - if some calculation P(I)
triggers the
TEST
(so it contains two calls from 377 from 503, with no
conditional
branch
inbetween), does this genuinely imply that the
calculation
will
never
halt?

Bear in mind that the two calls in question do not
necessarily
occur in
the same "virtual address space", that is to say the two
calls can
[and
in the case of T_Hat(T_Hat) *do* ] occur at /different
levels of
emulation/.   [Your trace notation obscures this simple
fact,
making
everything appear to be in one single virtual process,
when
it's
not.]

What do you think?  This seems to be your primary
intuition
that
triggered all this "refuting" activity, BUT IS IT
ACTUALLY
CORRECT?

Of course, you will say "All my intuitions are
correct by
definition -
I'm never wrong" but that doesn't make it true!  :)

Is TEST *SOUND* ?


Noted: still no response to this basic question.

Mike.

<.. snip non-response to question ..>

I'm not sure if that non-response was deliberate.  I
didn't ask
whether one specified implementation of [whatever] exhibits
infinite
recursion!

In case it was just a misreading, here is the question
again.


   So...  what do you think.  Is the following test a SOUND
test
for
   non-halting?

      TEST:  "monitor the simulation until there is a
function
              call to 377 from 503 a second time, with no
conditional
              branch in-between"

It is much more generic than that.
(1) Keep a global execution trace of every line of user
code.

(2) Whenever any instruction is executed see if it is a
function
call.

(3) If it is a function call find the prior call to this
same
function
from the current machine address (if any) searching backward
through the
global execution trace and counting conditional branch
instructions.

(4) If found and conditional-branch-count == zero terminate
the
input.

Copyright 2020 Pete Olcott (I just wrote that algorithm
right
now).

OK, I always imagined the test would be more general than
just
checking specifically for calls to 377 from 503.  :)  No
problem on
that front.

I'm thinking this is probably the basis of your initial
intuition
that
you could actually detect and handle the type of recursion in
your
fledgeling (at that time) halt decider design.

It is good that you've clarified the test, and yet it seems
you're
reluctant to plainly say that you believe the test works!

logical necessity speaks for itself it doesn't need me for a
cheerleader.


LOL.  I knew you'd do something like that.

OK, so you are saying that if your test detects the behaviour
described, then it's a "logical necessity" that the input being
examined is non-halting?

Yes that is what I am saying.

There - that wasn't so bad, was it?  :)


Can you find a counter-example?

Well, if it's a logical necessity I'm in for a hard time on that
one...

But here's the point:  logical necessity absolutely /does/ need a
cheerleader!  Loads of things are "logically necessary" in that
they
must logically be true, and yet they are not /obviously/ true.
That's
why we have proofs.

This would be one of those scenarios, where even if your claim is
correct, it's not trivially obvious that it's correct, right?

Here is what we're saying:

TEST:
    If a calculation P(I) has a trace of steps
    (s0, s1, s2, s3, .....) and there are two steps s_i
    and s_j, such that si and sj are both unconditional
    branches from A to B, and none of the steps in-between
    s_i and s_j are conditional branches, THEN calculation
    P(I) never halts.

Well that's certainly not a "trivial restatement of word
meanings" or
similar, and so is not seen to correct just on a casual glance.

So obviously where I'm going is : do you have a proof of this?

Now I know you're not one for proofs, and maybe during the
course of
discussion such a proof will fall out (provided the underlying
logic
is correct...)

So to start with, perhaps you can just give your thinking as to
/why/
you believe it to be logically necessary?  [You clearly didn't
wake up
one day and think "hey, what about TEST - oh! it's a logical
necessity, that's handy - I can use it in my halt decider!".
There
was something that led you to consider TEST, and having
considered
it,
you decided for whatever reason it was true...]


Mike.


Let's look at it a little simpler:
HERE:  // current location
  Instructions that cannot possibly exit a loop
THERE: goto HERE;

Can you see how this definitely loops?

I can - and if this was relevant there would be a straight forward
proof that such code loops.

But this isn't like the scenario you are dealing with AT ALL!  What
you are showing here is a kind of "in-process" loop detection.
What
you need is some kind of recursive EMULATION detection.  (Emulation
works differently in this respect.)

I'm pretty sure I explained the difference in a post a couple of
weeks
ago but you never responded.

We are trying to determine whether or not a specific sequence of x86
machine code bytes specify an infinite loop as if this machine code
was
a mathematical formalism.

The only thing that matters is: WHAT DO THE BYTES THEMSELVES SAY?


Well, I understand that the code bytes that you presented, if
executed
by a processor within one single logical thread of execution, would
never terminate - there is an obvious loop.

But that's ignoring the issue of RECURSION, where behaviour is not so
simple.  So what's the next step?  (So far what you've said is no
justification for the RECUSION scenario, which is what you TEST is
concerned with.)

Mike.


The sequences of instructions from HERE to THERE and HERE to HERE are
from actual execution traces. The x86 emulator screens out all dead
code
and only shows us the code that is actually reached.

-HERE:  // current location
-   Instructions that cannot possibly exit a loop
-THERE: goto HERE;

To form a mathematical proof on the basis of the x86 language being
construed as a formal language we only have to derive the complete
list
of every instruction that can possibly exit the above loop and if
there
are none of these between the labels HERE and THERE then we know that
the loop is infinite.

Like I said, that is ok for a "contiguous thread of execution", i.e.
if an x86 processor starts at HERE, and then steps its execution,
executing the instructions, then the processor will go round and round
the loop. The proof is easy.


The case for infinite recursion is similar.

No it's not.  The easy proof for the contiguous thread of execution
does not work in the case where there is recursion.  Or, put more
accurately, it works WITHIN A SINGLE CONTIGUOUS THREAD OF EXECUTION
(the obvious proof still works for this), but *NOT WHEN THE TRACE
ENTRIES CROSS RECURSION LEVELS*.


-HERE: Call Function At Address X
-   Instructions that cannot possibly exit recursion
-HERE: Call Function At Address X

If there are no instructions that can possibly exit recursion between
invocations of the same function from the same machine address, then

Click here to read the complete article
Subject: Re: It is known that a correct halt decider must return false (in this case)[V4](x86 as a formal language)
From: olcott
Newsgroups: comp.theory, comp.ai.philosophy, comp.software-eng
Date: Thu, 26 Nov 2020 20:32 UTC
References: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19
Path: i2pn2.org!i2pn.org!weretis.net!feeder6.news.weretis.net!news.snarked.org!border2.nntp.dca1.giganews.com!nntp.giganews.com!buffer2.nntp.dca1.giganews.com!news.giganews.com.POSTED!not-for-mail
NNTP-Posting-Date: Thu, 26 Nov 2020 14:32:35 -0600
Subject: Re: It is known that a correct halt decider must return false (in
this case)[V4](x86 as a formal language)
Newsgroups: comp.theory,comp.ai.philosophy,comp.software-eng
References: <TqWdnXCuh8jFkibCnZ2dnUU7-QfNnZ2d@giganews.com>
<ZridnafptIUjTyPCnZ2dnUU7-UXNnZ2d@giganews.com>
<zIudnVpmqcfEdCPCnZ2dnUU78aOdnZ2d@brightview.co.uk>
<_PidnS5eJ9eLcCPCnZ2dnUU7-LfNnZ2d@giganews.com>
<Iqmdnbz55_xraiPCnZ2dnUU78V-dnZ2d@brightview.co.uk>
<zf6dnTkZ6Pi-YSPCnZ2dnUU7-TudnZ2d@giganews.com>
<OPKdncr_54uPmiLCnZ2dnUU78QednZ2d@brightview.co.uk>
<NfidnR1APKUFkiLCnZ2dnUU7-b_NnZ2d@giganews.com>
<-rSdnShOi6s1syLCnZ2dnUU78X_NnZ2d@brightview.co.uk>
<p7SdnUWV3YT3rCLCnZ2dnUU7-KnNnZ2d@giganews.com>
<G9ednQR63dvHUyLCnZ2dnUU78QnNnZ2d@brightview.co.uk>
<PfmdnUdnnqhYTyLCnZ2dnUU7-c3NnZ2d@giganews.com>
<U8ednVm41KijRSLCnZ2dnUU78c_NnZ2d@brightview.co.uk>
<746dnWToYoc6RyLCnZ2dnUU7-N_NnZ2d@giganews.com>
<_eCdnSZdT4qMfCLCnZ2dnUU78I_NnZ2d@brightview.co.uk>
<Q9ydnbikEfeweiLCnZ2dnUU7-R_NnZ2d@giganews.com>
<KJidnf6fW8cunl3CnZ2dnUU78aGdnZ2d@brightview.co.uk>
<7qWdnVHa8r1DlV3CnZ2dnUU7-VHNnZ2d@giganews.com>
<WdOdnXv5dK9hkl3CnZ2dnUU78X3NnZ2d@brightview.co.uk>
From: NoO...@NoWhere.com (olcott)
Date: Thu, 26 Nov 2020 14:32:42 -0600
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:78.0) Gecko/20100101
Thunderbird/78.5.0
MIME-Version: 1.0
In-Reply-To: <WdOdnXv5dK9hkl3CnZ2dnUU78X3NnZ2d@brightview.co.uk>
Content-Type: text/plain; charset=windows-1252; format=flowed
Content-Language: en-US
Content-Transfer-Encoding: 8bit
Message-ID: <edqdnc-pcMl-jV3CnZ2dnUU7-QGdnZ2d@giganews.com>
Lines: 456
X-Usenet-Provider: http://www.giganews.com
X-Trace: sv3-SHHqamkWw5HpYJXTy6WzNoRoNVTQGLqNKV5YJuI+BZJkmOKZV36Lt2sFJZzJZexr0T3WuNcSDPEGnI0!ubpIzNOG/Lz7Wro+qPZD2xmK+Xc7wQzje426NpLekHWftzXGtApdBV9S7Nnt0yvIGLRJg6PKuyO8!Aw==
X-Complaints-To: abuse@giganews.com
X-DMCA-Notifications: http://www.giganews.com/info/dmca.html
X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers
X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint properly
X-Postfilter: 1.3.40
X-Original-Bytes: 20487
View all headers
On 11/26/2020 2:28 PM, Mike Terry wrote:
On 26/11/2020 19:58, olcott wrote:
On 11/26/2020 1:36 PM, Mike Terry wrote:
On 26/11/2020 17:34, olcott wrote:
On 11/26/2020 11:08 AM, Mike Terry wrote:
On 26/11/2020 16:41, olcott wrote:
On 11/26/2020 10:30 AM, Mike Terry wrote:
On 26/11/2020 16:07, olcott wrote:
On 11/26/2020 9:48 AM, Mike Terry wrote:
On 26/11/2020 04:39, olcott wrote:
On 11/25/2020 10:27 PM, Mike Terry wrote:
On 26/11/2020 02:14, olcott wrote:
On 11/25/2020 7:38 PM, Mike Terry wrote:
On 26/11/2020 00:51, olcott wrote:
On 11/25/2020 6:33 PM, Mike Terry wrote:
On 25/11/2020 23:47, olcott wrote:
On 11/25/2020 5:31 PM, Mike Terry wrote:
On 25/11/2020 21:55, olcott wrote:
On 11/25/2020 3:25 PM, Mike Terry wrote:
On 25/11/2020 17:21, olcott wrote:
On 11/25/2020 10:45 AM, Mike Terry wrote:
On 24/11/2020 15:41, Mike Terry wrote:
On 24/11/2020 04:18, olcott wrote:
<.. snip ..>

People can eventually look at all of my code and the
thousands of
lines
of code of the x86 emulator and they can look at the
hundreds of
pages
out output. It all boils down to this:

The simulator merely watches its simulation of the
following
instructions until it sees a function call to 377
from
503
the
second
time with no JCC (Jump-Condition_Code) in-between.


I have told you many times that your test must be
UNSOUND.
You
have
never responded to this, so I've assumed you don't
really
know
whether
your test is sound or unsound (or probably, what that
even
means,
although I've also explained that to you before).

Now you are getting closer to actually coding the test
(which
you
claimed to have "fully coded" two years ago), you are
finally
giving
more details.

So...  what do you think.  Is the following test a
SOUND
test
for
non-halting?

   TEST:  "monitor the simulation until there is a
function
           call to 377 from 503 a second time, with no
conditional
           branch inbetween"

Putting it more directly - if some calculation P(I)
triggers the
TEST
(so it contains two calls from 377 from 503, with no
conditional
branch
inbetween), does this genuinely imply that the
calculation
will
never
halt?

Bear in mind that the two calls in question do not
necessarily
occur in
the same "virtual address space", that is to say
the two
calls can
[and
in the case of T_Hat(T_Hat) *do* ] occur at /different
levels of
emulation/.   [Your trace notation obscures this
simple
fact,
making
everything appear to be in one single virtual process,
when
it's
not.]

What do you think?  This seems to be your primary
intuition
that
triggered all this "refuting" activity, BUT IS IT
ACTUALLY
CORRECT?

Of course, you will say "All my intuitions are
correct by
definition -
I'm never wrong" but that doesn't make it true!  :)

Is TEST *SOUND* ?


Noted: still no response to this basic question.

Mike.

<.. snip non-response to question ..>

I'm not sure if that non-response was deliberate.  I
didn't ask
whether one specified implementation of [whatever]
exhibits
infinite
recursion!

In case it was just a misreading, here is the question
again.


   So...  what do you think.  Is the following test a
SOUND
test
for
   non-halting?

      TEST:  "monitor the simulation until there is a
function
              call to 377 from 503 a second time, with no
conditional
              branch in-between"

It is much more generic than that.
(1) Keep a global execution trace of every line of user
code.

(2) Whenever any instruction is executed see if it is a
function
call.

(3) If it is a function call find the prior call to this
same
function
from the current machine address (if any) searching
backward
through the
global execution trace and counting conditional branch
instructions.

(4) If found and conditional-branch-count == zero
terminate
the
input.

Copyright 2020 Pete Olcott (I just wrote that algorithm
right
now).

OK, I always imagined the test would be more general than
just
checking specifically for calls to 377 from 503.  :)  No
problem on
that front.

I'm thinking this is probably the basis of your initial
intuition
that
you could actually detect and handle the type of
recursion in
your
fledgeling (at that time) halt decider design.

It is good that you've clarified the test, and yet it seems
you're
reluctant to plainly say that you believe the test works!

logical necessity speaks for itself it doesn't need me for a
cheerleader.


LOL.  I knew you'd do something like that.

OK, so you are saying that if your test detects the behaviour
described, then it's a "logical necessity" that the input
being
examined is non-halting?

Yes that is what I am saying.

There - that wasn't so bad, was it?  :)


Can you find a counter-example?

Well, if it's a logical necessity I'm in for a hard time on
that
one...

But here's the point:  logical necessity absolutely /does/
need a
cheerleader!  Loads of things are "logically necessary" in that
they
must logically be true, and yet they are not /obviously/ true.
That's
why we have proofs.

This would be one of those scenarios, where even if your
claim is
correct, it's not trivially obvious that it's correct, right?

Here is what we're saying:

TEST:
    If a calculation P(I) has a trace of steps
    (s0, s1, s2, s3, .....) and there are two steps s_i
    and s_j, such that si and sj are both unconditional
    branches from A to B, and none of the steps in-between
    s_i and s_j are conditional branches, THEN calculation
    P(I) never halts.

Well that's certainly not a "trivial restatement of word
meanings" or
similar, and so is not seen to correct just on a casual glance.

So obviously where I'm going is : do you have a proof of this?

Now I know you're not one for proofs, and maybe during the
course of
discussion such a proof will fall out (provided the underlying
logic
is correct...)

So to start with, perhaps you can just give your thinking as to
/why/
you believe it to be logically necessary?  [You clearly didn't
wake up
one day and think "hey, what about TEST - oh! it's a logical
necessity, that's handy - I can use it in my halt decider!".
There
was something that led you to consider TEST, and having
considered
it,
you decided for whatever reason it was true...]


Mike.


Let's look at it a little simpler:
HERE:  // current location
  Instructions that cannot possibly exit a loop
THERE: goto HERE;

Can you see how this definitely loops?

I can - and if this was relevant there would be a straight
forward
proof that such code loops.

But this isn't like the scenario you are dealing with AT ALL!
What
you are showing here is a kind of "in-process" loop detection.
What
you need is some kind of recursive EMULATION detection.
(Emulation
works differently in this respect.)

I'm pretty sure I explained the difference in a post a couple of
weeks
ago but you never responded.

We are trying to determine whether or not a specific sequence
of x86
machine code bytes specify an infinite loop as if this machine
code
was
a mathematical formalism.

The only thing that matters is: WHAT DO THE BYTES THEMSELVES SAY?


Well, I understand that the code bytes that you presented, if
executed
by a processor within one single logical thread of execution, would
never terminate - there is an obvious loop.

But that's ignoring the issue of RECURSION, where behaviour is
not so
simple.  So what's the next step?  (So far what you've said is no
justification for the RECUSION scenario, which is what you TEST is
concerned with.)

Mike.


The sequences of instructions from HERE to THERE and HERE to HERE
are
from actual execution traces. The x86 emulator screens out all dead
code
and only shows us the code that is actually reached.

-HERE:  // current location
-   Instructions that cannot possibly exit a loop
-THERE: goto HERE;

To form a mathematical proof on the basis of the x86 language being
construed as a formal language we only have to derive the complete
list
of every instruction that can possibly exit the above loop and if
there
are none of these between the labels HERE and THERE then we know
that
the loop is infinite.

Like I said, that is ok for a "contiguous thread of execution", i.e.
if an x86 processor starts at HERE, and then steps its execution,
executing the instructions, then the processor will go round and
round
the loop. The proof is easy.


The case for infinite recursion is similar.

No it's not.  The easy proof for the contiguous thread of execution
does not work in the case where there is recursion.  Or, put more
accurately, it works WITHIN A SINGLE CONTIGUOUS THREAD OF EXECUTION
(the obvious proof still works for this), but *NOT WHEN THE TRACE
ENTRIES CROSS RECURSION LEVELS*.


-HERE: Call Function At Address X
-   Instructions that cannot possibly exit recursion
-HERE: Call Function At Address X

Click here to read the complete article
Subject: Re: It is known that a correct halt decider must return false (in this case)[V4](x86 as a formal language)
From: olcott
Newsgroups: comp.theory, comp.ai.philosophy, comp.software-eng
Date: Thu, 26 Nov 2020 20:48 UTC
References: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19
Path: i2pn2.org!i2pn.org!weretis.net!feeder6.news.weretis.net!news.snarked.org!border2.nntp.dca1.giganews.com!nntp.giganews.com!buffer2.nntp.dca1.giganews.com!buffer1.nntp.dca1.giganews.com!news.giganews.com.POSTED!not-for-mail
NNTP-Posting-Date: Thu, 26 Nov 2020 14:47:57 -0600
Subject: Re: It is known that a correct halt decider must return false (in
this case)[V4](x86 as a formal language)
Newsgroups: comp.theory,comp.ai.philosophy,comp.software-eng
References: <TqWdnXCuh8jFkibCnZ2dnUU7-QfNnZ2d@giganews.com>
<_PidnS5eJ9eLcCPCnZ2dnUU7-LfNnZ2d@giganews.com>
<Iqmdnbz55_xraiPCnZ2dnUU78V-dnZ2d@brightview.co.uk>
<zf6dnTkZ6Pi-YSPCnZ2dnUU7-TudnZ2d@giganews.com>
<OPKdncr_54uPmiLCnZ2dnUU78QednZ2d@brightview.co.uk>
<NfidnR1APKUFkiLCnZ2dnUU7-b_NnZ2d@giganews.com>
<-rSdnShOi6s1syLCnZ2dnUU78X_NnZ2d@brightview.co.uk>
<p7SdnUWV3YT3rCLCnZ2dnUU7-KnNnZ2d@giganews.com>
<G9ednQR63dvHUyLCnZ2dnUU78QnNnZ2d@brightview.co.uk>
<PfmdnUdnnqhYTyLCnZ2dnUU7-c3NnZ2d@giganews.com>
<U8ednVm41KijRSLCnZ2dnUU78c_NnZ2d@brightview.co.uk>
<746dnWToYoc6RyLCnZ2dnUU7-N_NnZ2d@giganews.com>
<_eCdnSZdT4qMfCLCnZ2dnUU78I_NnZ2d@brightview.co.uk>
<Q9ydnbikEfeweiLCnZ2dnUU7-R_NnZ2d@giganews.com>
<KJidnf6fW8cunl3CnZ2dnUU78aGdnZ2d@brightview.co.uk>
<7qWdnVHa8r1DlV3CnZ2dnUU7-VHNnZ2d@giganews.com>
<WdOdnXv5dK9hkl3CnZ2dnUU78X3NnZ2d@brightview.co.uk>
<edqdnc-pcMl-jV3CnZ2dnUU7-QGdnZ2d@giganews.com>
<LY-dnbwpXbztjl3CnZ2dnUU78XfNnZ2d@brightview.co.uk>
From: NoO...@NoWhere.com (olcott)
Date: Thu, 26 Nov 2020 14:48:02 -0600
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:78.0) Gecko/20100101
Thunderbird/78.5.0
MIME-Version: 1.0
In-Reply-To: <LY-dnbwpXbztjl3CnZ2dnUU78XfNnZ2d@brightview.co.uk>
Content-Type: text/plain; charset=windows-1252; format=flowed
Content-Language: en-US
Content-Transfer-Encoding: 8bit
Message-ID: <yrKdnbMeAtvgiV3CnZ2dnUU7-THNnZ2d@giganews.com>
Lines: 484
X-Usenet-Provider: http://www.giganews.com
X-Trace: sv3-VkzVP1FmysJvUZLungTwNa1nLztCha49BDpkWLNSbO+7tPKuvMUGDpxJBi+DdXEubfF42QcY46g28Sz!BFMfDNY0hF3ouyv7yirDp9s+8XW8n7TTaJxMC2OLfHHAXuPbAeUmIiMGGbAsKtSZw+psISP4ER+q!hQ==
X-Complaints-To: abuse@giganews.com
X-DMCA-Notifications: http://www.giganews.com/info/dmca.html
X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers
X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint properly
X-Postfilter: 1.3.40
X-Original-Bytes: 21825
View all headers
On 11/26/2020 2:43 PM, Mike Terry wrote:
On 26/11/2020 20:32, olcott wrote:
On 11/26/2020 2:28 PM, Mike Terry wrote:
On 26/11/2020 19:58, olcott wrote:
On 11/26/2020 1:36 PM, Mike Terry wrote:
On 26/11/2020 17:34, olcott wrote:
On 11/26/2020 11:08 AM, Mike Terry wrote:
On 26/11/2020 16:41, olcott wrote:
On 11/26/2020 10:30 AM, Mike Terry wrote:
On 26/11/2020 16:07, olcott wrote:
On 11/26/2020 9:48 AM, Mike Terry wrote:
On 26/11/2020 04:39, olcott wrote:
On 11/25/2020 10:27 PM, Mike Terry wrote:
On 26/11/2020 02:14, olcott wrote:
On 11/25/2020 7:38 PM, Mike Terry wrote:
On 26/11/2020 00:51, olcott wrote:
On 11/25/2020 6:33 PM, Mike Terry wrote:
On 25/11/2020 23:47, olcott wrote:
On 11/25/2020 5:31 PM, Mike Terry wrote:
On 25/11/2020 21:55, olcott wrote:
On 11/25/2020 3:25 PM, Mike Terry wrote:
On 25/11/2020 17:21, olcott wrote:
On 11/25/2020 10:45 AM, Mike Terry wrote:
On 24/11/2020 15:41, Mike Terry wrote:
On 24/11/2020 04:18, olcott wrote:
<.. snip ..>

People can eventually look at all of my code and
the
thousands of
lines
of code of the x86 emulator and they can look at
the
hundreds of
pages
out output. It all boils down to this:

The simulator merely watches its simulation of the
following
instructions until it sees a function call to 377
from
503
the
second
time with no JCC (Jump-Condition_Code) in-between.


I have told you many times that your test must be
UNSOUND.
You
have
never responded to this, so I've assumed you don't
really
know
whether
your test is sound or unsound (or probably, what
that
even
means,
although I've also explained that to you before).

Now you are getting closer to actually coding the
test
(which
you
claimed to have "fully coded" two years ago), you
are
finally
giving
more details.

So...  what do you think.  Is the following test a
SOUND
test
for
non-halting?

   TEST:  "monitor the simulation until there is a
function
           call to 377 from 503 a second time,
with no
conditional
           branch inbetween"

Putting it more directly - if some calculation P(I)
triggers the
TEST
(so it contains two calls from 377 from 503, with no
conditional
branch
inbetween), does this genuinely imply that the
calculation
will
never
halt?

Bear in mind that the two calls in question do not
necessarily
occur in
the same "virtual address space", that is to say
the two
calls can
[and
in the case of T_Hat(T_Hat) *do* ] occur at
/different
levels of
emulation/.   [Your trace notation obscures this
simple
fact,
making
everything appear to be in one single virtual
process,
when
it's
not.]

What do you think?  This seems to be your primary
intuition
that
triggered all this "refuting" activity, BUT IS IT
ACTUALLY
CORRECT?

Of course, you will say "All my intuitions are
correct by
definition -
I'm never wrong" but that doesn't make it true!  :)

Is TEST *SOUND* ?


Noted: still no response to this basic question.

Mike.

<.. snip non-response to question ..>

I'm not sure if that non-response was deliberate.  I
didn't ask
whether one specified implementation of [whatever]
exhibits
infinite
recursion!

In case it was just a misreading, here is the question
again.


   So...  what do you think.  Is the following test a
SOUND
test
for
   non-halting?

      TEST:  "monitor the simulation until there is a
function
              call to 377 from 503 a second time,
with no
conditional
              branch in-between"

It is much more generic than that.
(1) Keep a global execution trace of every line of user
code.

(2) Whenever any instruction is executed see if it is a
function
call.

(3) If it is a function call find the prior call to this
same
function
from the current machine address (if any) searching
backward
through the
global execution trace and counting conditional branch
instructions.

(4) If found and conditional-branch-count == zero
terminate
the
input.

Copyright 2020 Pete Olcott (I just wrote that algorithm
right
now).

OK, I always imagined the test would be more general than
just
checking specifically for calls to 377 from 503.  :)  No
problem on
that front.

I'm thinking this is probably the basis of your initial
intuition
that
you could actually detect and handle the type of
recursion in
your
fledgeling (at that time) halt decider design.

It is good that you've clarified the test, and yet it
seems
you're
reluctant to plainly say that you believe the test works!

logical necessity speaks for itself it doesn't need me
for a
cheerleader.


LOL.  I knew you'd do something like that.

OK, so you are saying that if your test detects the
behaviour
described, then it's a "logical necessity" that the input
being
examined is non-halting?

Yes that is what I am saying.

There - that wasn't so bad, was it?  :)


Can you find a counter-example?

Well, if it's a logical necessity I'm in for a hard time on
that
one...

But here's the point:  logical necessity absolutely /does/
need a
cheerleader!  Loads of things are "logically necessary" in
that
they
must logically be true, and yet they are not /obviously/
true.
That's
why we have proofs.

This would be one of those scenarios, where even if your
claim is
correct, it's not trivially obvious that it's correct, right?

Here is what we're saying:

TEST:
    If a calculation P(I) has a trace of steps
    (s0, s1, s2, s3, .....) and there are two steps s_i
    and s_j, such that si and sj are both unconditional
    branches from A to B, and none of the steps in-between
    s_i and s_j are conditional branches, THEN calculation
    P(I) never halts.

Well that's certainly not a "trivial restatement of word
meanings" or
similar, and so is not seen to correct just on a casual
glance.

So obviously where I'm going is : do you have a proof of
this?

Now I know you're not one for proofs, and maybe during the
course of
discussion such a proof will fall out (provided the
underlying
logic
is correct...)

So to start with, perhaps you can just give your thinking
as to
/why/
you believe it to be logically necessary?  [You clearly
didn't
wake up
one day and think "hey, what about TEST - oh! it's a logical
necessity, that's handy - I can use it in my halt decider!".
There
was something that led you to consider TEST, and having
considered
it,
you decided for whatever reason it was true...]


Mike.


Let's look at it a little simpler:
HERE:  // current location
  Instructions that cannot possibly exit a loop
THERE: goto HERE;

Can you see how this definitely loops?

I can - and if this was relevant there would be a straight
forward
proof that such code loops.

But this isn't like the scenario you are dealing with AT ALL!
What
you are showing here is a kind of "in-process" loop detection.
What
you need is some kind of recursive EMULATION detection.
(Emulation
works differently in this respect.)

I'm pretty sure I explained the difference in a post a
couple of
weeks
ago but you never responded.

We are trying to determine whether or not a specific sequence
of x86
machine code bytes specify an infinite loop as if this machine
code
was
a mathematical formalism.

The only thing that matters is: WHAT DO THE BYTES THEMSELVES
SAY?


Well, I understand that the code bytes that you presented, if
executed
by a processor within one single logical thread of execution,
would
never terminate - there is an obvious loop.

But that's ignoring the issue of RECURSION, where behaviour is
not so
simple.  So what's the next step?  (So far what you've said is no
justification for the RECUSION scenario, which is what you
TEST is
concerned with.)

Mike.


The sequences of instructions from HERE to THERE and HERE to HERE
are
from actual execution traces. The x86 emulator screens out all
dead
code
and only shows us the code that is actually reached.

-HERE:  // current location
-   Instructions that cannot possibly exit a loop
-THERE: goto HERE;

To form a mathematical proof on the basis of the x86 language
being
construed as a formal language we only have to derive the complete
list
of every instruction that can possibly exit the above loop and if
there
are none of these between the labels HERE and THERE then we know
that
the loop is infinite.

Like I said, that is ok for a "contiguous thread of execution",
i.e.
if an x86 processor starts at HERE, and then steps its execution,
executing the instructions, then the processor will go round and
round
the loop. The proof is easy.


The case for infinite recursion is similar.

No it's not.  The easy proof for the contiguous thread of execution
does not work in the case where there is recursion.  Or, put more
accurately, it works WITHIN A SINGLE CONTIGUOUS THREAD OF EXECUTION
(the obvious proof still works for this), but *NOT WHEN THE TRACE

Click here to read the complete article
Subject: Re: It is known that a correct halt decider must return false (in this case)[V4](x86 as a formal language)
From: olcott
Newsgroups: comp.theory, comp.ai.philosophy, comp.software-eng
Date: Thu, 26 Nov 2020 20:50 UTC
References: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19
Path: i2pn2.org!i2pn.org!weretis.net!feeder6.news.weretis.net!news.snarked.org!border2.nntp.dca1.giganews.com!nntp.giganews.com!buffer2.nntp.dca1.giganews.com!news.giganews.com.POSTED!not-for-mail
NNTP-Posting-Date: Thu, 26 Nov 2020 14:50:12 -0600
Subject: Re: It is known that a correct halt decider must return false (in
this case)[V4](x86 as a formal language)
Newsgroups: comp.theory,comp.ai.philosophy,comp.software-eng
References: <TqWdnXCuh8jFkibCnZ2dnUU7-QfNnZ2d@giganews.com>
<_PidnS5eJ9eLcCPCnZ2dnUU7-LfNnZ2d@giganews.com>
<Iqmdnbz55_xraiPCnZ2dnUU78V-dnZ2d@brightview.co.uk>
<zf6dnTkZ6Pi-YSPCnZ2dnUU7-TudnZ2d@giganews.com>
<OPKdncr_54uPmiLCnZ2dnUU78QednZ2d@brightview.co.uk>
<NfidnR1APKUFkiLCnZ2dnUU7-b_NnZ2d@giganews.com>
<-rSdnShOi6s1syLCnZ2dnUU78X_NnZ2d@brightview.co.uk>
<p7SdnUWV3YT3rCLCnZ2dnUU7-KnNnZ2d@giganews.com>
<G9ednQR63dvHUyLCnZ2dnUU78QnNnZ2d@brightview.co.uk>
<PfmdnUdnnqhYTyLCnZ2dnUU7-c3NnZ2d@giganews.com>
<U8ednVm41KijRSLCnZ2dnUU78c_NnZ2d@brightview.co.uk>
<746dnWToYoc6RyLCnZ2dnUU7-N_NnZ2d@giganews.com>
<_eCdnSZdT4qMfCLCnZ2dnUU78I_NnZ2d@brightview.co.uk>
<Q9ydnbikEfeweiLCnZ2dnUU7-R_NnZ2d@giganews.com>
<KJidnf6fW8cunl3CnZ2dnUU78aGdnZ2d@brightview.co.uk>
<7qWdnVHa8r1DlV3CnZ2dnUU7-VHNnZ2d@giganews.com>
<WdOdnXv5dK9hkl3CnZ2dnUU78X3NnZ2d@brightview.co.uk>
<edqdnc-pcMl-jV3CnZ2dnUU7-QGdnZ2d@giganews.com>
<LY-dnbwpXbztjl3CnZ2dnUU78XfNnZ2d@brightview.co.uk>
From: NoO...@NoWhere.com (olcott)
Date: Thu, 26 Nov 2020 14:50:18 -0600
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:78.0) Gecko/20100101
Thunderbird/78.5.0
MIME-Version: 1.0
In-Reply-To: <LY-dnbwpXbztjl3CnZ2dnUU78XfNnZ2d@brightview.co.uk>
Content-Type: text/plain; charset=windows-1252; format=flowed
Content-Language: en-US
Content-Transfer-Encoding: 8bit
Message-ID: <yrKdnbIeAtuZiF3CnZ2dnUU7-TGdnZ2d@giganews.com>
Lines: 508
X-Usenet-Provider: http://www.giganews.com
X-Trace: sv3-DryL4JS/2DuClB4C1CQllM9TCol/HynJqfJ4hLXnbtkkcWrR77fOOuYT2GCzgV7Q82HOuCizz8nyJK/!OzSEo4vJ8gnQIiy73Eg9JXa+t0P6+ykFDHV5WxHv82RetRJNbtv02I827qHWegAKHN50HtQ6YIsa!tg==
X-Complaints-To: abuse@giganews.com
X-DMCA-Notifications: http://www.giganews.com/info/dmca.html
X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers
X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint properly
X-Postfilter: 1.3.40
X-Original-Bytes: 22145
View all headers
On 11/26/2020 2:43 PM, Mike Terry wrote:
On 26/11/2020 20:32, olcott wrote:
On 11/26/2020 2:28 PM, Mike Terry wrote:
On 26/11/2020 19:58, olcott wrote:
On 11/26/2020 1:36 PM, Mike Terry wrote:
On 26/11/2020 17:34, olcott wrote:
On 11/26/2020 11:08 AM, Mike Terry wrote:
On 26/11/2020 16:41, olcott wrote:
On 11/26/2020 10:30 AM, Mike Terry wrote:
On 26/11/2020 16:07, olcott wrote:
On 11/26/2020 9:48 AM, Mike Terry wrote:
On 26/11/2020 04:39, olcott wrote:
On 11/25/2020 10:27 PM, Mike Terry wrote:
On 26/11/2020 02:14, olcott wrote:
On 11/25/2020 7:38 PM, Mike Terry wrote:
On 26/11/2020 00:51, olcott wrote:
On 11/25/2020 6:33 PM, Mike Terry wrote:
On 25/11/2020 23:47, olcott wrote:
On 11/25/2020 5:31 PM, Mike Terry wrote:
On 25/11/2020 21:55, olcott wrote:
On 11/25/2020 3:25 PM, Mike Terry wrote:
On 25/11/2020 17:21, olcott wrote:
On 11/25/2020 10:45 AM, Mike Terry wrote:
On 24/11/2020 15:41, Mike Terry wrote:
On 24/11/2020 04:18, olcott wrote:
<.. snip ..>

People can eventually look at all of my code and
the
thousands of
lines
of code of the x86 emulator and they can look at
the
hundreds of
pages
out output. It all boils down to this:

The simulator merely watches its simulation of the
following
instructions until it sees a function call to 377
from
503
the
second
time with no JCC (Jump-Condition_Code) in-between.


I have told you many times that your test must be
UNSOUND.
You
have
never responded to this, so I've assumed you don't
really
know
whether
your test is sound or unsound (or probably, what
that
even
means,
although I've also explained that to you before).

Now you are getting closer to actually coding the
test
(which
you
claimed to have "fully coded" two years ago), you
are
finally
giving
more details.

So...  what do you think.  Is the following test a
SOUND
test
for
non-halting?

   TEST:  "monitor the simulation until there is a
function
           call to 377 from 503 a second time,
with no
conditional
           branch inbetween"

Putting it more directly - if some calculation P(I)
triggers the
TEST
(so it contains two calls from 377 from 503, with no
conditional
branch
inbetween), does this genuinely imply that the
calculation
will
never
halt?

Bear in mind that the two calls in question do not
necessarily
occur in
the same "virtual address space", that is to say
the two
calls can
[and
in the case of T_Hat(T_Hat) *do* ] occur at
/different
levels of
emulation/.   [Your trace notation obscures this
simple
fact,
making
everything appear to be in one single virtual
process,
when
it's
not.]

What do you think?  This seems to be your primary
intuition
that
triggered all this "refuting" activity, BUT IS IT
ACTUALLY
CORRECT?

Of course, you will say "All my intuitions are
correct by
definition -
I'm never wrong" but that doesn't make it true!  :)

Is TEST *SOUND* ?


Noted: still no response to this basic question.

Mike.

<.. snip non-response to question ..>

I'm not sure if that non-response was deliberate.  I
didn't ask
whether one specified implementation of [whatever]
exhibits
infinite
recursion!

In case it was just a misreading, here is the question
again.


   So...  what do you think.  Is the following test a
SOUND
test
for
   non-halting?

      TEST:  "monitor the simulation until there is a
function
              call to 377 from 503 a second time,
with no
conditional
              branch in-between"

It is much more generic than that.
(1) Keep a global execution trace of every line of user
code.

(2) Whenever any instruction is executed see if it is a
function
call.

(3) If it is a function call find the prior call to this
same
function
from the current machine address (if any) searching
backward
through the
global execution trace and counting conditional branch
instructions.

(4) If found and conditional-branch-count == zero
terminate
the
input.

Copyright 2020 Pete Olcott (I just wrote that algorithm
right
now).

OK, I always imagined the test would be more general than
just
checking specifically for calls to 377 from 503.  :)  No
problem on
that front.

I'm thinking this is probably the basis of your initial
intuition
that
you could actually detect and handle the type of
recursion in
your
fledgeling (at that time) halt decider design.

It is good that you've clarified the test, and yet it
seems
you're
reluctant to plainly say that you believe the test works!

logical necessity speaks for itself it doesn't need me
for a
cheerleader.


LOL.  I knew you'd do something like that.

OK, so you are saying that if your test detects the
behaviour
described, then it's a "logical necessity" that the input
being
examined is non-halting?

Yes that is what I am saying.

There - that wasn't so bad, was it?  :)


Can you find a counter-example?

Well, if it's a logical necessity I'm in for a hard time on
that
one...

But here's the point:  logical necessity absolutely /does/
need a
cheerleader!  Loads of things are "logically necessary" in
that
they
must logically be true, and yet they are not /obviously/
true.
That's
why we have proofs.

This would be one of those scenarios, where even if your
claim is
correct, it's not trivially obvious that it's correct, right?

Here is what we're saying:

TEST:
    If a calculation P(I) has a trace of steps
    (s0, s1, s2, s3, .....) and there are two steps s_i
    and s_j, such that si and sj are both unconditional
    branches from A to B, and none of the steps in-between
    s_i and s_j are conditional branches, THEN calculation
    P(I) never halts.

Well that's certainly not a "trivial restatement of word
meanings" or
similar, and so is not seen to correct just on a casual
glance.

So obviously where I'm going is : do you have a proof of
this?

Now I know you're not one for proofs, and maybe during the
course of
discussion such a proof will fall out (provided the
underlying
logic
is correct...)

So to start with, perhaps you can just give your thinking
as to
/why/
you believe it to be logically necessary?  [You clearly
didn't
wake up
one day and think "hey, what about TEST - oh! it's a logical
necessity, that's handy - I can use it in my halt decider!".
There
was something that led you to consider TEST, and having
considered
it,
you decided for whatever reason it was true...]


Mike.


Let's look at it a little simpler:
HERE:  // current location
  Instructions that cannot possibly exit a loop
THERE: goto HERE;

Can you see how this definitely loops?

I can - and if this was relevant there would be a straight
forward
proof that such code loops.

But this isn't like the scenario you are dealing with AT ALL!
What
you are showing here is a kind of "in-process" loop detection.
What
you need is some kind of recursive EMULATION detection.
(Emulation
works differently in this respect.)

I'm pretty sure I explained the difference in a post a
couple of
weeks
ago but you never responded.

We are trying to determine whether or not a specific sequence
of x86
machine code bytes specify an infinite loop as if this machine
code
was
a mathematical formalism.

The only thing that matters is: WHAT DO THE BYTES THEMSELVES
SAY?


Well, I understand that the code bytes that you presented, if
executed
by a processor within one single logical thread of execution,
would
never terminate - there is an obvious loop.

But that's ignoring the issue of RECURSION, where behaviour is
not so
simple.  So what's the next step?  (So far what you've said is no
justification for the RECUSION scenario, which is what you
TEST is
concerned with.)

Mike.


The sequences of instructions from HERE to THERE and HERE to HERE
are
from actual execution traces. The x86 emulator screens out all
dead
code
and only shows us the code that is actually reached.

-HERE:  // current location
-   Instructions that cannot possibly exit a loop
-THERE: goto HERE;

To form a mathematical proof on the basis of the x86 language
being
construed as a formal language we only have to derive the complete
list
of every instruction that can possibly exit the above loop and if
there
are none of these between the labels HERE and THERE then we know
that
the loop is infinite.

Like I said, that is ok for a "contiguous thread of execution",
i.e.
if an x86 processor starts at HERE, and then steps its execution,
executing the instructions, then the processor will go round and
round
the loop. The proof is easy.


The case for infinite recursion is similar.

No it's not.  The easy proof for the contiguous thread of execution
does not work in the case where there is recursion.  Or, put more
accurately, it works WITHIN A SINGLE CONTIGUOUS THREAD OF EXECUTION
(the obvious proof still works for this), but *NOT WHEN THE TRACE

Click here to read the complete article
Subject: Re: It is known that a correct halt decider must return false (in this case)[V4](x86 as a formal language)
From: olcott
Newsgroups: comp.theory, comp.ai.philosophy, comp.software-eng
Date: Thu, 26 Nov 2020 21:16 UTC
References: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19
Path: i2pn2.org!i2pn.org!aioe.org!peer03.ams4!peer.am4.highwinds-media.com!news.highwinds-media.com!tr1.eu1.usenetexpress.com!feeder.usenetexpress.com!tr1.iad1.usenetexpress.com!border1.nntp.dca1.giganews.com!nntp.giganews.com!buffer1.nntp.dca1.giganews.com!news.giganews.com.POSTED!not-for-mail
NNTP-Posting-Date: Thu, 26 Nov 2020 15:16:38 -0600
Subject: Re: It is known that a correct halt decider must return false (in this case)[V4](x86 as a formal language)
Newsgroups: comp.theory,comp.ai.philosophy,comp.software-eng
References: <TqWdnXCuh8jFkibCnZ2dnUU7-QfNnZ2d@giganews.com> <zf6dnTkZ6Pi-YSPCnZ2dnUU7-TudnZ2d@giganews.com> <OPKdncr_54uPmiLCnZ2dnUU78QednZ2d@brightview.co.uk> <NfidnR1APKUFkiLCnZ2dnUU7-b_NnZ2d@giganews.com> <-rSdnShOi6s1syLCnZ2dnUU78X_NnZ2d@brightview.co.uk> <p7SdnUWV3YT3rCLCnZ2dnUU7-KnNnZ2d@giganews.com> <G9ednQR63dvHUyLCnZ2dnUU78QnNnZ2d@brightview.co.uk> <PfmdnUdnnqhYTyLCnZ2dnUU7-c3NnZ2d@giganews.com> <U8ednVm41KijRSLCnZ2dnUU78c_NnZ2d@brightview.co.uk> <746dnWToYoc6RyLCnZ2dnUU7-N_NnZ2d@giganews.com> <_eCdnSZdT4qMfCLCnZ2dnUU78I_NnZ2d@brightview.co.uk> <Q9ydnbikEfeweiLCnZ2dnUU7-R_NnZ2d@giganews.com> <KJidnf6fW8cunl3CnZ2dnUU78aGdnZ2d@brightview.co.uk> <7qWdnVHa8r1DlV3CnZ2dnUU7-VHNnZ2d@giganews.com> <WdOdnXv5dK9hkl3CnZ2dnUU78X3NnZ2d@brightview.co.uk> <edqdnc-pcMl-jV3CnZ2dnUU7-QGdnZ2d@giganews.com> <LY-dnbwpXbztjl3CnZ2dnUU78XfNnZ2d@brightview.co.uk> <yrKdnbIeAtuZiF3CnZ2dnUU7-TGdnZ2d@giganews.com> <vIGdnXPT4om4h13CnZ2dnUU78TXNnZ2d@brightview.co.uk>
From: NoO...@NoWhere.com (olcott)
Date: Thu, 26 Nov 2020 15:16:43 -0600
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:78.0) Gecko/20100101 Thunderbird/78.5.0
MIME-Version: 1.0
In-Reply-To: <vIGdnXPT4om4h13CnZ2dnUU78TXNnZ2d@brightview.co.uk>
Content-Type: text/plain; charset=windows-1252; format=flowed
Content-Language: en-US
Content-Transfer-Encoding: 8bit
Message-ID: <OPGdnZp2OtSrhl3CnZ2dnUU7-L3NnZ2d@giganews.com>
Lines: 569
X-Usenet-Provider: http://www.giganews.com
X-Trace: sv3-KroaItP5zmD4D2hYDy2TyhnN7mnrcMHcNq/ryP+qLf2rt5B1X7pBvO2QEITgBy9dCzMiEq4jcDvcBTo!NNN9gRrLi8c5UawH/u4cMwH0EzkCqZXaB3Hup8KYdEZNDww8+ycl+pz2GRvDl2BOL3rX1K3q3RrS!LQ==
X-Complaints-To: abuse@giganews.com
X-DMCA-Notifications: http://www.giganews.com/info/dmca.html
X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers
X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint properly
X-Postfilter: 1.3.40
X-Original-Bytes: 24715
X-Received-Bytes: 24846
X-Received-Body-CRC: 2307450355
View all headers
On 11/26/2020 3:12 PM, Mike Terry wrote:
On 26/11/2020 20:50, olcott wrote:
On 11/26/2020 2:43 PM, Mike Terry wrote:
On 26/11/2020 20:32, olcott wrote:
On 11/26/2020 2:28 PM, Mike Terry wrote:
On 26/11/2020 19:58, olcott wrote:
On 11/26/2020 1:36 PM, Mike Terry wrote:
On 26/11/2020 17:34, olcott wrote:
On 11/26/2020 11:08 AM, Mike Terry wrote:
On 26/11/2020 16:41, olcott wrote:
On 11/26/2020 10:30 AM, Mike Terry wrote:
On 26/11/2020 16:07, olcott wrote:
On 11/26/2020 9:48 AM, Mike Terry wrote:
On 26/11/2020 04:39, olcott wrote:
On 11/25/2020 10:27 PM, Mike Terry wrote:
On 26/11/2020 02:14, olcott wrote:
On 11/25/2020 7:38 PM, Mike Terry wrote:
On 26/11/2020 00:51, olcott wrote:
On 11/25/2020 6:33 PM, Mike Terry wrote:
On 25/11/2020 23:47, olcott wrote:
On 11/25/2020 5:31 PM, Mike Terry wrote:
On 25/11/2020 21:55, olcott wrote:
On 11/25/2020 3:25 PM, Mike Terry wrote:
On 25/11/2020 17:21, olcott wrote:
On 11/25/2020 10:45 AM, Mike Terry wrote:
On 24/11/2020 15:41, Mike Terry wrote:
On 24/11/2020 04:18, olcott wrote:
<.. snip ..>

People can eventually look at all of my code and
the
thousands of
lines
of code of the x86 emulator and they can look at
the
hundreds of
pages
out output. It all boils down to this:

The simulator merely watches its simulation of
the
following
instructions until it sees a function call to 377
from
503
the
second
time with no JCC (Jump-Condition_Code)
in-between.


I have told you many times that your test must be
UNSOUND.
You
have
never responded to this, so I've assumed you don't
really
know
whether
your test is sound or unsound (or probably, what
that
even
means,
although I've also explained that to you before).

Now you are getting closer to actually coding the
test
(which
you
claimed to have "fully coded" two years ago), you
are
finally
giving
more details.

So...  what do you think.  Is the following test a
SOUND
test
for
non-halting?

   TEST:  "monitor the simulation until there is a
function
           call to 377 from 503 a second time,
with no
conditional
           branch inbetween"

Putting it more directly - if some calculation
P(I)
triggers the
TEST
(so it contains two calls from 377 from 503,
with no
conditional
branch
inbetween), does this genuinely imply that the
calculation
will
never
halt?

Bear in mind that the two calls in question do not
necessarily
occur in
the same "virtual address space", that is to say
the two
calls can
[and
in the case of T_Hat(T_Hat) *do* ] occur at
/different
levels of
emulation/.   [Your trace notation obscures this
simple
fact,
making
everything appear to be in one single virtual
process,
when
it's
not.]

What do you think?  This seems to be your primary
intuition
that
triggered all this "refuting" activity, BUT IS IT
ACTUALLY
CORRECT?

Of course, you will say "All my intuitions are
correct by
definition -
I'm never wrong" but that doesn't make it
true!  :)

Is TEST *SOUND* ?


Noted: still no response to this basic question.

Mike.

<.. snip non-response to question ..>

I'm not sure if that non-response was deliberate.  I
didn't ask
whether one specified implementation of [whatever]
exhibits
infinite
recursion!

In case it was just a misreading, here is the
question
again.


   So...  what do you think.  Is the following test a
SOUND
test
for
   non-halting?

      TEST:  "monitor the simulation until there is a
function
              call to 377 from 503 a second time,
with no
conditional
              branch in-between"

It is much more generic than that.
(1) Keep a global execution trace of every line of
user
code.

(2) Whenever any instruction is executed see if it
is a
function
call.

(3) If it is a function call find the prior call to
this
same
function
from the current machine address (if any) searching
backward
through the
global execution trace and counting conditional branch
instructions.

(4) If found and conditional-branch-count == zero
terminate
the
input.

Copyright 2020 Pete Olcott (I just wrote that
algorithm
right
now).

OK, I always imagined the test would be more general
than
just
checking specifically for calls to 377 from 503.
:)  No
problem on
that front.

I'm thinking this is probably the basis of your initial
intuition
that
you could actually detect and handle the type of
recursion in
your
fledgeling (at that time) halt decider design.

It is good that you've clarified the test, and yet it
seems
you're
reluctant to plainly say that you believe the test
works!

logical necessity speaks for itself it doesn't need me
for a
cheerleader.


LOL.  I knew you'd do something like that.

OK, so you are saying that if your test detects the
behaviour
described, then it's a "logical necessity" that the input
being
examined is non-halting?

Yes that is what I am saying.

There - that wasn't so bad, was it?  :)


Can you find a counter-example?

Well, if it's a logical necessity I'm in for a hard time on
that
one...

But here's the point:  logical necessity absolutely /does/
need a
cheerleader!  Loads of things are "logically necessary" in
that
they
must logically be true, and yet they are not /obviously/
true.
That's
why we have proofs.

This would be one of those scenarios, where even if your
claim is
correct, it's not trivially obvious that it's correct,
right?

Here is what we're saying:

TEST:
    If a calculation P(I) has a trace of steps
    (s0, s1, s2, s3, .....) and there are two steps s_i
    and s_j, such that si and sj are both unconditional
    branches from A to B, and none of the steps in-between
    s_i and s_j are conditional branches, THEN calculation
    P(I) never halts.

Well that's certainly not a "trivial restatement of word
meanings" or
similar, and so is not seen to correct just on a casual
glance.

So obviously where I'm going is : do you have a proof of
this?

Now I know you're not one for proofs, and maybe during the
course of
discussion such a proof will fall out (provided the
underlying
logic
is correct...)

So to start with, perhaps you can just give your thinking
as to
/why/
you believe it to be logically necessary?  [You clearly
didn't
wake up
one day and think "hey, what about TEST - oh! it's a
logical
necessity, that's handy - I can use it in my halt
decider!".
There
was something that led you to consider TEST, and having
considered
it,
you decided for whatever reason it was true...]


Mike.


Let's look at it a little simpler:
HERE:  // current location
  Instructions that cannot possibly exit a loop
THERE: goto HERE;

Can you see how this definitely loops?

I can - and if this was relevant there would be a straight
forward
proof that such code loops.

But this isn't like the scenario you are dealing with AT ALL!
What
you are showing here is a kind of "in-process" loop
detection.
What
you need is some kind of recursive EMULATION detection.
(Emulation
works differently in this respect.)

I'm pretty sure I explained the difference in a post a
couple of
weeks
ago but you never responded.

We are trying to determine whether or not a specific sequence
of x86
machine code bytes specify an infinite loop as if this machine
code
was
a mathematical formalism.

The only thing that matters is: WHAT DO THE BYTES THEMSELVES
SAY?


Well, I understand that the code bytes that you presented, if
executed
by a processor within one single logical thread of execution,
would
never terminate - there is an obvious loop.

But that's ignoring the issue of RECURSION, where behaviour is
not so
simple.  So what's the next step?  (So far what you've said
is no
justification for the RECUSION scenario, which is what you
TEST is
concerned with.)

Mike.


The sequences of instructions from HERE to THERE and HERE to
HERE
are
from actual execution traces. The x86 emulator screens out all
dead
code
and only shows us the code that is actually reached.

-HERE:  // current location
-   Instructions that cannot possibly exit a loop
-THERE: goto HERE;

To form a mathematical proof on the basis of the x86 language
being
construed as a formal language we only have to derive the
complete
list
of every instruction that can possibly exit the above loop
and if
there
are none of these between the labels HERE and THERE then we know
that
the loop is infinite.

Like I said, that is ok for a "contiguous thread of execution",
i.e.
if an x86 processor starts at HERE, and then steps its execution,
executing the instructions, then the processor will go round and
round
the loop. The proof is easy.


The case for infinite recursion is similar.

No it's not.  The easy proof for the contiguous thread of
execution
does not work in the case where there is recursion.  Or, put more

Click here to read the complete article
Pages:1234
rocksolid light 0.7.2
clearneti2ptor