Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]

Groups > comp.software-eng > #3531

Re: Halting problem proofs refuted on the basis of software engineering V2

Cross-posted to 4 groups.

Show all headers | View raw

On Mon, 4 Jul 2022 14:09:32 -0500
olcott <NoOne@NoWhere.com> wrote:

> On 7/4/2022 1:38 PM, Mr Flibble wrote:
> > On Mon, 4 Jul 2022 13:00:21 -0500
> > olcott <NoOne@NoWhere.com> wrote:
> >   
> >> On 7/4/2022 12:54 PM, Mr Flibble wrote:  
> >>> On Mon, 4 Jul 2022 12:51:24 -0500
> >>> olcott <NoOne@NoWhere.com> wrote:
> >>>      
> >>>> On 7/4/2022 12:39 PM, Mr Flibble wrote:  
> >>>>> On Mon, 4 Jul 2022 12:33:44 -0500
> >>>>> olcott <NoOne@NoWhere.com> wrote:
> >>>>>         
> >>>>>> On 7/4/2022 12:25 PM, Mr Flibble wrote:  
> >>>>>>> On Mon, 4 Jul 2022 11:54:55 -0500
> >>>>>>> olcott <NoOne@NoWhere.com> wrote:
> >>>>>>>            
> >>>>>>>> On 7/4/2022 10:58 AM, Mr Flibble wrote:  
> >>>>>>>>> On Mon, 4 Jul 2022 09:45:45 -0500
> >>>>>>>>> olcott <NoOne@NoWhere.com> wrote:
> >>>>>>>>>               
> >>>>>>>>>> No one can provide any "rebuttal" of my paper on any other
> >>>>>>>>>> basis than
> >>>>>>>>>>
> >>>>>>>>>> (1) disagreeing with the semantics of the x86 language
> >>>>>>>>>> *x86 Instruction Set Reference* https://c9x.me/x86/
> >>>>>>>>>>
> >>>>>>>>>> *or disagreeing with this necessarily true principle*
> >>>>>>>>>> (2) A halt decider must compute the mapping from its inputs
> >>>>>>>>>> to an accept or reject state on the basis of the actual
> >>>>>>>>>> behavior that is actually specified by these inputs.
> >>>>>>>>>>
> >>>>>>>>>>
> >>>>>>>>>>
> >>>>>>>>>> This much more concise version of my paper focuses on the
> >>>>>>>>>> actual execution of three fully operational examples.
> >>>>>>>>>>
> >>>>>>>>>> H0 correctly determines that Infinite_Loop() never halts
> >>>>>>>>>> H correctly determines that Infinite_Recursion() never
> >>>>>>>>>> halts H(P,P) correctly determines that its input never
> >>>>>>>>>> halts  
> >>>>>>>>>
> >>>>>>>>> As I have shown with my signaling halting decider there is
> >>>>>>>>> no need for a call to a simulation-based halting decider,
> >>>>>>>>> H, from the input program to be recursive; this is
> >>>>>>>>> compatible with [Strachey 1965] and associated proofs which
> >>>>>>>>> are not recursive in nature. Your H is invalid as it aborts
> >>>>>>>>> the simulation to prevent infinite recursion rather than
> >>>>>>>>> returning an answer to its caller which results in it
> >>>>>>>>> giving the wrong answer for a non-pathological input that
> >>>>>>>>> calls H.
> >>>>>>>>>
> >>>>>>>>> /Flibble
> >>>>>>>>>               
> >>>>>>>>
> >>>>>>>> YOU KEEP DISAGREEING WITH VERIFIED FACTS:
> >>>>>>>>      From a purely software engineering perspective
> >>>>>>>> (anchored in the semantics of the x86 language) it is proven
> >>>>>>>> that H(P,P) correctly predicts that its correct and complete
> >>>>>>>> x86 emulation of its input would never reach the "ret"
> >>>>>>>> instruction (final state) of this input.  
> >>>>>>>      
> >>>>>>> No it doesn't. What you have doesn't work.
> >>>>>>>
> >>>>>>> /Flibble
> >>>>>>>            
> >>>>>>
> >>>>>> Try and prove how foolish you are by attempting to refute the
> >>>>>> above statement on the basis is this paper:
> >>>>>>
> >>>>>> *Halting problem proofs refuted on the basis of software
> >>>>>> engineering*
> >>>>>> https://www.researchgate.net/publication/361701808_Halting_problem_proofs_refuted_on_the_basis_of_software_engineering
> >>>>>>        
> >>>>>     
> >>>>> I don't have to consider your "paper"; the evidence is here for
> >>>>> all to see:
> >>>>>
> >>>>> void Px(u32 x)
> >>>>> {
> >>>>>       H(x, x);
> >>>>>       return;
> >>>>> }
> >>>>>
> >>>>> int main()
> >>>>> {
> >>>>>       Output("Input_Halts = ", H((u32)Px, (u32)Px));
> >>>>> }
> >>>>>
> >>>>> ...[000013e8][00102357][00000000] 83c408          add esp,+08
> >>>>> ...[000013eb][00102353][00000000] 50              push eax
> >>>>> ...[000013ec][0010234f][00000427] 6827040000      push 00000427
> >>>>> ---[000013f1][0010234f][00000427] e880f0ffff      call 00000476
> >>>>> Input_Halts = 0
> >>>>> ...[000013f6][00102357][00000000] 83c408          add esp,+08
> >>>>> ...[000013f9][00102357][00000000] 33c0            xor eax,eax
> >>>>> ...[000013fb][0010235b][00100000] 5d              pop ebp
> >>>>> ...[000013fc][0010235f][00000004] c3              ret
> >>>>> Number of Instructions Executed(16120)
> >>>>>
> >>>>> As can be seen above Olcott's H decides that Px does not halt
> >>>>> but it is obvious that Px should always halt if H is a valid
> >>>>> halt decider that always returns a decision to its caller (Px).
> >>>>> Olcott's H does not return a decision to its caller (Px) and is
> >>>>> thus invalid.  
> >>>>
> >>>> Your trace always deceitfully leaves out key details.  
> >>>
> >>> My trace only includes the pertinent details: namely that it gets
> >>> the halting decision wrong:
> >>>      
> >>>>> Input_Halts = 0  
> >>>
> >>> /Flibble
> >>>      
> >>
> >> You continue under the false assumption that a function called in
> >> infinite recursion must return to its caller. That you continue in
> >> the false assumption after multiple corrections is a little nuts.  
> >   
> > There is no infinite recursion in [Strachey 1965] or associated
> > proofs  
> 
> Only because no one bothered to ever fully examine applying a
> simulating halt decider to the halting theorem counter-examples prior
> to:
> 
> comp.theory: [Solution to one instance of the Halting Problem]
> On 3/14/2017 9:05 AM, peteolcott wrote:
> 
> > and I have shown that there need not be any recursion when using a
> > simulation-based halting decider;   
> 
> You have not shown this. One is not free to diverge from the
> semantics specified by the C/x86 source-code. If infinite recursion
> is specified in this source-code then infinite recursion must occur
> in the execution trace until it is aborted.

I have shown this: see my recent post "An idea for a simulating halt
decider" in this forum.

> 
> > if you have to abort your simulation
> > to avoid infinite recursion then that just goes to show that your
> > solution is wrong.  
> 
> Actually it proves that my solution is correct. A simulating halt 
> decider must always abort its simulation of every non-halting input.

No, it proves your solution is incorrect.

/Flibble

Back to comp.software-eng | Previous | Next — Previous in thread | Next in thread | Find similar | Unroll thread

Thread

Halting problem proofs refuted on the basis of software engineering V2 olcott <NoOne@NoWhere.com> - 2022-07-04 09:45 -0500
  Re: Halting problem proofs refuted on the basis of software engineering V2 olcott <NoOne@NoWhere.com> - 2022-07-04 11:54 -0500
    Re: Halting problem proofs refuted on the basis of software engineering V2 Mr Flibble <flibble@reddwarf.jmc> - 2022-07-04 18:25 +0100
      Re: Halting problem proofs refuted on the basis of software engineering V2 olcott <NoOne@NoWhere.com> - 2022-07-04 12:33 -0500
        Re: Halting problem proofs refuted on the basis of software engineering V2 Mr Flibble <flibble@reddwarf.jmc> - 2022-07-04 18:39 +0100
          Re: Halting problem proofs refuted on the basis of software engineering V2 olcott <NoOne@NoWhere.com> - 2022-07-04 12:51 -0500
            Re: Halting problem proofs refuted on the basis of software engineering V2 Mr Flibble <flibble@reddwarf.jmc> - 2022-07-04 18:54 +0100
              Re: Halting problem proofs refuted on the basis of software engineering V2 olcott <NoOne@NoWhere.com> - 2022-07-04 13:00 -0500
                Re: Halting problem proofs refuted on the basis of software engineering V2 Mr Flibble <flibble@reddwarf.jmc> - 2022-07-04 19:38 +0100
                Re: Halting problem proofs refuted on the basis of software engineering V2 olcott <NoOne@NoWhere.com> - 2022-07-04 14:09 -0500
                Re: Halting problem proofs refuted on the basis of software engineering V2 Mr Flibble <flibble@reddwarf.jmc> - 2022-07-04 20:13 +0100
                Re: Halting problem proofs refuted on the basis of software engineering V2 Richard Damon <Richard@Damon-Family.org> - 2022-07-04 15:40 -0400

csiph-web