Rocksolid Light

Welcome to novaBBS (click a section below)

mail  files  register  nodelist  faq  login

The steady state of disks is full. -- Ken Thompson


programming / comp.lang.asm.x86 / Re: Refuting the {Linz, Sipser, Kozen} HP Proofs (Ben's example)

SubjectAuthor
* Re: Refuting the {Linz, Sipser, Kozen} HP Proofs (Ben's example)olcott
`- Re: Refuting the {Linz, Sipser, Kozen} HP Proofs (Ben's example)Kaz Kylheku

1
Subject: Re: Refuting the {Linz, Sipser, Kozen} HP Proofs (Ben's example)
From: olcott
Newsgroups: comp.theory, comp.ai.philosophy, comp.lang.asm.x86
Organization: A noiseless patient Spider
Date: Thu, 17 Dec 2020 05:10 UTC
References: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24
Path: i2pn2.org!i2pn.org!eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: NoO...@nospicedham.NoWhere.com (olcott)
Newsgroups: comp.theory,comp.ai.philosophy,comp.lang.asm.x86
Subject: Re: Refuting the {Linz, Sipser, Kozen} HP Proofs (Ben's example)
Date: Wed, 16 Dec 2020 23:10:29 -0600
Organization: A noiseless patient Spider
Lines: 75
Approved: fbkotler@myfairpoint.net - comp.lang.asm.x86 moderation team.
Message-ID: <0L2dnSYm4ejbdUfCnZ2dnUU7-YnNnZ2d@giganews.com>
References: <3JSdnRrpiNHInV3CnZ2dnUU7-YHNnZ2d@giganews.com>
<87v9d57srg.fsf@bsb.me.uk> <yK2dnXzXs69GQkXCnZ2dnUU7-dvNnZ2d@giganews.com>
<875z5262oy.fsf@bsb.me.uk> <XKWdnc8Hn9oQzkTCnZ2dnUU7-RHNnZ2d@giganews.com>
<877dpi4ksa.fsf@bsb.me.uk> <S7WdnVxdtqB7-0TCnZ2dnUU7-TPNnZ2d@giganews.com>
<6b106784-3f6a-44c3-ad5b-646adba93fe6n@googlegroups.com>
<IoGdndKfvMgzw0fCnZ2dnUU7-WvNnZ2d@giganews.com> <rrdomo$4ta$1@dont-email.me>
<If6dnUUqRMbH9UfCnZ2dnUU7-e_NnZ2d@giganews.com> <rrdqe4$i7d$1@dont-email.me>
<kOydnRDlOZQZ6EfCnZ2dnUU7-XPNnZ2d@giganews.com> <rrdtd6$a4j$1@dont-email.me>
<DaGdnXUvT8KlEUfCnZ2dnUU7-VXNnZ2d@giganews.com> <rre588$gv5$1@dont-email.me>
<N8KdnVLL45clBkfCnZ2dnUU7-e3NnZ2d@giganews.com>
<20201216162234.114@kylheku.com>
<zaOdnU6LUeoIMUfCnZ2dnUU7-SXNnZ2d@giganews.com>
<20201216174857.611@kylheku.com>
<ttKdnaPKJbLzW0fCnZ2dnUU7-cnNnZ2d@giganews.com>
<20201216202107.24@kylheku.com>
<Xu6dncrJz_bhQ0fCnZ2dnUU7-e3NnZ2d@giganews.com>
<20201216204022.111@kylheku.com>
Mime-Version: 1.0
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Info: reader02.eternal-september.org; posting-host="4a23faa1200c6b29da9d0c80fbd9723f";
logging-data="4972"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX18a3VJy091ENbEcC6qBj1Lhcrk0njlZzaI="
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:78.0) Gecko/20100101
Thunderbird/78.5.1
Cancel-Lock: sha1:zlpagMHurpgI/seE+avmsrdphcw=
View all headers
On 12/16/2020 10:50 PM, Kaz Kylheku wrote:
On 2020-12-17, olcott <NoOne@NoWhere.com> wrote:
On 12/16/2020 10:24 PM, Kaz Kylheku wrote:
On 2020-12-17, olcott <NoOne@NoWhere.com> wrote:
On 12/16/2020 7:51 PM, Kaz Kylheku wrote:
If the progression is caused by an infinite recursion of a function
with the same paraemters, then all of the simulation levels are
indistinguishable. No UTM knows how many levels are above,
and each one has the same number of identical levels below.

That's it.


If we allowed the infinite recursion to infinitely recur this would be
true. We cut off the otherwise infinite recursion at three.

While it is possible to break that, by doing so you break the
premise that we have a pure function.


Halts() is a function of its inputs.

Unfortunately "inputs" no longer refers to "those argument things
between the parentheses that we are painstakingly keeping the same".


I think that may be simply because you have a narrow minded view of
inputs as some fixed sized set of objects.

Oh, I specifically do not. Above, I'm demonstrating flexibility and
insight; I'm recognizing the new situation that there are more inputs
than just the arguments to those function parameters, and I'm
acknowleding that those are bona fide inputs.


Great !

However, the proofs that are used to demonstrate the nonexistence of a
universal halting aglorithms specify certain functions which have
certain inputs, and only those inputs, and are generally pure.

The dynamically generated execution trace of the simulation of H_Hat and its input are what Halts bases its halting decision on. That the conventiopal proof may have incorectly assumed static analysis is merely a false assumption on its part.

In your coding simulation of those functions, you cannot be adding
additional hidden inputs to the programming language functions
which are supposed to correspond to the proof's functions.


The only thing that I actually need to make a correct halting decision is the sequence of user specified x86 instructions that are simulated by the halt decider. A simulator would have access to this sequence.

You are ruling out all dynamically generated inputs.

Well, not me, personally, but the proofs.

The halting proofs use certain functions and they specify what exactly
those functions mean. You're changing what the functions mean, so your
code execution produces situations that don't pertain to the original
functions in the proof.


The halting proofs merely falsely assume static rather than dynamic analysis. That is their mistake not mine.


--
Copyright 2020 Pete Olcott

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



Subject: Re: Refuting the {Linz, Sipser, Kozen} HP Proofs (Ben's example)
From: Kaz Kylheku
Newsgroups: comp.theory, comp.ai.philosophy, comp.lang.asm.x86
Followup: comp.theory
Organization: Aioe.org NNTP Server
Date: Thu, 17 Dec 2020 16:06 UTC
References: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24
Path: i2pn2.org!i2pn.org!eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: 563-365-...@kylheku.com (Kaz Kylheku)
Newsgroups: comp.theory,comp.ai.philosophy,comp.lang.asm.x86
Subject: Re: Refuting the {Linz, Sipser, Kozen} HP Proofs (Ben's example)
Followup-To: comp.theory
Date: Thu, 17 Dec 2020 16:06:16 +0000 (UTC)
Organization: Aioe.org NNTP Server
Lines: 102
Approved: fbkotler@myfairpoint.net - comp.lang.asm.x86 moderation team.
Message-ID: <20201216213650.678@kylheku.com>
References: <3JSdnRrpiNHInV3CnZ2dnUU7-YHNnZ2d@giganews.com>
<yK2dnXzXs69GQkXCnZ2dnUU7-dvNnZ2d@giganews.com> <875z5262oy.fsf@bsb.me.uk>
<XKWdnc8Hn9oQzkTCnZ2dnUU7-RHNnZ2d@giganews.com> <877dpi4ksa.fsf@bsb.me.uk>
<S7WdnVxdtqB7-0TCnZ2dnUU7-TPNnZ2d@giganews.com>
<6b106784-3f6a-44c3-ad5b-646adba93fe6n@googlegroups.com>
<IoGdndKfvMgzw0fCnZ2dnUU7-WvNnZ2d@giganews.com>
<rrdomo$4ta$1@dont-email.me>
<If6dnUUqRMbH9UfCnZ2dnUU7-e_NnZ2d@giganews.com>
<rrdqe4$i7d$1@dont-email.me>
<kOydnRDlOZQZ6EfCnZ2dnUU7-XPNnZ2d@giganews.com>
<rrdtd6$a4j$1@dont-email.me>
<DaGdnXUvT8KlEUfCnZ2dnUU7-VXNnZ2d@giganews.com>
<rre588$gv5$1@dont-email.me>
<N8KdnVLL45clBkfCnZ2dnUU7-e3NnZ2d@giganews.com>
<20201216162234.114@kylheku.com>
<zaOdnU6LUeoIMUfCnZ2dnUU7-SXNnZ2d@giganews.com>
<20201216174857.611@kylheku.com>
<ttKdnaPKJbLzW0fCnZ2dnUU7-cnNnZ2d@giganews.com>
<20201216202107.24@kylheku.com>
<Xu6dncrJz_bhQ0fCnZ2dnUU7-e3NnZ2d@giganews.com>
<20201216204022.111@kylheku.com>
<0L2dnSYm4ejbdUfCnZ2dnUU7-YnNnZ2d@giganews.com>
Injection-Info: reader02.eternal-september.org; posting-host="4a23faa1200c6b29da9d0c80fbd9723f";
logging-data="21873"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1+zy8093pBQnVyH2Yji6UVwISkGdZKkV8s="
User-Agent: slrn/1.0.3 (Linux)
Cancel-Lock: sha1:RI6uj48VtSF9ecIJiyDmzBecHRg=
View all headers
["Followup-To:" header set to comp.theory.]
On 2020-12-17, olcott <NoOne@nospicedham.NoWhere.com> wrote:
On 12/16/2020 10:50 PM, Kaz Kylheku wrote:
On 2020-12-17, olcott <NoOne@NoWhere.com> wrote:
On 12/16/2020 10:24 PM, Kaz Kylheku wrote:
On 2020-12-17, olcott <NoOne@NoWhere.com> wrote:
On 12/16/2020 7:51 PM, Kaz Kylheku wrote:
If the progression is caused by an infinite recursion of a function
with the same paraemters, then all of the simulation levels are
indistinguishable. No UTM knows how many levels are above,
and each one has the same number of identical levels below.

That's it.


If we allowed the infinite recursion to infinitely recur this would be
true. We cut off the otherwise infinite recursion at three.

While it is possible to break that, by doing so you break the
premise that we have a pure function.


Halts() is a function of its inputs.

Unfortunately "inputs" no longer refers to "those argument things
between the parentheses that we are painstakingly keeping the same".


I think that may be simply because you have a narrow minded view of
inputs as some fixed sized set of objects.

Oh, I specifically do not. Above, I'm demonstrating flexibility and
insight; I'm recognizing the new situation that there are more inputs
than just the arguments to those function parameters, and I'm
acknowleding that those are bona fide inputs.


Great !

However, the proofs that are used to demonstrate the nonexistence of a
universal halting aglorithms specify certain functions which have
certain inputs, and only those inputs, and are generally pure.

The dynamically generated execution trace of the simulation of H_Hat and
its input are what Halts bases its halting decision on. That the
conventiopal proof may have incorectly assumed static analysis is merely
a false assumption on its part.

The conventional proofs have no such problem. They place absolutely no
restrictions on Halts other than that it have two arguments, return a
Boolean indication and be a function. Within these constraints, no
technique, be it "static" or "dynamic" is off the table.

The proofs show that no definition of Halts, under their constraints,
can be a universal halting decider. Because Halts is constrained in such
a way that it can be comprised of any Turing machine (there is an
equivalence between pure funcions and Turing machines), the proofs show
that no Turing machine can be a universal halting decider.

Your apparatus contains contains functions which meet a different,
informal definition of the word "function" denoting an imperative
procedure that returns a value, that may access (and even mutate) state
information not contained in its arguments.

Your claim is that your apparatus is an embodiment of the entities
described in the proof, and therefore properties of the apparatus speak
to the proof. This claim is false, and is to a large extent based
on equivocation over word semantics: changing between the definition of
"function" in mathematics jargon, and the definition of "function" in
the jargon of certain programming languages.

Equivocation is one of the most embarrassing errors of inference that
man can make: not pinning down the meanings of words.

The assumptions which a proof makes are its privilege, and they
contribute to its definition. If you have to change them in order to
challenge the proof, you're attacking a strawman caricature of the proof,
not the real one.

The halting proofs merely falsely assume static rather than dynamic
analysis. That is their mistake not mine.

No such words appear in any proof you can cite from any credible
textbook or paper. All proper presentations of the proof allow the
decider simply be an arbitrary recursive funtion, which allows it to be
any Turing machine.

(Quite literally, the decider function can encode the arguments P and I
onto a tape of symbols, and feed it to an actual Universal Turing Machine.)

The techniques you are using do not allow this; you could not translate
your simulation approach such that Halts encodes P and I onto a tape and
just launches a UTM, and then (if the UTM halts) collects the return
value from the tape.

Your approach would require the multiple invocations of that UTM to be
diddled by an interfering process into incorrectly producing different
results.

--
TXR Programming Language: http://nongnu.org/txr



1
rocksolid light 0.7.2
clearneti2ptor