Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]
Groups > comp.software-eng > #3494 > unrolled thread
| Started by | olcott <NoOne@NoWhere.com> |
|---|---|
| First post | 2022-07-02 10:34 -0500 |
| Last post | 2022-07-17 13:06 -0400 |
| Articles | 20 on this page of 51 — 3 participants |
Back to article view | Back to comp.software-eng
Halting problem proofs refuted on the basis of software engineering olcott <NoOne@NoWhere.com> - 2022-07-02 10:34 -0500
Re: Halting problem proofs refuted on the basis of software engineering Mr Flibble <flibble@reddwarf.jmc> - 2022-07-02 17:26 +0100
Re: Halting problem proofs refuted on the basis of software engineering olcott <NoOne@NoWhere.com> - 2022-07-02 11:42 -0500
Re: Halting problem proofs refuted on the basis of software engineering olcott <NoOne@NoWhere.com> - 2022-07-02 12:15 -0500
Re: Halting problem proofs refuted on the basis of software engineering Mr Flibble <flibble@reddwarf.jmc> - 2022-07-02 18:26 +0100
Re: Halting problem proofs refuted on the basis of software engineering olcott <NoOne@NoWhere.com> - 2022-07-02 12:30 -0500
Re: Halting problem proofs refuted on the basis of software engineering Mr Flibble <flibble@reddwarf.jmc> - 2022-07-02 19:28 +0100
Re: Halting problem proofs refuted on the basis of software engineering olcott <NoOne@NoWhere.com> - 2022-07-02 13:41 -0500
Re: Halting problem proofs refuted on the basis of software engineering Mr Flibble <flibble@reddwarf.jmc> - 2022-07-02 19:44 +0100
Re: Halting problem proofs refuted on the basis of software engineering olcott <NoOne@NoWhere.com> - 2022-07-02 16:26 -0500
Re: Halting problem proofs refuted on the basis of software engineering Mr Flibble <flibble@reddwarf.jmc> - 2022-07-02 23:05 +0100
Re: Halting problem proofs refuted on the basis of software engineering olcott <NoOne@NoWhere.com> - 2022-07-02 17:13 -0500
Re: Halting problem proofs refuted on the basis of software engineering Mr Flibble <flibble@reddwarf.jmc> - 2022-07-03 15:27 +0100
Re: Halting problem proofs refuted on the basis of software engineering olcott <NoOne@NoWhere.com> - 2022-07-03 09:57 -0500
Re: Halting problem proofs refuted on the basis of software engineering Mr Flibble <flibble@reddwarf.jmc> - 2022-07-03 16:21 +0100
Re: Halting problem proofs refuted on the basis of software engineering olcott <NoOne@NoWhere.com> - 2022-07-03 10:30 -0500
Re: Halting problem proofs refuted on the basis of software engineering Mr Flibble <flibble@reddwarf.jmc> - 2022-07-03 16:45 +0100
Re: Halting problem proofs refuted on the basis of software engineering olcott <NoOne@NoWhere.com> - 2022-07-03 10:48 -0500
Re: Halting problem proofs refuted on the basis of software engineering Mr Flibble <flibble@reddwarf.jmc> - 2022-07-03 16:51 +0100
Re: Halting problem proofs refuted on the basis of software engineering olcott <NoOne@NoWhere.com> - 2022-07-03 11:05 -0500
Re: Halting problem proofs refuted on the basis of software engineering Mr Flibble <flibble@reddwarf.jmc> - 2022-07-03 17:07 +0100
Re: Halting problem proofs refuted on the basis of software engineering olcott <NoOne@NoWhere.com> - 2022-07-04 11:57 -0500
Re: Halting problem proofs refuted on the basis of software engineering olcott <NoOne@NoWhere.com> - 2022-07-04 14:17 -0500
Re: Halting problem proofs refuted on the basis of software engineering olcott <NoOne@NoWhere.com> - 2022-07-04 14:21 -0500
Re: Halting problem proofs refuted on the basis of software engineering [ Curry–Howard correspondence ] olcott <NoOne@NoWhere.com> - 2022-07-04 18:08 -0500
Re: Halting problem proofs refuted on the basis of software engineering [ Curry–Howard correspondence ] olcott <NoOne@NoWhere.com> - 2022-07-05 14:31 -0500
Re: Halting problem proofs refuted on the basis of software engineering [ Curry–Howard correspondence ] olcott <NoOne@NoWhere.com> - 2022-07-05 15:42 -0500
Re: Halting problem proofs refuted on the basis of software engineering [ Curry–Howard correspondence ] Richard Damon <Richard@Damon-Family.org> - 2022-07-05 19:29 -0400
Re: Halting problem proofs refuted on the basis of software engineering [ Curry–Howard correspondence ] olcott <NoOne@NoWhere.com> - 2022-07-05 19:01 -0500
Re: Halting problem proofs refuted on the basis of software engineering [ Curry–Howard correspondence ] olcott <NoOne@NoWhere.com> - 2022-07-06 16:13 -0500
Re: Halting problem proofs refuted on the basis of software engineering [ Curry–Howard correspondence ] olcott <NoOne@NoWhere.com> - 2022-07-07 16:08 -0500
Re: Halting problem proofs refuted on the basis of software engineering [ Curry–Howard correspondence ] olcott <NoOne@NoWhere.com> - 2022-07-07 20:34 -0500
Re: Halting problem proofs refuted on the basis of software engineering [ Curry–Howard correspondence ] olcott <NoOne@NoWhere.com> - 2022-07-07 23:48 -0500
Re: Halting problem proofs refuted on the basis of software engineering [ Irrefutably Correct ] olcott <NoOne@NoWhere.com> - 2022-07-09 13:40 -0500
Re: Halting problem proofs refuted on the basis of software engineering [ Irrefutably Correct ] Richard Damon <Richard@Damon-Family.org> - 2022-07-09 15:06 -0400
Re: Halting problem proofs refuted on the basis of software engineering [ Curry–Howard correspondence ] olcott <NoOne@NoWhere.com> - 2022-07-05 19:50 -0500
Re: Halting problem proofs refuted on the basis of software engineering [ Curry–Howard correspondence ] olcott <NoOne@NoWhere.com> - 2022-07-05 21:37 -0500
Re: Halting problem proofs refuted on the basis of software engineering olcott <NoOne@NoWhere.com> - 2022-07-05 07:59 -0500
Re: Halting problem proofs refuted on the basis of software engineering olcott <NoOne@NoWhere.com> - 2022-07-05 08:00 -0500
Re: Halting problem proofs refuted on the basis of software engineering Richard Damon <Richard@Damon-Family.org> - 2022-07-05 19:31 -0400
Re: Halting problem proofs refuted on the basis of software engineering olcott <NoOne@NoWhere.com> - 2022-07-13 14:37 -0500
Re: Halting problem proofs refuted on the basis of software engineering olcott <NoOne@NoWhere.com> - 2022-07-13 15:51 -0500
Re: Halting problem proofs refuted on the basis of software engineering olcott <NoOne@NoWhere.com> - 2022-07-13 19:10 -0500
Re: Halting problem proofs refuted on the basis of software engineering Richard Damon <Richard@Damon-Family.org> - 2022-07-13 21:29 -0400
Re: Halting problem proofs refuted on the basis of software engineering Richard Damon <Richard@Damon-Family.org> - 2022-07-13 19:29 -0400
Re: Halting problem proofs refuted on the basis of software engineering olcott <NoOne@NoWhere.com> - 2022-07-15 11:26 -0500
Re: Halting problem proofs refuted on the basis of software engineering olcott <NoOne@NoWhere.com> - 2022-07-16 19:18 -0500
Re: Halting problem proofs refuted on the basis of software engineering Richard Damon <Richard@Damon-Family.org> - 2022-07-16 20:38 -0400
Re: Halting problem proofs refuted on the basis of software engineering olcott <NoOne@NoWhere.com> - 2022-07-16 20:19 -0500
Re: Halting problem proofs refuted on the basis of software engineering [thanks Mike] olcott <NoOne@NoWhere.com> - 2022-07-17 12:00 -0500
Re: Halting problem proofs refuted on the basis of software engineering [thanks Mike] Richard Damon <Richard@Damon-Family.org> - 2022-07-17 13:06 -0400
Page 2 of 3 — ← Prev page 1 [2] 3 Next page →
| From | Mr Flibble <flibble@reddwarf.jmc> |
|---|---|
| Date | 2022-07-03 17:07 +0100 |
| Message-ID | <20220703170707.00006ec9@reddwarf.jmc> |
| In reply to | #3513 |
On Sun, 3 Jul 2022 11:05:21 -0500
olcott <NoOne@NoWhere.com> wrote:
> On 7/3/2022 10:51 AM, Mr Flibble wrote:
> > On Sun, 3 Jul 2022 10:48:18 -0500
> > olcott <NoOne@NoWhere.com> wrote:
> >
> >> On 7/3/2022 10:45 AM, Mr Flibble wrote:
> >>> On Sun, 3 Jul 2022 10:30:45 -0500
> >>> olcott <NoOne@NoWhere.com> wrote:
> >>>
> >>>> On 7/3/2022 10:21 AM, Mr Flibble wrote:
> >>>>> On Sun, 3 Jul 2022 09:57:57 -0500
> >>>>> olcott <NoOne@NoWhere.com> wrote:
> >>>>>
> >>>>>> On 7/3/2022 9:27 AM, Mr Flibble wrote:
> >>>>>>> On Sat, 2 Jul 2022 17:13:01 -0500
> >>>>>>> olcott <NoOne@NoWhere.com> wrote:
> >>>>>>>
> >>>>>>>> On 7/2/2022 5:05 PM, Mr Flibble wrote:
> >>>>>>>>> On Sat, 2 Jul 2022 16:26:45 -0500
> >>>>>>>>> olcott <NoOne@NoWhere.com> wrote:
> >>>>>>>>>
> >>>>>>>>>> On 7/2/2022 1:44 PM, Mr Flibble wrote:
> >>>>>>>>>>> On Sat, 2 Jul 2022 13:41:14 -0500
> >>>>>>>>>>> olcott <NoOne@NoWhere.com> wrote:
> >>>>>>>>>>>
> >>>>>>>>>>>> On 7/2/2022 1:28 PM, Mr Flibble wrote:
> >>>>>>>>>>>>> On Sat, 2 Jul 2022 12:30:03 -0500
> >>>>>>>>>>>>> olcott <NoOne@NoWhere.com> wrote:
> >>>>>>>>>>>>>
> >>>>>>>>>>>>>> On 7/2/2022 12:26 PM, Mr Flibble wrote:
> >>>>>>>>>>>>>>> On Sat, 2 Jul 2022 12:15:58 -0500
> >>>>>>>>>>>>>>> olcott <NoOne@NoWhere.com> wrote:
> >>>>>>>>>>>>>>>
> >>>>>>>>>>>>>>>> On 7/2/2022 12:10 PM, Mr Flibble wrote:
> >>>>>>>>>>>>>>>>> On Sat, 2 Jul 2022 11:42:48 -0500
> >>>>>>>>>>>>>>>>> olcott <NoOne@NoWhere.com> wrote:
> >>>>>>>>>>>>>>>>>
> >>>>>>>>>>>>>>>>>> On 7/2/2022 11:26 AM, Mr Flibble wrote:
> >>>>>>>>>>>>>>>>>>> On Sat, 2 Jul 2022 10:34:34 -0500
> >>>>>>>>>>>>>>>>>>> olcott <NoOne@NoWhere.com> wrote:
> >>>>>>>>>>>>>>>>>>>
> >>>>>>>>>>>>>>>>>>>> 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 correctly
> >>>>>>>>>>>>>>>>>>>> determines that P() never halts
> >>>>>>>>>>>>>>>>>>>>
> >>>>>>>>>>>>>>>>>>>> void P(u32 x)
> >>>>>>>>>>>>>>>>>>>> {
> >>>>>>>>>>>>>>>>>>>> if (H(x, x))
> >>>>>>>>>>>>>>>>>>>> HERE: goto HERE;
> >>>>>>>>>>>>>>>>>>>> return;
> >>>>>>>>>>>>>>>>>>>> }
> >>>>>>>>>>>>>>>>>>>>
> >>>>>>>>>>>>>>>>>>>> int main()
> >>>>>>>>>>>>>>>>>>>> {
> >>>>>>>>>>>>>>>>>>>> Output("Input_Halts = ", H((u32)P,
> >>>>>>>>>>>>>>>>>>>> (u32)P)); }
> >>>>>>>>>>>>>>>>>>>>
> >>>>>>>>>>>>>>>>>>>> As shown below the above P and H have the
> >>>>>>>>>>>>>>>>>>>> required (halting problem) pathological
> >>>>>>>>>>>>>>>>>>>> relationship to each other:
> >>>>>>>>>>>>>>>>>>>>
> >>>>>>>>>>>>>>>>>>>> For any program H that might
> >>>>>>>>>>>>>>>>>>>> determine if programs halt, a "pathological"
> >>>>>>>>>>>>>>>>>>>> program P, called with some
> >>>>>>>>>>>>>>>>>>>> input, can pass its own source and its input to
> >>>>>>>>>>>>>>>>>>>> H and then specifically do the
> >>>>>>>>>>>>>>>>>>>> opposite of what H predicts P will do. No H
> >>>>>>>>>>>>>>>>>>>> can exist that handles this case.
> >>>>>>>>>>>>>>>>>>>> https://en.wikipedia.org/wiki/Halting_problem
> >>>>>>>>>>>>>>>>>>>>
> >>>>>>>>>>>>>>>>>>>> I really need software engineers to verify that H
> >>>>>>>>>>>>>>>>>>>> does correctly predict that its complete and
> >>>>>>>>>>>>>>>>>>>> correct x86 emulation of its input would never
> >>>>>>>>>>>>>>>>>>>> reach the "ret" instruction of this input.
> >>>>>>>>>>>>>>>>>>>>
> >>>>>>>>>>>>>>>>>>>> *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
> >>>>>>>>>>>>>>>>>>>>
> >>>>>>>>>>>>>>>>>>>
> >>>>>>>>>>>>>>>>>>> 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.
> >>>>>>>>>>>>>>>>>>>
> >>>>>>>>>>>>>>>>>>> /Flibble
> >>>>>>>>>>>>>>>>>>>
> >>>>>>>>>>>>>>>>>>
> >>>>>>>>>>>>>>>>>> Your false assumptions are directly contradicted by
> >>>>>>>>>>>>>>>>>> the semantics of the x86 programming language.
> >>>>>>>>>>>>>>>>>>
> >>>>>>>>>>>>>>>>>> *x86 Instruction Set Reference*
> >>>>>>>>>>>>>>>>>> https://c9x.me/x86/
> >>>>>>>>>>>>>>>>>>
> >>>>>>>>>>>>>>>>>> void Px(u32 x)
> >>>>>>>>>>>>>>>>>> {
> >>>>>>>>>>>>>>>>>> H(x, x);
> >>>>>>>>>>>>>>>>>> return;
> >>>>>>>>>>>>>>>>>> }
> >>>>>>>>>>>>>>>>>>
> >>>>>>>>>>>>>>>>>> int main()
> >>>>>>>>>>>>>>>>>> {
> >>>>>>>>>>>>>>>>>> Output("Input_Halts = ", H((u32)Px,
> >>>>>>>>>>>>>>>>>> (u32)Px)); }
> >>>>>>>>>>>>>>>>>>
> >>>>>>>>>>>>>>>>>> _Px()
> >>>>>>>>>>>>>>>>>> [00001192](01) 55 push ebp
> >>>>>>>>>>>>>>>>>> [00001193](02) 8bec mov ebp,esp
> >>>>>>>>>>>>>>>>>> [00001195](03) 8b4508 mov eax,[ebp+08]
> >>>>>>>>>>>>>>>>>> [00001198](01) 50 push eax
> >>>>>>>>>>>>>>>>>> [00001199](03) 8b4d08 mov ecx,[ebp+08]
> >>>>>>>>>>>>>>>>>> [0000119c](01) 51 push ecx
> >>>>>>>>>>>>>>>>>> [0000119d](05) e8d0fdffff call 00000f72
> >>>>>>>>>>>>>>>>>> [000011a2](03) 83c408 add esp,+08
> >>>>>>>>>>>>>>>>>> [000011a5](01) 5d pop ebp
> >>>>>>>>>>>>>>>>>> [000011a6](01) c3 ret
> >>>>>>>>>>>>>>>>>> Size in bytes:(0021) [000011a6]
> >>>>>>>>>>>>>>>>>>
> >>>>>>>>>>>>>>>>>> _main()
> >>>>>>>>>>>>>>>>>> [000011d2](01) 55 push ebp
> >>>>>>>>>>>>>>>>>> [000011d3](02) 8bec mov ebp,esp
> >>>>>>>>>>>>>>>>>> [000011d5](05) 6892110000 push 00001192
> >>>>>>>>>>>>>>>>>> [000011da](05) 6892110000 push 00001192
> >>>>>>>>>>>>>>>>>> [000011df](05) e88efdffff call 00000f72
> >>>>>>>>>>>>>>>>>> [000011e4](03) 83c408 add esp,+08
> >>>>>>>>>>>>>>>>>> [000011e7](01) 50 push eax
> >>>>>>>>>>>>>>>>>> [000011e8](05) 68a3040000 push 000004a3
> >>>>>>>>>>>>>>>>>> [000011ed](05) e800f3ffff call 000004f2
> >>>>>>>>>>>>>>>>>> [000011f2](03) 83c408 add esp,+08
> >>>>>>>>>>>>>>>>>> [000011f5](02) 33c0 xor eax,eax
> >>>>>>>>>>>>>>>>>> [000011f7](01) 5d pop ebp
> >>>>>>>>>>>>>>>>>> [000011f8](01) c3 ret
> >>>>>>>>>>>>>>>>>> Size in bytes:(0039) [000011f8]
> >>>>>>>>>>>>>>>>>>
> >>>>>>>>>>>>>>>>>> machine stack stack machine
> >>>>>>>>>>>>>>>>>> assembly address address data code
> >>>>>>>>>>>>>>>>>> language ======== ======== ======== =========
> >>>>>>>>>>>>>>>>>> ============= [000011d2][00101f7f][00000000] 55
> >>>>>>>>>>>>>>>>>> push ebp [000011d3][00101f7f][00000000] 8bec
> >>>>>>>>>>>>>>>>>> mov ebp,esp [000011d5][00101f7b][00001192]
> >>>>>>>>>>>>>>>>>> 6892110000 push 00001192
> >>>>>>>>>>>>>>>>>> [000011da][00101f77][00001192] 6892110000 push
> >>>>>>>>>>>>>>>>>> 00001192 [000011df][00101f73][000011e4] e88efdffff
> >>>>>>>>>>>>>>>>>> call 00000f72
> >>>>>>>>>>>>>>>>>>
> >>>>>>>>>>>>>>>>>> H: Begin Simulation Execution Trace Stored
> >>>>>>>>>>>>>>>>>> at:11202b Address_of_H:f72
> >>>>>>>>>>>>>>>>>> [00001192][00112017][0011201b] 55 push ebp
> >>>>>>>>>>>>>>>>>> [00001193][00112017][0011201b] 8bec mov
> >>>>>>>>>>>>>>>>>> ebp,esp [00001195][00112017][0011201b] 8b4508
> >>>>>>>>>>>>>>>>>> mov eax,[ebp+08] [00001198][00112013][00001192] 50
> >>>>>>>>>>>>>>>>>> push eax // push Px
> >>>>>>>>>>>>>>>>>> [00001199][00112013][00001192] 8b4d08 mov
> >>>>>>>>>>>>>>>>>> ecx,[ebp+08] [0000119c][0011200f][00001192] 51
> >>>>>>>>>>>>>>>>>> push ecx // push Px
> >>>>>>>>>>>>>>>>>> [0000119d][0011200b][000011a2] e8d0fdffff call
> >>>>>>>>>>>>>>>>>> 00000f72 // call H(Px,Px) H: Infinitely Recursive
> >>>>>>>>>>>>>>>>>> Simulation Detected Simulation Stopped
> >>>>>>>>>>>>>>>>>>
> >>>>>>>>>>>>>>>>>> H knows its own machine address and on this basis
> >>>>>>>>>>>>>>>>>> it can easily examine its stored execution_trace
> >>>>>>>>>>>>>>>>>> of Px (see above) to determine: (a) Px is calling
> >>>>>>>>>>>>>>>>>> H with the same arguments that H was called with.
> >>>>>>>>>>>>>>>>>> (b) No instructions in Px could possibly escape
> >>>>>>>>>>>>>>>>>> this otherwise infinitely recursive emulation. (c)
> >>>>>>>>>>>>>>>>>> H aborts its emulation of Px before its call to H
> >>>>>>>>>>>>>>>>>> is emulated.
> >>>>>>>>>>>>>>>>>>
> >>>>>>>>>>>>>>>>>> [000011e4][00101f7f][00000000] 83c408 add
> >>>>>>>>>>>>>>>>>> esp,+08 [000011e7][00101f7b][00000000] 50
> >>>>>>>>>>>>>>>>>> push eax [000011e8][00101f77][000004a3] 68a3040000
> >>>>>>>>>>>>>>>>>> push 000004a3 [000011ed][00101f77][000004a3]
> >>>>>>>>>>>>>>>>>> e800f3ffff call 000004f2 Input_Halts = 0
> >>>>>>>>>>>>>>>>>> [000011f2][00101f7f][00000000] 83c408 add
> >>>>>>>>>>>>>>>>>> esp,+08 [000011f5][00101f7f][00000000] 33c0
> >>>>>>>>>>>>>>>>>> xor eax,eax [000011f7][00101f83][00000018] 5d
> >>>>>>>>>>>>>>>>>> pop ebp [000011f8][00101f87][00000000] c3
> >>>>>>>>>>>>>>>>>> ret Number of Instructions Executed(880) == 13
> >>>>>>>>>>>>>>>>>> Pages
> >>>>>>>>>>>>>>>>>
> >>>>>>>>>>>>>>>>> If H wasn't a simulation-based halting decider then
> >>>>>>>>>>>>>>>>> Px() would always halt; the infinite recursion is a
> >>>>>>>>>>>>>>>>> manifestation of your invalid simulation-based
> >>>>>>>>>>>>>>>>> halting decider. There is no recursion in
> >>>>>>>>>>>>>>>>> [Strachey 1965].
> >>>>>>>>>>>>>>>>>
> >>>>>>>>>>>>>>>>> /Flibble
> >>>>>>>>>>>>>>>>
> >>>>>>>>>>>>>>>> In other words you are rejecting the concept of a
> >>>>>>>>>>>>>>>> simulating halt decider even though I conclusively
> >>>>>>>>>>>>>>>> proved that it does correctly determine the halt
> >>>>>>>>>>>>>>>> status of: (see my new paper)
> >>>>>>>>>>>>>>>
> >>>>>>>>>>>>>>> No I am rejecting your simulating halt decider as it
> >>>>>>>>>>>>>>> gets the answer wrong for Px() which is not a
> >>>>>>>>>>>>>>> pathological input. Px() halts.
> >>>>>>>>>>>>>>>
> >>>>>>>>>>>>>>> /Flibble
> >>>>>>>>>>>>>>>
> >>>>>>>>>>>>>>
> >>>>>>>>>>>>>> I just proved that H(Px,Px) does correctly predict that
> >>>>>>>>>>>>>> its complete and correct x86 emulation of its input
> >>>>>>>>>>>>>> would never reach the "ret" instruction of this input
> >>>>>>>>>>>>>> because of the pathological relationship between H and
> >>>>>>>>>>>>>> Px.
> >>>>>>>>>>>>>
> >>>>>>>>>>>>> Wrong. Px() is not a pathological input as defined by
> >>>>>>>>>>>>> the halting problem and [Strachey 1965] as it does not
> >>>>>>>>>>>>> try to do the opposite of what H decides.
> >>>>>>>>>>>>>
> >>>>>>>>>>>>> /Flibble
> >>>>>>>>>>>>>
> >>>>>>>>>>>>
> >>>>>>>>>>>> Your lack of comprehension does not actually count as any
> >>>>>>>>>>>> rebuttal at all.
> >>>>>>>>>>>>
> >>>>>>>>>>>> void P(u32 x)
> >>>>>>>>>>>> {
> >>>>>>>>>>>> if (H(x, x))
> >>>>>>>>>>>> HERE: goto HERE;
> >>>>>>>>>>>> return;
> >>>>>>>>>>>> }
> >>>>>>>>>>>>
> >>>>>>>>>>>> int main()
> >>>>>>>>>>>> {
> >>>>>>>>>>>> Output("Input_Halts = ", H((u32)P, (u32)P));
> >>>>>>>>>>>> }
> >>>>>>>>>>>>
> >>>>>>>>>>>> As shown below the above P and H have the required
> >>>>>>>>>>>> (halting problem) pathological relationship to each
> >>>>>>>>>>>> other:
> >>>>>>>>>>> [snip]
> >>>>>>>>>>>
> >>>>>>>>>>> P does but Px does not. I am talking about Px not P.
> >>>>>>>>>>>
> >>>>>>>>>>> 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.
> >>>>>>>>>>>
> >>>>>>>>>>> /Flibble
> >>>>>>>>>>>
> >>>>>>>>>>
> >>>>>>>>>> >
> >>>>>>>>>>
> >>>>>>>>>> Your false assumptions are directly contradicted by the
> >>>>>>>>>> semantics of the x86 programming language.
> >>>>>>>>>>
> >>>>>>>>>> *x86 Instruction Set Reference* https://c9x.me/x86/
> >>>>>>>>>>
> >>>>>>>>>> void Px(u32 x)
> >>>>>>>>>> {
> >>>>>>>>>> H(x, x);
> >>>>>>>>>> return;
> >>>>>>>>>> }
> >>>>>>>>>>
> >>>>>>>>>> int main()
> >>>>>>>>>> {
> >>>>>>>>>> Output("Input_Halts = ", H((u32)Px, (u32)Px));
> >>>>>>>>>> }
> >>>>>>>>>>
> >>>>>>>>>> _Px()
> >>>>>>>>>> [00001192](01) 55 push ebp
> >>>>>>>>>> [00001193](02) 8bec mov ebp,esp
> >>>>>>>>>> [00001195](03) 8b4508 mov eax,[ebp+08]
> >>>>>>>>>> [00001198](01) 50 push eax
> >>>>>>>>>> [00001199](03) 8b4d08 mov ecx,[ebp+08]
> >>>>>>>>>> [0000119c](01) 51 push ecx
> >>>>>>>>>> [0000119d](05) e8d0fdffff call 00000f72
> >>>>>>>>>> [000011a2](03) 83c408 add esp,+08
> >>>>>>>>>> [000011a5](01) 5d pop ebp
> >>>>>>>>>> [000011a6](01) c3 ret
> >>>>>>>>>> Size in bytes:(0021) [000011a6]
> >>>>>>>>>>
> >>>>>>>>>> _main()
> >>>>>>>>>> [000011d2](01) 55 push ebp
> >>>>>>>>>> [000011d3](02) 8bec mov ebp,esp
> >>>>>>>>>> [000011d5](05) 6892110000 push 00001192
> >>>>>>>>>> [000011da](05) 6892110000 push 00001192
> >>>>>>>>>> [000011df](05) e88efdffff call 00000f72
> >>>>>>>>>> [000011e4](03) 83c408 add esp,+08
> >>>>>>>>>> [000011e7](01) 50 push eax
> >>>>>>>>>> [000011e8](05) 68a3040000 push 000004a3
> >>>>>>>>>> [000011ed](05) e800f3ffff call 000004f2
> >>>>>>>>>> [000011f2](03) 83c408 add esp,+08
> >>>>>>>>>> [000011f5](02) 33c0 xor eax,eax
> >>>>>>>>>> [000011f7](01) 5d pop ebp
> >>>>>>>>>> [000011f8](01) c3 ret
> >>>>>>>>>> Size in bytes:(0039) [000011f8]
> >>>>>>>>>>
> >>>>>>>>>> machine stack stack machine assembly
> >>>>>>>>>> address address data code language
> >>>>>>>>>> ======== ======== ======== =========
> >>>>>>>>>> ============= [000011d2][00101f7f][00000000] 55
> >>>>>>>>>> push ebp [000011d3][00101f7f][00000000] 8bec mov
> >>>>>>>>>> ebp,esp [000011d5][00101f7b][00001192] 6892110000 push
> >>>>>>>>>> 00001192 [000011da][00101f77][00001192] 6892110000 push
> >>>>>>>>>> 00001192 [000011df][00101f73][000011e4] e88efdffff call
> >>>>>>>>>> 00000f72
> >>>>>>>>>>
> >>>>>>>>>> H: Begin Simulation Execution Trace Stored at:11202b
> >>>>>>>>>> Address_of_H:f72
> >>>>>>>>>> [00001192][00112017][0011201b] 55 push ebp
> >>>>>>>>>> [00001193][00112017][0011201b] 8bec mov ebp,esp
> >>>>>>>>>> [00001195][00112017][0011201b] 8b4508 mov eax,[ebp+08]
> >>>>>>>>>> [00001198][00112013][00001192] 50 push eax //
> >>>>>>>>>> push Px [00001199][00112013][00001192] 8b4d08 mov
> >>>>>>>>>> ecx,[ebp+08] [0000119c][0011200f][00001192] 51 push
> >>>>>>>>>> ecx // push Px [0000119d][0011200b][000011a2]
> >>>>>>>>>> e8d0fdffff call 00000f72 // call H(Px,Px) H: Infinitely
> >>>>>>>>>> Recursive Simulation Detected Simulation Stopped
> >>>>>>>>>>
> >>>>>>>>>> H knows its own machine address and on this basis it can
> >>>>>>>>>> easily examine its stored execution_trace of Px (see above)
> >>>>>>>>>> to determine: (a) Px is calling H with the same arguments
> >>>>>>>>>> that H was called with. (b) No instructions in Px could
> >>>>>>>>>> possibly escape this otherwise infinitely recursive
> >>>>>>>>>> emulation. (c) H aborts its emulation of Px before its call
> >>>>>>>>>> to H is emulated.
> >>>>>>>>>>
> >>>>>>>>>> [000011e4][00101f7f][00000000] 83c408 add esp,+08
> >>>>>>>>>> [000011e7][00101f7b][00000000] 50 push eax
> >>>>>>>>>> [000011e8][00101f77][000004a3] 68a3040000 push 000004a3
> >>>>>>>>>> [000011ed][00101f77][000004a3] e800f3ffff call 000004f2
> >>>>>>>>>> Input_Halts = 0
> >>>>>>>>>> [000011f2][00101f7f][00000000] 83c408 add esp,+08
> >>>>>>>>>> [000011f5][00101f7f][00000000] 33c0 xor eax,eax
> >>>>>>>>>> [000011f7][00101f83][00000018] 5d pop ebp
> >>>>>>>>>> [000011f8][00101f87][00000000] c3 ret
> >>>>>>>>>> Number of Instructions Executed(880) == 13 Pages
> >>>>>>>>>
> >>>>>>>>> I see you wish to pointlessly go around in circles. Oh well.
> >>>>>>>>>
> >>>>>>>>> Px() is not a pathological input as defined by the halting
> >>>>>>>>> problem and [Strachey 1965] as it does not try to do the
> >>>>>>>>> opposite of what H decides.
> >>>>>>>>>
> >>>>>>>>> Px() always halts so your H gets the answer wrong.
> >>>>>>>>>
> >>>>>>>>> /Flibble
> >>>>>>>>
> >>>>>>>> I found that my reply did not make it to all the groups so I
> >>>>>>>> posted it again.
> >>>>>>>>
> >>>>>>>> *This general principle refutes conventional halting problem
> >>>>>>>> proofs* Every simulating halt decider that correctly
> >>>>>>>> simulates its input until it correctly predicts that this
> >>>>>>>> simulated input would never reach its final state, correctly
> >>>>>>>> rejects this input as non-halting.
> >>>>>>>
> >>>>>>> Your H does not "correctly predict" that Px() does reach its
> >>>>>>> final state and so should accept the input as halting.
> >>>>>>>
> >>>>>>> /Flibble
> >>>>>>>
> >>>>>>
> >>>>>> (x86 Instruction Set Reference* https://c9x.me/x86/
> >>>>>>
> >>>>>> The semantics of the x86 language conclusively proves that the
> >>>>>> above code is correct. People that disagree with verified facts
> >>>>>> are either incompetent or liars. Since you cannot even
> >>>>>> understand that the return statement in Px is unreachable
> >>>>>> code, (to every simulating halt decider H) you would be
> >>>>>> incompetent.
> >>>>>
> >>>>> Not EVERY simulating halt decider, only YOURS gets the answer
> >>>>> wrong. Px() halts.
> >>>>>
> >>>>> /Flibble
> >>>>>
> >>>>
> >>>> Since you cannot even understand that the return statement in Px
> >>>> is unreachable code, (to *every simulating halt* decider H) you
> >>>> would be incompetent.
> >>>
> >>> Not at all. If I was to design a simulating halt decider then
> >>> rather than aborting the simulation at the point where P()/Px()
> >>> calls H I would instead fork the simulation, returning 0 to one
> >>> branch (the non-halting branch) and 1 to the other branch (the
> >>> halting branch) and then continue to simulate both branches in
> >>> parallel thereby getting rid of the "infinite recursion".
> >>>
> >>> /Flibble
> >>>
> >>
> >> Yet that is *not* what the actual code specifies. Every function
> >> called in infinite recursion is not allowed to return to its
> >> caller.
> >
> > The infinite recursion is an artifact of how YOU are trying to solve
> > the problem; there is no infinite recursion in [Strachey 1965] and
> > associated proofs.
> >
> > /Flibble
> >
>
> The halting problem expressly allows every algorithm in the universe
> as long as it correctly predicts the behavior of the input.
Your H does not correctly predict the behavior of Px() as Px() always
halts yet your H incorrectly says it doesn't.
/Flibble
[toc] | [prev] | [next] | [standalone]
| From | olcott <NoOne@NoWhere.com> |
|---|---|
| Date | 2022-07-04 11:57 -0500 |
| Message-ID | <JZGdnTDV77xthl7_nZ2dnUU7_8xh4p2d@giganews.com> |
| In reply to | #3513 |
On 7/4/2022 11:36 AM, dklei...@gmail.com wrote: > On Sunday, July 3, 2022 at 5:44:32 PM UTC-7, olcott wrote: >> On 7/3/2022 6:10 PM, dklei...@gmail.com wrote: >>> On Sunday, July 3, 2022 at 12:51:41 PM UTC-7, olcott wrote: >>>> On 7/3/2022 2:35 PM, dklei...@gmail.com wrote: >>>>> On Sunday, July 3, 2022 at 9:05:30 AM UTC-7, olcott wrote: >>>>>> >>>>>> *This general principle refutes conventional halting problem proofs* >>>>>> >>>>>> Every simulating halt decider that correctly simulates its input until >>>>>> it correctly predicts that this simulated input would never reach its >>>>>> final state, correctly rejects this input as non-halting. >>>>>> >>>>> This "general principle is" a trivial definition: A simulation of a >>>>> called routine that stops when it can predict that the routine >>>>> will never return is called a halt decider. >>>>> >>>>> In words of one syllable - so what? >>>> >>>> It refutes conventional halting problem proofs >>>> >>> It might if any such halt deciders existed. You need to prove such "halt >>> deciders" exist. >> >> You can't keep ignoring my paper and claiming that I have not proved my >> point. >> *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 >> > Your paper is not acceptable as a proof of anything. But that is to > be expected because my standard is mathematical proof and > you don't even pretend to be doing mathematics. When we construe the x86 language and its associated semantics as a formal language with formal semantics then this becomes a formal proof: 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. -- Copyright 2022 Pete Olcott "Talent hits a target no one else can hit; Genius hits a target no one else can see." Arthur Schopenhauer
[toc] | [prev] | [next] | [standalone]
| From | olcott <NoOne@NoWhere.com> |
|---|---|
| Date | 2022-07-04 14:17 -0500 |
| Message-ID | <-vGdnazQwchWoV7_nZ2dnUU7_83NnZ2d@giganews.com> |
| In reply to | #3522 |
On 7/4/2022 1:42 PM, dklei...@gmail.com wrote: > On Monday, July 4, 2022 at 9:57:28 AM UTC-7, olcott wrote: >> On 7/4/2022 11:36 AM, dklei...@gmail.com wrote: >>> On Sunday, July 3, 2022 at 5:44:32 PM UTC-7, olcott wrote: >>>> On 7/3/2022 6:10 PM, dklei...@gmail.com wrote: >>>>> On Sunday, July 3, 2022 at 12:51:41 PM UTC-7, olcott wrote: >>>>>> On 7/3/2022 2:35 PM, dklei...@gmail.com wrote: >>>>>>> On Sunday, July 3, 2022 at 9:05:30 AM UTC-7, olcott wrote: >>>>>>>> >>>>>>>> *This general principle refutes conventional halting problem proofs* >>>>>>>> >>>>>>>> Every simulating halt decider that correctly simulates its input until >>>>>>>> it correctly predicts that this simulated input would never reach its >>>>>>>> final state, correctly rejects this input as non-halting. >>>>>>>> >>>>>>> This "general principle is" a trivial definition: A simulation of a >>>>>>> called routine that stops when it can predict that the routine >>>>>>> will never return is called a halt decider. >>>>>>> >>>>>>> In words of one syllable - so what? >>>>>> >>>>>> It refutes conventional halting problem proofs >>>>>> >>>>> It might if any such halt deciders existed. You need to prove such "halt >>>>> deciders" exist. >>>> >>>> You can't keep ignoring my paper and claiming that I have not proved my >>>> point. >>>> *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 >>>> >>> Your paper is not acceptable as a proof of anything. But that is to >>> be expected because my standard is mathematical proof and >>> you don't even pretend to be doing mathematics. >> >> When we construe the x86 language and its associated semantics as a >> formal language with formal semantics then this becomes a formal proof: >> > There is a great deal more to a mathematical proof than a formal > language. I believe that you do not have training in mathematics and you > do show little sympathy for the concerns of the mathematical > community. What you call "software engineering" is essentially hostile to > classical mathematics. > > Moreover if you wish us to take you seriously you must do more than > "construing". You must exhibit the x86 "language" as a formal system > and show how it is used in a formal proof. What more is there to the essence of any formal proof besides applying the formal semantics specified by a formal language as a sequence of truth preserving steps? Instead of premises a computation has an initial state. Instead of a conclusion premises a computation has a final state. *Curry–Howard correspondence* In programming language theory and proof theory, the Curry–Howard correspondence (also known as the Curry–Howard isomorphism or equivalence, or the proofs-as-programs and propositions- or formulae-as-types interpretation) is the direct relationship between computer programs and mathematical proofs. https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence -- Copyright 2022 Pete Olcott "Talent hits a target no one else can hit; Genius hits a target no one else can see." Arthur Schopenhauer
[toc] | [prev] | [next] | [standalone]
| From | olcott <NoOne@NoWhere.com> |
|---|---|
| Date | 2022-07-04 14:21 -0500 |
| Message-ID | <-vGdna_QwcgvoF7_nZ2dnUU7_81g4p2d@giganews.com> |
| In reply to | #3532 |
On 7/4/2022 2:17 PM, olcott wrote: > On 7/4/2022 1:42 PM, dklei...@gmail.com wrote: >> On Monday, July 4, 2022 at 9:57:28 AM UTC-7, olcott wrote: >>> On 7/4/2022 11:36 AM, dklei...@gmail.com wrote: >>>> On Sunday, July 3, 2022 at 5:44:32 PM UTC-7, olcott wrote: >>>>> On 7/3/2022 6:10 PM, dklei...@gmail.com wrote: >>>>>> On Sunday, July 3, 2022 at 12:51:41 PM UTC-7, olcott wrote: >>>>>>> On 7/3/2022 2:35 PM, dklei...@gmail.com wrote: >>>>>>>> On Sunday, July 3, 2022 at 9:05:30 AM UTC-7, olcott wrote: >>>>>>>>> >>>>>>>>> *This general principle refutes conventional halting problem >>>>>>>>> proofs* >>>>>>>>> >>>>>>>>> Every simulating halt decider that correctly simulates its >>>>>>>>> input until >>>>>>>>> it correctly predicts that this simulated input would never >>>>>>>>> reach its >>>>>>>>> final state, correctly rejects this input as non-halting. >>>>>>>>> >>>>>>>> This "general principle is" a trivial definition: A simulation of a >>>>>>>> called routine that stops when it can predict that the routine >>>>>>>> will never return is called a halt decider. >>>>>>>> >>>>>>>> In words of one syllable - so what? >>>>>>> >>>>>>> It refutes conventional halting problem proofs >>>>>>> >>>>>> It might if any such halt deciders existed. You need to prove such >>>>>> "halt >>>>>> deciders" exist. >>>>> >>>>> You can't keep ignoring my paper and claiming that I have not >>>>> proved my >>>>> point. >>>>> *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 >>>>> >>>>> >>>> Your paper is not acceptable as a proof of anything. But that is to >>>> be expected because my standard is mathematical proof and >>>> you don't even pretend to be doing mathematics. >>> >>> When we construe the x86 language and its associated semantics as a >>> formal language with formal semantics then this becomes a formal proof: >>> >> There is a great deal more to a mathematical proof than a formal >> language. I believe that you do not have training in mathematics and you >> do show little sympathy for the concerns of the mathematical >> community. What you call "software engineering" is essentially hostile to >> classical mathematics. >> >> Moreover if you wish us to take you seriously you must do more than >> "construing". You must exhibit the x86 "language" as a formal system >> and show how it is used in a formal proof. > > What more is there to the essence of any formal proof besides applying > the formal semantics specified by a formal language as a sequence of > truth preserving steps? > > Instead of premises a computation has an initial state. > Instead of a conclusion premises a computation has a final state. Instead of a conclusion a computation has a final state. > > *Curry–Howard correspondence* > In programming language theory and proof theory, the Curry–Howard > correspondence (also known as the Curry–Howard isomorphism or > equivalence, or the proofs-as-programs and propositions- or > formulae-as-types interpretation) is the direct relationship between > computer programs and mathematical proofs. > > https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence > -- Copyright 2022 Pete Olcott "Talent hits a target no one else can hit; Genius hits a target no one else can see." Arthur Schopenhauer
[toc] | [prev] | [next] | [standalone]
| From | olcott <NoOne@NoWhere.com> |
|---|---|
| Date | 2022-07-04 18:08 -0500 |
| Subject | Re: Halting problem proofs refuted on the basis of software engineering [ Curry–Howard correspondence ] |
| Message-ID | <SYWdnQoA9L5I717_nZ2dnUU7_83NnZ2d@giganews.com> |
| In reply to | #3522 |
On 7/4/2022 1:42 PM, dklei...@gmail.com wrote: > On Monday, July 4, 2022 at 9:57:28 AM UTC-7, olcott wrote: >> On 7/4/2022 11:36 AM, dklei...@gmail.com wrote: >>> On Sunday, July 3, 2022 at 5:44:32 PM UTC-7, olcott wrote: >>>> On 7/3/2022 6:10 PM, dklei...@gmail.com wrote: >>>>> On Sunday, July 3, 2022 at 12:51:41 PM UTC-7, olcott wrote: >>>>>> On 7/3/2022 2:35 PM, dklei...@gmail.com wrote: >>>>>>> On Sunday, July 3, 2022 at 9:05:30 AM UTC-7, olcott wrote: >>>>>>>> >>>>>>>> *This general principle refutes conventional halting problem proofs* >>>>>>>> >>>>>>>> Every simulating halt decider that correctly simulates its input until >>>>>>>> it correctly predicts that this simulated input would never reach its >>>>>>>> final state, correctly rejects this input as non-halting. >>>>>>>> >>>>>>> This "general principle is" a trivial definition: A simulation of a >>>>>>> called routine that stops when it can predict that the routine >>>>>>> will never return is called a halt decider. >>>>>>> >>>>>>> In words of one syllable - so what? >>>>>> >>>>>> It refutes conventional halting problem proofs >>>>>> >>>>> It might if any such halt deciders existed. You need to prove such "halt >>>>> deciders" exist. >>>> >>>> You can't keep ignoring my paper and claiming that I have not proved my >>>> point. >>>> *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 >>>> >>> Your paper is not acceptable as a proof of anything. But that is to >>> be expected because my standard is mathematical proof and >>> you don't even pretend to be doing mathematics. >> >> When we construe the x86 language and its associated semantics as a >> formal language with formal semantics then this becomes a formal proof: >> > There is a great deal more to a mathematical proof than a formal > language. I believe that you do not have training in mathematics and you > do show little sympathy for the concerns of the mathematical > community. What you call "software engineering" is essentially hostile to > classical mathematics. > > Moreover if you wish us to take you seriously you must do more than > "construing". You must exhibit the x86 "language" as a formal system > and show how it is used in a formal proof. It would seem that *Curry–Howard correspondence* https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence would allow the x86 language and its semantics to be construed as a formal system such that the initial state and final state of a computable function along with all of the state transitions between could be construed as a formal proof. -- Copyright 2022 Pete Olcott "Talent hits a target no one else can hit; Genius hits a target no one else can see." Arthur Schopenhauer
[toc] | [prev] | [next] | [standalone]
| From | olcott <NoOne@NoWhere.com> |
|---|---|
| Date | 2022-07-05 14:31 -0500 |
| Subject | Re: Halting problem proofs refuted on the basis of software engineering [ Curry–Howard correspondence ] |
| Message-ID | <f8ednbiyxKkBDFn_nZ2dnUU7_83NnZ2d@giganews.com> |
| In reply to | #3535 |
On 7/5/2022 1:50 PM, dklei...@gmail.com wrote:
> On Monday, July 4, 2022 at 4:08:12 PM UTC-7, olcott wrote:
>> On 7/4/2022 1:42 PM, dklei...@gmail.com wrote:
>>> On Monday, July 4, 2022 at 9:57:28 AM UTC-7, olcott wrote:
>>>> On 7/4/2022 11:36 AM, dklei...@gmail.com wrote:
>>>>> On Sunday, July 3, 2022 at 5:44:32 PM UTC-7, olcott wrote:
>>>>>> On 7/3/2022 6:10 PM, dklei...@gmail.com wrote:
>>>>>>> On Sunday, July 3, 2022 at 12:51:41 PM UTC-7, olcott wrote:
>>>>>>>> On 7/3/2022 2:35 PM, dklei...@gmail.com wrote:
>>>>>>>>> On Sunday, July 3, 2022 at 9:05:30 AM UTC-7, olcott wrote:
>>>>>>>>>>
>>>>>>>>>> *This general principle refutes conventional halting problem proofs*
>>>>>>>>>>
>>>>>>>>>> Every simulating halt decider that correctly simulates its input until
>>>>>>>>>> it correctly predicts that this simulated input would never reach its
>>>>>>>>>> final state, correctly rejects this input as non-halting.
>>>>>>>>>>
>>>>>>>>> This "general principle is" a trivial definition: A simulation of a
>>>>>>>>> called routine that stops when it can predict that the routine
>>>>>>>>> will never return is called a halt decider.
>>>>>>>>>
>>>>>>>>> In words of one syllable - so what?
>>>>>>>>
>>>>>>>> It refutes conventional halting problem proofs
>>>>>>>>
>>>>>>> It might if any such halt deciders existed. You need to prove such "halt
>>>>>>> deciders" exist.
>>>>>>
>>>>>> You can't keep ignoring my paper and claiming that I have not proved my
>>>>>> point.
>>>>>> *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
>>>>>>
>>>>> Your paper is not acceptable as a proof of anything. But that is to
>>>>> be expected because my standard is mathematical proof and
>>>>> you don't even pretend to be doing mathematics.
>>>>
>>>> When we construe the x86 language and its associated semantics as a
>>>> formal language with formal semantics then this becomes a formal proof:
>>>>
>>> There is a great deal more to a mathematical proof than a formal
>>> language. I believe that you do not have training in mathematics and you
>>> do show little sympathy for the concerns of the mathematical
>>> community. What you call "software engineering" is essentially hostile to
>>> classical mathematics.
>>>
>>> Moreover if you wish us to take you seriously you must do more than
>>> "construing". You must exhibit the x86 "language" as a formal system
>>> and show how it is used in a formal proof.
>> It would seem that *Curry–Howard correspondence*
>> https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence
>> would allow the x86 language and its semantics to be construed as a
>> formal system such that the initial state and final state of a
>> computable function along with all of the state transitions between
>> could be construed as a formal proof.
>
> I am afraid you don't see mathematical proof like a mathematician
> might. A good and simple example is the theorem that proves all
> Burnside three groups are finite.
>
> But if you do want to use the Curry-Howard correspondence as a
> proof method you must either reference the formal x86 language
> formulation or yourself supply such a formal language description.
>
I already provided this:
x86 Instruction Set Reference
https://c9x.me/x86/
> Your task would be much easier were you to use C as the formal
> language. And much easier to follow.
If we use C as the formal language then we have to translate it into its
corresponding directed graph of control flow ourselves or the computer
will not be able to process it.
I use C/x86 together so the human can examine the C and the machine can
examine the machine code and the human can see the bijection between the
C and the machine code as assembly language generated from the C.
void P(u32 x)
{
if (H(x, x))
HERE: goto HERE;
return;
}
_P()
[00001202](01) 55 push ebp
[00001203](02) 8bec mov ebp,esp
[00001205](03) 8b4508 mov eax,[ebp+08]
[00001208](01) 50 push eax
[00001209](03) 8b4d08 mov ecx,[ebp+08]
[0000120c](01) 51 push ecx
[0000120d](05) e820feffff call 00001032
[00001212](03) 83c408 add esp,+08
[00001215](02) 85c0 test eax,eax
[00001217](02) 7402 jz 0000121b
[00001219](02) ebfe jmp 00001219
[0000121b](01) 5d pop ebp
[0000121c](01) c3 ret
Size in bytes:(0027) [0000121c]
--
Copyright 2022 Pete Olcott
"Talent hits a target no one else can hit;
Genius hits a target no one else can see."
Arthur Schopenhauer
[toc] | [prev] | [next] | [standalone]
| From | olcott <NoOne@NoWhere.com> |
|---|---|
| Date | 2022-07-05 15:42 -0500 |
| Subject | Re: Halting problem proofs refuted on the basis of software engineering [ Curry–Howard correspondence ] |
| Message-ID | <HI6dncus-5-vP1n_nZ2dnUU7_83NnZ2d@giganews.com> |
| In reply to | #3535 |
On 7/5/2022 3:24 PM, André G. Isaak wrote: > On 2022-07-05 12:50, dklei...@gmail.com wrote: >> On Monday, July 4, 2022 at 4:08:12 PM UTC-7, olcott wrote: >>> On 7/4/2022 1:42 PM, dklei...@gmail.com wrote: >>>> On Monday, July 4, 2022 at 9:57:28 AM UTC-7, olcott wrote: >>>>> On 7/4/2022 11:36 AM, dklei...@gmail.com wrote: >>>>>> On Sunday, July 3, 2022 at 5:44:32 PM UTC-7, olcott wrote: >>>>>>> On 7/3/2022 6:10 PM, dklei...@gmail.com wrote: >>>>>>>> On Sunday, July 3, 2022 at 12:51:41 PM UTC-7, olcott wrote: >>>>>>>>> On 7/3/2022 2:35 PM, dklei...@gmail.com wrote: >>>>>>>>>> On Sunday, July 3, 2022 at 9:05:30 AM UTC-7, olcott wrote: >>>>>>>>>>> >>>>>>>>>>> *This general principle refutes conventional halting problem >>>>>>>>>>> proofs* >>>>>>>>>>> >>>>>>>>>>> Every simulating halt decider that correctly simulates its >>>>>>>>>>> input until >>>>>>>>>>> it correctly predicts that this simulated input would never >>>>>>>>>>> reach its >>>>>>>>>>> final state, correctly rejects this input as non-halting. >>>>>>>>>>> >>>>>>>>>> This "general principle is" a trivial definition: A simulation >>>>>>>>>> of a >>>>>>>>>> called routine that stops when it can predict that the routine >>>>>>>>>> will never return is called a halt decider. >>>>>>>>>> >>>>>>>>>> In words of one syllable - so what? >>>>>>>>> >>>>>>>>> It refutes conventional halting problem proofs >>>>>>>>> >>>>>>>> It might if any such halt deciders existed. You need to prove >>>>>>>> such "halt >>>>>>>> deciders" exist. >>>>>>> >>>>>>> You can't keep ignoring my paper and claiming that I have not >>>>>>> proved my >>>>>>> point. >>>>>>> *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 >>>>>>> >>>>>>> >>>>>> Your paper is not acceptable as a proof of anything. But that is to >>>>>> be expected because my standard is mathematical proof and >>>>>> you don't even pretend to be doing mathematics. >>>>> >>>>> When we construe the x86 language and its associated semantics as a >>>>> formal language with formal semantics then this becomes a formal >>>>> proof: >>>>> >>>> There is a great deal more to a mathematical proof than a formal >>>> language. I believe that you do not have training in mathematics and >>>> you >>>> do show little sympathy for the concerns of the mathematical >>>> community. What you call "software engineering" is essentially >>>> hostile to >>>> classical mathematics. >>>> >>>> Moreover if you wish us to take you seriously you must do more than >>>> "construing". You must exhibit the x86 "language" as a formal system >>>> and show how it is used in a formal proof. >>> It would seem that *Curry–Howard correspondence* >>> https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence >>> would allow the x86 language and its semantics to be construed as a >>> formal system such that the initial state and final state of a >>> computable function along with all of the state transitions between >>> could be construed as a formal proof. >> >> I am afraid you don't see mathematical proof like a mathematician >> might. A good and simple example is the theorem that proves all >> Burnside three groups are finite. >> >> But if you do want to use the Curry-Howard correspondence as a >> proof method you must either reference the formal x86 language >> formulation or yourself supply such a formal language description. >> >> Your task would be much easier were you to use C as the formal >> language. And much easier to follow. > > If he really wants to use (and if he actually understood) Curry-Howard, > he'd be better off using Scheme or Haskell or something like that... > > But it wouldn't make a difference. He has not provided an actual proof > NOR an actual program, so talking about some alleged correspondence > between two imaginary entities is hardly going to enlighten anyone. > > André > Welcome back you are one of my competent reviewers. *My most recent paper provides complete proof of this* 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. *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 *Only to those having the required software engineering prerequisites* The start state, state transitions inbetween and the final state of a computation can be construed as a formal proof from premises to conclusion. -- Copyright 2022 Pete Olcott "Talent hits a target no one else can hit; Genius hits a target no one else can see." Arthur Schopenhauer
[toc] | [prev] | [next] | [standalone]
| From | Richard Damon <Richard@Damon-Family.org> |
|---|---|
| Date | 2022-07-05 19:29 -0400 |
| Subject | Re: Halting problem proofs refuted on the basis of software engineering [ Curry–Howard correspondence ] |
| Message-ID | <qP3xK.19679$BZ1.10403@fx03.iad> |
| In reply to | #3541 |
On 7/5/22 4:42 PM, olcott wrote: > On 7/5/2022 3:24 PM, André G. Isaak wrote: >> On 2022-07-05 12:50, dklei...@gmail.com wrote: >>> On Monday, July 4, 2022 at 4:08:12 PM UTC-7, olcott wrote: >>>> On 7/4/2022 1:42 PM, dklei...@gmail.com wrote: >>>>> On Monday, July 4, 2022 at 9:57:28 AM UTC-7, olcott wrote: >>>>>> On 7/4/2022 11:36 AM, dklei...@gmail.com wrote: >>>>>>> On Sunday, July 3, 2022 at 5:44:32 PM UTC-7, olcott wrote: >>>>>>>> On 7/3/2022 6:10 PM, dklei...@gmail.com wrote: >>>>>>>>> On Sunday, July 3, 2022 at 12:51:41 PM UTC-7, olcott wrote: >>>>>>>>>> On 7/3/2022 2:35 PM, dklei...@gmail.com wrote: >>>>>>>>>>> On Sunday, July 3, 2022 at 9:05:30 AM UTC-7, olcott wrote: >>>>>>>>>>>> >>>>>>>>>>>> *This general principle refutes conventional halting problem >>>>>>>>>>>> proofs* >>>>>>>>>>>> >>>>>>>>>>>> Every simulating halt decider that correctly simulates its >>>>>>>>>>>> input until >>>>>>>>>>>> it correctly predicts that this simulated input would never >>>>>>>>>>>> reach its >>>>>>>>>>>> final state, correctly rejects this input as non-halting. >>>>>>>>>>>> >>>>>>>>>>> This "general principle is" a trivial definition: A >>>>>>>>>>> simulation of a >>>>>>>>>>> called routine that stops when it can predict that the routine >>>>>>>>>>> will never return is called a halt decider. >>>>>>>>>>> >>>>>>>>>>> In words of one syllable - so what? >>>>>>>>>> >>>>>>>>>> It refutes conventional halting problem proofs >>>>>>>>>> >>>>>>>>> It might if any such halt deciders existed. You need to prove >>>>>>>>> such "halt >>>>>>>>> deciders" exist. >>>>>>>> >>>>>>>> You can't keep ignoring my paper and claiming that I have not >>>>>>>> proved my >>>>>>>> point. >>>>>>>> *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 >>>>>>>> >>>>>>>> >>>>>>> Your paper is not acceptable as a proof of anything. But that is to >>>>>>> be expected because my standard is mathematical proof and >>>>>>> you don't even pretend to be doing mathematics. >>>>>> >>>>>> When we construe the x86 language and its associated semantics as a >>>>>> formal language with formal semantics then this becomes a formal >>>>>> proof: >>>>>> >>>>> There is a great deal more to a mathematical proof than a formal >>>>> language. I believe that you do not have training in mathematics >>>>> and you >>>>> do show little sympathy for the concerns of the mathematical >>>>> community. What you call "software engineering" is essentially >>>>> hostile to >>>>> classical mathematics. >>>>> >>>>> Moreover if you wish us to take you seriously you must do more than >>>>> "construing". You must exhibit the x86 "language" as a formal system >>>>> and show how it is used in a formal proof. >>>> It would seem that *Curry–Howard correspondence* >>>> https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence >>>> would allow the x86 language and its semantics to be construed as a >>>> formal system such that the initial state and final state of a >>>> computable function along with all of the state transitions between >>>> could be construed as a formal proof. >>> >>> I am afraid you don't see mathematical proof like a mathematician >>> might. A good and simple example is the theorem that proves all >>> Burnside three groups are finite. >>> >>> But if you do want to use the Curry-Howard correspondence as a >>> proof method you must either reference the formal x86 language >>> formulation or yourself supply such a formal language description. >>> >>> Your task would be much easier were you to use C as the formal >>> language. And much easier to follow. >> >> If he really wants to use (and if he actually understood) >> Curry-Howard, he'd be better off using Scheme or Haskell or something >> like that... >> >> But it wouldn't make a difference. He has not provided an actual proof >> NOR an actual program, so talking about some alleged correspondence >> between two imaginary entities is hardly going to enlighten anyone. >> >> André >> > > Welcome back you are one of my competent reviewers. > > *My most recent paper provides complete proof of this* > > 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. > > *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 > > > *Only to those having the required software engineering prerequisites* > > The start state, state transitions inbetween and the final state of a > computation can be construed as a formal proof from premises to conclusion. > > Except that H doesn't actually look at the input as an actual program, but replaces the call to H with parameters P,P with something that acts differently then the actual call to H(P,P) from "main", so fails to meet the requirements of Curly-Howard. Note, your rule (b) is incorrect as you use it, which is a core fault with your "proof".
[toc] | [prev] | [next] | [standalone]
| From | olcott <NoOne@NoWhere.com> |
|---|---|
| Date | 2022-07-05 19:01 -0500 |
| Subject | Re: Halting problem proofs refuted on the basis of software engineering [ Curry–Howard correspondence ] |
| Message-ID | <19idnQ_DrKFbTVn_nZ2dnUU7_8zNnZ2d@giganews.com> |
| In reply to | #3535 |
On 7/5/2022 6:53 PM, Ben Bacarisse wrote: > "dklei...@gmail.com" <dkleinecke@gmail.com> writes: > >> But if you do want to use the Curry-Howard correspondence as a >> proof method you must either reference the formal x86 language >> formulation or yourself supply such a formal language description. > > Goodness, no. He'd have to do a whole lot more than that. It's clear > he has no idea what the Curry-Howard correspondence is about. It's > simply not relevant to "x86 language". > > If anyone can be bothered to show that PO knows nothing about this > subtopic, just ask him: what is the type of the "x86 language" program > that corresponds to the proof he is claiming. > >> Your task would be much easier were you to use C as the formal >> language. And much easier to follow. > > But that's *why* he's not using anything better. Clarity is anathema to > cranks. > Bullshit Ben and you know better: The halt decider must have machine code the human users can see this in C and the assembly language mapping from C to x86 assembly language allows the human users to see what the halt decider is doing and verify that it is correct. -- Copyright 2022 Pete Olcott "Talent hits a target no one else can hit; Genius hits a target no one else can see." Arthur Schopenhauer
[toc] | [prev] | [next] | [standalone]
| From | olcott <NoOne@NoWhere.com> |
|---|---|
| Date | 2022-07-06 16:13 -0500 |
| Subject | Re: Halting problem proofs refuted on the basis of software engineering [ Curry–Howard correspondence ] |
| Message-ID | <KeadnaibXr-ZZlj_nZ2dnUU7_83NnZ2d@giganews.com> |
| In reply to | #3544 |
On 7/6/2022 3:58 PM, dklei...@gmail.com wrote: > On Tuesday, July 5, 2022 at 9:02:28 PM UTC-7, olcott wrote: >> On 7/5/2022 11:00 PM, dklei...@gmail.com wrote: >>> On Tuesday, July 5, 2022 at 5:01:17 PM UTC-7, olcott wrote: >>>> >>>> The halt decider must have machine code >>>> >>> Why? What is impossible to do in C? >> >> It is not impossible it is merely 1000-fold more work that is already >> done by the compiler. Do you know what a directed graph is? >> > I know what a directed graph is and I don't see why you mention them. > > There is no reason to ever compiler so the compiler is not necessary. > C is a perfectly good well-defined formal language. And apparently > you agree your arguments could be expressed in C. When a C function is translated into machine code it is very easy for a computer program to examine the control flow of this x86 emulated x86 code while it is running. This is not at all the case when the halt decider only has static C source-code. In this case the halt decider would be required to implement its own C interpreter before it could begin its dynamic analysis. Another advantage of x86 machine code is there there are no multiple levels of nested control flow, there is only a single flat address space. Every control flow is simply a directed path from, one address to another, forming a single network of all control flow. >> >>>> the human users can see this in >>>> C and the assembly language mapping from C to x86 assembly language >>>> allows the human users to see what the halt decider is doing and verify >>>> that it is correct. -- Copyright 2022 Pete Olcott "Talent hits a target no one else can hit; Genius hits a target no one else can see." Arthur Schopenhauer
[toc] | [prev] | [next] | [standalone]
| From | olcott <NoOne@NoWhere.com> |
|---|---|
| Date | 2022-07-07 16:08 -0500 |
| Subject | Re: Halting problem proofs refuted on the basis of software engineering [ Curry–Howard correspondence ] |
| Message-ID | <1v2dnYG44Zah1lr_nZ2dnUU7_8zNnZ2d@giganews.com> |
| In reply to | #3556 |
On 7/7/2022 3:54 PM, dklei...@gmail.com wrote: > On Thursday, July 7, 2022 at 12:39:41 PM UTC-7, olcott wrote: >> On 7/7/2022 2:19 PM, dklei...@gmail.com wrote: >>> On Wednesday, July 6, 2022 at 2:13:47 PM UTC-7, olcott wrote: >>>> On 7/6/2022 3:58 PM, dklei...@gmail.com wrote: >>>>> On Tuesday, July 5, 2022 at 9:02:28 PM UTC-7, olcott wrote: >>>>>> On 7/5/2022 11:00 PM, dklei...@gmail.com wrote: >>>>>>> On Tuesday, July 5, 2022 at 5:01:17 PM UTC-7, olcott wrote: >>>>>>>> >>>>>>>> The halt decider must have machine code >>>>>>>> >>>>>>> Why? What is impossible to do in C? >>>>>> >>>>>> It is not impossible it is merely 1000-fold more work that is already >>>>>> done by the compiler. Do you know what a directed graph is? >>>>>> >>>>> I know what a directed graph is and I don't see why you mention them. >>>>> >>>>> There is no reason to ever compiler so the compiler is not necessary. >>>>> C is a perfectly good well-defined formal language. And apparently >>>>> you agree your arguments could be expressed in C. >>>> When a C function is translated into machine code it is very easy for a >>>> computer program to examine the control flow of this x86 emulated x86 >>>> code while it is running. >>>> >>>> This is not at all the case when the halt decider only has static C >>>> source-code. In this case the halt decider would be required to >>>> implement its own C interpreter before it could begin its dynamic analysis. >>>> >>>> Another advantage of x86 machine code is there there are no multiple >>>> levels of nested control flow, there is only a single flat address >>>> space. Every control flow is simply a directed path from, one address to >>>> another, forming a single network of all control flow. >>>>>> >>>>>>>> the human users can see this in >>>>>>>> C and the assembly language mapping from C to x86 assembly language >>>>>>>> allows the human users to see what the halt decider is doing and verify >>>>>>>> that it is correct. >>> >>> Have you ever dissambled a complex program? Especially one written in >>> assembly? Making sense of the control flow is usually the hardest part of >>> the task. IMO, and that of the computer community in general, is that >>> higher order languages - such as C - are much easier to read. >>> >> *I will repeat this point several times because you keep not getting it* >> >> Control flow x86 is much easier for machines than control flow in C >> Control flow x86 is much easier for machines than control flow in C >> Control flow x86 is much easier for machines than control flow in C >> Control flow x86 is much easier for machines than control flow in C >> Control flow x86 is much easier for machines than control flow in C > > It might be easier for the machine. But that's not the point. The goal > of a proof is to convince human readers that such-and-such is true. If the human reader is too lazy to understand the x86 language then the human reader is too lazy to understand what the halt decider is doing. > So what matters is humans reading formal languages. > What are the properties of a formal language that distinguish it from a natural language? The x86 language has all of these properties. https://en.wikipedia.org/wiki/Formal_language https://en.wikipedia.org/wiki/Semantics_(computer_science) > This is, rather clearly, subjective. What is easy for me might be hard > for you. But the audience of proofs - usually mathematicians - clearly > prefers higher-order languages. C is probably not the best choice of > formal language but it will do if you must use it. Readers that insist on making sure that they continue to lack the mandatory prerequisites to understand my proof will continue to fail to understand my proof. *To fully understand this paper a* *software engineer must be an expert in* (a) The C programming language. (b) The x86 programming language. (c) Exactly how C translates into x86 (how C function calls are implemented in x86). (d) The ability to recognize infinite recursion at the x86 assembly language level. *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 -- Copyright 2022 Pete Olcott "Talent hits a target no one else can hit; Genius hits a target no one else can see." Arthur Schopenhauer
[toc] | [prev] | [next] | [standalone]
| From | olcott <NoOne@NoWhere.com> |
|---|---|
| Date | 2022-07-07 20:34 -0500 |
| Subject | Re: Halting problem proofs refuted on the basis of software engineering [ Curry–Howard correspondence ] |
| Message-ID | <nLKdnWzS7d48FFr_nZ2dnUU7_83NnZ2d@giganews.com> |
| In reply to | #3558 |
On 7/7/2022 7:36 PM, dklei...@gmail.com wrote:
> On Thursday, July 7, 2022 at 2:08:19 PM UTC-7, olcott wrote:
>> On 7/7/2022 3:54 PM, dklei...@gmail.com wrote:
>>> On Thursday, July 7, 2022 at 12:39:41 PM UTC-7, olcott wrote:
>>>> On 7/7/2022 2:19 PM, dklei...@gmail.com wrote:
>>
>>>>> Have you ever dissambled a complex program? Especially one written in
>>>>> assembly? Making sense of the control flow is usually the hardest part of
>>>>> the task. IMO, and that of the computer community in general, is that
>>>>> higher order languages - such as C - are much easier to read.
>>>>>
> . . .
>>>> Control flow x86 is much easier for machines than control flow in C
>>>
>>> It might be easier for the machine. But that's not the point. The goal
>>> of a proof is to convince human readers that such-and-such is true.
>>
>> If the human reader is too lazy to understand the x86 language then the
>> human reader is too lazy to understand what the halt decider is doing.
>
> Why ask them to do something orders of magnitude harder than
> necessary? Reading C is much easier than reading x86.
Then we have disagreements that are entirely based on interpreting the
vagueness differently.
typedef void (*ptr)();
// rec routine P
// §L :if T[P] go to L
// Return §
void Strachey_P()
{
L: if (T(Strachey_P)) goto L;
return;
}
int main()
{
Output("Input_Halts = ", T(Strachey_P));
}
When I say that simulating halt decider T correctly determines that its
input never reaches its "return" statement on the basis that T can see
Strachey_P calling itself with its same parameters there are not enough
details provided to correctly understand that I am necessarily correct.
*When we look at the x86 level we have 100% of all of these details*
>>
>>> So what matters is humans reading formal languages.
>>>
>> What are the properties of a formal language that distinguish it from a
>> natural language?
>>
> Formal language is very different than natural language. But the
> difference that matters is that formal languages are precisely defined -
> in both syntax and semantics. The higher-order computer languages
> are designed (precisely) to feel more like natural language to the user.
The x86 language is this same way.
--
Copyright 2022 Pete Olcott
"Talent hits a target no one else can hit;
Genius hits a target no one else can see."
Arthur Schopenhauer
[toc] | [prev] | [next] | [standalone]
| From | olcott <NoOne@NoWhere.com> |
|---|---|
| Date | 2022-07-07 23:48 -0500 |
| Subject | Re: Halting problem proofs refuted on the basis of software engineering [ Curry–Howard correspondence ] |
| Message-ID | <A_adncjcX-yXKlr_nZ2dnUU7_8zNnZ2d@giganews.com> |
| In reply to | #3559 |
On 7/7/2022 11:35 PM, dklei...@gmail.com wrote:
> On Thursday, July 7, 2022 at 6:34:32 PM UTC-7, olcott wrote:
>> On 7/7/2022 7:36 PM, dklei...@gmail.com wrote:
>>> On Thursday, July 7, 2022 at 2:08:19 PM UTC-7, olcott wrote:
>>>> On 7/7/2022 3:54 PM, dklei...@gmail.com wrote:
>>>>> On Thursday, July 7, 2022 at 12:39:41 PM UTC-7, olcott wrote:
>>>>>> On 7/7/2022 2:19 PM, dklei...@gmail.com wrote:
>>>>
>>>>>>> Have you ever dissambled a complex program? Especially one written in
>>>>>>> assembly? Making sense of the control flow is usually the hardest part of
>>>>>>> the task. IMO, and that of the computer community in general, is that
>>>>>>> higher order languages - such as C - are much easier to read.
>>>>>>>
>>> . . .
>>>>>> Control flow x86 is much easier for machines than control flow in C
>>>>>
>>>>> It might be easier for the machine. But that's not the point. The goal
>>>>> of a proof is to convince human readers that such-and-such is true.
>>>>
>>>> If the human reader is too lazy to understand the x86 language then the
>>>> human reader is too lazy to understand what the halt decider is doing.
>>>
>>> Why ask them to do something orders of magnitude harder than
>>> necessary? Reading C is much easier than reading x86.
>> Then we have disagreements that are entirely based on interpreting the
>> vagueness differently.
>>
> int Strachey_P(void) {
> if (T(&Strachey_P)) return 1;
> else return 0; }
>
> int main() {
> if (T(&Strachey_P)) Output("Halts");
> else Output ("Does not halt");}
>
> Without the definition of T this is just boiler plate.
Yours is incorrect:
typedef void (*ptr)();
// rec routine P
// §L :if T[P] go to L
// Return §
void Strachey_P()
{
L: if (T(Strachey_P)) goto L;
return;
}
int main()
{
Output("Input_Halts = ", T(Strachey_P));
}
--
Copyright 2022 Pete Olcott
"Talent hits a target no one else can hit;
Genius hits a target no one else can see."
Arthur Schopenhauer
[toc] | [prev] | [next] | [standalone]
| From | olcott <NoOne@NoWhere.com> |
|---|---|
| Date | 2022-07-09 13:40 -0500 |
| Subject | Re: Halting problem proofs refuted on the basis of software engineering [ Irrefutably Correct ] |
| Message-ID | <JLudndvy85E6VlT_nZ2dnUU7_83NnZ2d@giganews.com> |
| In reply to | #3560 |
On 7/9/2022 12:22 PM, dklei...@gmail.com wrote:
> On Saturday, July 9, 2022 at 6:16:37 AM UTC-7, olcott wrote:
>> On 7/8/2022 5:48 PM, olcott wrote:
>>> On 7/8/2022 1:09 AM, dklei...@gmail.com wrote:
>>>> On Thursday, July 7, 2022 at 9:48:17 PM UTC-7, olcott wrote:
>>>>> On 7/7/2022 11:35 PM, dklei...@gmail.com wrote:
>>>>>
>>>>>> int Strachey_P(void) {
>>>>>> if (T(&Strachey_P)) return 1;
>>>>>> else return 0; }
>>>>>>
>>>>>> int main() {
>>>>>> if (T(&Strachey_P)) Output("Halts");
>>>>>> else Output ("Does not halt");}
>>>>>>
>>>>>> Without the definition of T this is just boiler plate.
>>>>>
>>>>> Yours is incorrect:
>>>>
>>>> How? I assume C89.
>>>
>>> typedef void (*ptr)();
>>>
>>> int Strachey_P2(void) {
>>> if (T(&Strachey_P2)) return 1;
>>> else return 0; }
>>>
>>> int main()
>>> {
>>> if (T(Strachey_P2)) OutputString("Halts\n");
>>> else OutputString("Does not halt\n");
>>> }
>>>
>>> _Strachey_P2()
>>> [0000134e](01) 55 push ebp
>>> [0000134f](02) 8bec mov ebp,esp
>>> [00001351](05) 684e130000 push 0000134e
>>> [00001356](05) e893fbffff call 00000eee
>>> [0000135b](03) 83c404 add esp,+04
>>> [0000135e](02) 85c0 test eax,eax
>>> [00001360](02) 7409 jz 0000136b
>>> [00001362](05) b801000000 mov eax,00000001
>>> [00001367](02) eb04 jmp 0000136d
>>> [00001369](02) eb02 jmp 0000136d
>>> [0000136b](02) 33c0 xor eax,eax
>>> [0000136d](01) 5d pop ebp
>>> [0000136e](01) c3 ret
>>> Size in bytes:(0033) [0000136e]
>>>
>>> _main()
>>> [0000137e](01) 55 push ebp
>>> [0000137f](02) 8bec mov ebp,esp
>>> [00001381](05) 684e130000 push 0000134e
>>> [00001386](05) e863fbffff call 00000eee
>>> [0000138b](03) 83c404 add esp,+04
>>> [0000138e](02) 85c0 test eax,eax
>>> [00001390](02) 740f jz 000013a1
>>> [00001392](05) 6817050000 push 00000517
>>> [00001397](05) e8c2f1ffff call 0000055e
>>> [0000139c](03) 83c404 add esp,+04
>>> [0000139f](02) eb0d jmp 000013ae
>>> [000013a1](05) 681f050000 push 0000051f
>>> [000013a6](05) e8b3f1ffff call 0000055e
>>> [000013ab](03) 83c404 add esp,+04
>>> [000013ae](02) 33c0 xor eax,eax
>>> [000013b0](01) 5d pop ebp
>>> [000013b1](01) c3 ret
>>> Size in bytes:(0052) [000013b1]
>>>
>>> machine stack stack machine assembly
>>> address address data code language
>>> ======== ======== ======== ========= =============
>>> [0000137e][001022be][00000000] 55 push ebp
>>> [0000137f][001022be][00000000] 8bec mov ebp,esp
>>> [00001381][001022ba][0000134e] 684e130000 push 0000134e
>>> [00001386][001022b6][0000138b] e863fbffff call 00000eee
>>>
>>> T: Begin Simulation Execution Trace Stored at:11236a
>>> Address_of_T:eee
>>> [0000134e][0011235a][0011235e] 55 push ebp
>>> [0000134f][0011235a][0011235e] 8bec mov ebp,esp
>>> [00001351][00112356][0000134e] 684e130000 push 0000134e
>>> [00001356][00112352][0000135b] e893fbffff call 00000eee
>>> T: Infinitely Recursive Simulation Detected Simulation Stopped
>>>
>>> [0000138b][001022be][00000000] 83c404 add esp,+04
>>> [0000138e][001022be][00000000] 85c0 test eax,eax
>>> [00001390][001022be][00000000] 740f jz 000013a1
>>> [000013a1][001022ba][0000051f] 681f050000 push 0000051f
>>> [000013a6][001022ba][0000051f] e8b3f1ffff call 0000055e
>>> Does not halt
>>> [000013ab][001022be][00000000] 83c404 add esp,+04
>>> [000013ae][001022be][00000000] 33c0 xor eax,eax
>>> [000013b0][001022c2][00000018] 5d pop ebp
>>> [000013b1][001022c6][00000000] c3 ret
>>> Number of Instructions Executed(539) == 8 Pages
>
> As nearly as I can tell this is all what I called boilerplate. Essentially
> no substantial content.
>
> If you have a computer program that shows what you claim show
> your complete code and we can check its validity. No programmer
> is competent to pass a definitive judgement baout his own work.
The above execution trace of simulating halt decider T(Strachey_P2)
proves that T correctly predicts that its correct and complete x86
emulation of its input would never reach the "ret" instruction of this
input. This allows T to correctly reject Strachey_P2 as non-halting.
Anyone having these required prerequisites can verify the above
paragraph without seeing the source-code.
To fully understand this paper a software engineer must be an expert in:
(a) The C programming language.
(b) The x86 programming language.
(c) Exactly how C translates into x86 (how C function calls are
implemented in x86).
(d) The ability to recognize infinite recursion at the x86 assembly
language level.
Anyone not having these required prerequisites will not be able to
verify the above paragraph even after seeing the source-code because
they will not be able to understand what the halt decider is doing
unless they know the x86 language quite well.
The code requires more refactoring before it is clean enough for
publication.
I updated the original x86 emulator so that
(1) It compiles under Windows as well as Linux. 16390 source-code lines.
(2) One of its original functions can disassemble or simulate its input
depending on a boolean flag.
(3) The COFF output of the the Microsoft C compiler can be directly
executed. (contained in Read_COFF_Object.h). 924 source-code lines.
The x86utm operation system is in x86utm.cpp
2038 source-code lines.
The various halt deciders and their sample input is in Halt7.c
638 source-code lines.
--
Copyright 2022 Pete Olcott
"Talent hits a target no one else can hit;
Genius hits a target no one else can see."
Arthur Schopenhauer
[toc] | [prev] | [next] | [standalone]
| From | Richard Damon <Richard@Damon-Family.org> |
|---|---|
| Date | 2022-07-09 15:06 -0400 |
| Subject | Re: Halting problem proofs refuted on the basis of software engineering [ Irrefutably Correct ] |
| Message-ID | <NkkyK.490830$JVi.390602@fx17.iad> |
| In reply to | #3561 |
On 7/9/22 2:40 PM, olcott wrote:
> On 7/9/2022 12:22 PM, dklei...@gmail.com wrote:
>> On Saturday, July 9, 2022 at 6:16:37 AM UTC-7, olcott wrote:
>>> On 7/8/2022 5:48 PM, olcott wrote:
>>>> On 7/8/2022 1:09 AM, dklei...@gmail.com wrote:
>>>>> On Thursday, July 7, 2022 at 9:48:17 PM UTC-7, olcott wrote:
>>>>>> On 7/7/2022 11:35 PM, dklei...@gmail.com wrote:
>>>>>>
>>>>>>> int Strachey_P(void) {
>>>>>>> if (T(&Strachey_P)) return 1;
>>>>>>> else return 0; }
>>>>>>>
>>>>>>> int main() {
>>>>>>> if (T(&Strachey_P)) Output("Halts");
>>>>>>> else Output ("Does not halt");}
>>>>>>>
>>>>>>> Without the definition of T this is just boiler plate.
>>>>>>
>>>>>> Yours is incorrect:
>>>>>
>>>>> How? I assume C89.
>>>>
>>>> typedef void (*ptr)();
>>>>
>>>> int Strachey_P2(void) {
>>>> if (T(&Strachey_P2)) return 1;
>>>> else return 0; }
>>>>
>>>> int main()
>>>> {
>>>> if (T(Strachey_P2)) OutputString("Halts\n");
>>>> else OutputString("Does not halt\n");
>>>> }
>>>>
>>>> _Strachey_P2()
>>>> [0000134e](01) 55 push ebp
>>>> [0000134f](02) 8bec mov ebp,esp
>>>> [00001351](05) 684e130000 push 0000134e
>>>> [00001356](05) e893fbffff call 00000eee
>>>> [0000135b](03) 83c404 add esp,+04
>>>> [0000135e](02) 85c0 test eax,eax
>>>> [00001360](02) 7409 jz 0000136b
>>>> [00001362](05) b801000000 mov eax,00000001
>>>> [00001367](02) eb04 jmp 0000136d
>>>> [00001369](02) eb02 jmp 0000136d
>>>> [0000136b](02) 33c0 xor eax,eax
>>>> [0000136d](01) 5d pop ebp
>>>> [0000136e](01) c3 ret
>>>> Size in bytes:(0033) [0000136e]
>>>>
>>>> _main()
>>>> [0000137e](01) 55 push ebp
>>>> [0000137f](02) 8bec mov ebp,esp
>>>> [00001381](05) 684e130000 push 0000134e
>>>> [00001386](05) e863fbffff call 00000eee
>>>> [0000138b](03) 83c404 add esp,+04
>>>> [0000138e](02) 85c0 test eax,eax
>>>> [00001390](02) 740f jz 000013a1
>>>> [00001392](05) 6817050000 push 00000517
>>>> [00001397](05) e8c2f1ffff call 0000055e
>>>> [0000139c](03) 83c404 add esp,+04
>>>> [0000139f](02) eb0d jmp 000013ae
>>>> [000013a1](05) 681f050000 push 0000051f
>>>> [000013a6](05) e8b3f1ffff call 0000055e
>>>> [000013ab](03) 83c404 add esp,+04
>>>> [000013ae](02) 33c0 xor eax,eax
>>>> [000013b0](01) 5d pop ebp
>>>> [000013b1](01) c3 ret
>>>> Size in bytes:(0052) [000013b1]
>>>>
>>>> machine stack stack machine assembly
>>>> address address data code language
>>>> ======== ======== ======== ========= =============
>>>> [0000137e][001022be][00000000] 55 push ebp
>>>> [0000137f][001022be][00000000] 8bec mov ebp,esp
>>>> [00001381][001022ba][0000134e] 684e130000 push 0000134e
>>>> [00001386][001022b6][0000138b] e863fbffff call 00000eee
>>>>
>>>> T: Begin Simulation Execution Trace Stored at:11236a
>>>> Address_of_T:eee
>>>> [0000134e][0011235a][0011235e] 55 push ebp
>>>> [0000134f][0011235a][0011235e] 8bec mov ebp,esp
>>>> [00001351][00112356][0000134e] 684e130000 push 0000134e
>>>> [00001356][00112352][0000135b] e893fbffff call 00000eee
>>>> T: Infinitely Recursive Simulation Detected Simulation Stopped
>>>>
>>>> [0000138b][001022be][00000000] 83c404 add esp,+04
>>>> [0000138e][001022be][00000000] 85c0 test eax,eax
>>>> [00001390][001022be][00000000] 740f jz 000013a1
>>>> [000013a1][001022ba][0000051f] 681f050000 push 0000051f
>>>> [000013a6][001022ba][0000051f] e8b3f1ffff call 0000055e
>>>> Does not halt
>>>> [000013ab][001022be][00000000] 83c404 add esp,+04
>>>> [000013ae][001022be][00000000] 33c0 xor eax,eax
>>>> [000013b0][001022c2][00000018] 5d pop ebp
>>>> [000013b1][001022c6][00000000] c3 ret
>>>> Number of Instructions Executed(539) == 8 Pages
>>
>> As nearly as I can tell this is all what I called boilerplate.
>> Essentially
>> no substantial content.
>>
>> If you have a computer program that shows what you claim show
>> your complete code and we can check its validity. No programmer
>> is competent to pass a definitive judgement baout his own work.
>
> The above execution trace of simulating halt decider T(Strachey_P2)
> proves that T correctly predicts that its correct and complete x86
> emulation of its input would never reach the "ret" instruction of this
> input. This allows T to correctly reject Strachey_P2 as non-halting.
>
> Anyone having these required prerequisites can verify the above
> paragraph without seeing the source-code.
>
> To fully understand this paper a software engineer must be an expert in:
> (a) The C programming language.
> (b) The x86 programming language.
> (c) Exactly how C translates into x86 (how C function calls are
> implemented in x86).
> (d) The ability to recognize infinite recursion at the x86 assembly
> language level.
>
> Anyone not having these required prerequisites will not be able to
> verify the above paragraph even after seeing the source-code because
> they will not be able to understand what the halt decider is doing
> unless they know the x86 language quite well.
>
>
>
> The code requires more refactoring before it is clean enough for
> publication.
>
> I updated the original x86 emulator so that
> (1) It compiles under Windows as well as Linux. 16390 source-code lines.
>
> (2) One of its original functions can disassemble or simulate its input
> depending on a boolean flag.
>
> (3) The COFF output of the the Microsoft C compiler can be directly
> executed. (contained in Read_COFF_Object.h). 924 source-code lines.
>
> The x86utm operation system is in x86utm.cpp
> 2038 source-code lines.
>
> The various halt deciders and their sample input is in Halt7.c
> 638 source-code lines.
>
No, your system is broken.
T(x) is shown to either be incorrect in the case of x = Strachey_P2 or
that T isn't actually the claimed pure function.
The likely error is that it does the incorrect assuption that when
Strachey_P2 calls T(&Strachey_P2) that it assumes that this T will not
aborts its own emultion of its input, when it is shown that T will.
Thus, either T is incorrect about the behavior of this T, or T actually
does have different behavior when deciding on this input, and thus is
proved not to be an actual computation aka a Pure Function.
Note, your claim that T(&Strachey_P2) not reflecting the behavior of
Strachey_P2() just shows that something is defined incorrectly, since
that is how YOU have defined Strachey_P2 to ask exactly that question.
Simple inspection sees that this is true, as if we use the knowledge
that T(&Strachey_P2) returns 0 as claimed, and that T is a pure function
so ALWAYS behaves the same for the same input, then Strachey_P2 must
call T(Strachey_P2), get that 0 return, at which point it will return 1.
The ONLY way for Strachey_P2 to be non-halting is if T is non-halting
(easily provable since Strachey_P2 has NO instructions that don't
progress farther except for inside T) and thus for T to say Strachey_P2
is non-halting is to say that in some condition T is non-halting and
thus fails to meet its requirements.
[toc] | [prev] | [next] | [standalone]
| From | olcott <NoOne@NoWhere.com> |
|---|---|
| Date | 2022-07-05 19:50 -0500 |
| Subject | Re: Halting problem proofs refuted on the basis of software engineering [ Curry–Howard correspondence ] |
| Message-ID | <C4qdnTVifMneQVn_nZ2dnUU7_83NnZ2d@giganews.com> |
| In reply to | #3535 |
On 7/5/2022 6:53 PM, Ben Bacarisse wrote: > "dklei...@gmail.com" <dkleinecke@gmail.com> writes: > >> But if you do want to use the Curry-Howard correspondence as a >> proof method you must either reference the formal x86 language >> formulation or yourself supply such a formal language description. > > Goodness, no. He'd have to do a whole lot more than that. It's clear > he has no idea what the Curry-Howard correspondence is about. It's > simply not relevant to "x86 language". > In programming language theory and proof theory, the Curry–Howard correspondence (also known as the Curry–Howard isomorphism or equivalence, or the proofs-as-programs and propositions- or formulae-as-types interpretation) is the direct relationship between computer programs and mathematical proofs. https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence The generic idea that there is an isomorphism between mathematical proofs and computations can be understood in that the initial state of a computation corresponds to the premises of a formal proof. The state transitions of a computation correspond to the inference steps of a formal proof. The final state of a computation correspond to the conclusion of a formal proof. Curry/Howard does not do it exactly this way. The x86 language and its semantics would comprise one example of a formal system of the Olcott/isomorphism. > If anyone can be bothered to show that PO knows nothing about this > subtopic, just ask him: what is the type of the "x86 language" program > that corresponds to the proof he is claiming. > >> Your task would be much easier were you to use C as the formal >> language. And much easier to follow. > > But that's *why* he's not using anything better. Clarity is anathema to > cranks. > -- Copyright 2022 Pete Olcott "Talent hits a target no one else can hit; Genius hits a target no one else can see." Arthur Schopenhauer
[toc] | [prev] | [next] | [standalone]
| From | olcott <NoOne@NoWhere.com> |
|---|---|
| Date | 2022-07-05 21:37 -0500 |
| Subject | Re: Halting problem proofs refuted on the basis of software engineering [ Curry–Howard correspondence ] |
| Message-ID | <cIGdnXBYnKnBaFn_nZ2dnUU7_81g4p2d@giganews.com> |
| In reply to | #3535 |
On 7/5/2022 6:53 PM, Ben Bacarisse wrote: > "dklei...@gmail.com" <dkleinecke@gmail.com> writes: > >> But if you do want to use the Curry-Howard correspondence as a >> proof method you must either reference the formal x86 language >> formulation or yourself supply such a formal language description. > > Goodness, no. He'd have to do a whole lot more than that. It's clear > he has no idea what the Curry-Howard correspondence is about. It's > simply not relevant to "x86 language". > > If anyone can be bothered to show that PO knows nothing about this > subtopic, just ask him: what is the type of the "x86 language" program > that corresponds to the proof he is claiming. > >> Your task would be much easier were you to use C as the formal >> language. And much easier to follow. > > But that's *why* he's not using anything better. Clarity is anathema to > cranks. > Bullshit Ben and you know better: The halt decider must have machine code the human users can see this in C and the assembly language mapping from C to x86 assembly language allows the human users to see what the halt decider is doing and verify that it is correct. *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 -- Copyright 2022 Pete Olcott "Talent hits a target no one else can hit; Genius hits a target no one else can see." Arthur Schopenhauer
[toc] | [prev] | [next] | [standalone]
| From | olcott <NoOne@NoWhere.com> |
|---|---|
| Date | 2022-07-05 07:59 -0500 |
| Message-ID | <r7CdnV4ZIPICqFn_nZ2dnUU7_8zNnZ2d@giganews.com> |
| In reply to | #3513 |
On 7/5/2022 3:53 AM, Mikko wrote: > On 2022-07-04 00:44:23 +0000, olcott said: > >> You can't keep ignoring my paper and claiming that I have not proved >> my point. > > In order to make your proof publishable, you should decrate every sentence > in the proof with the numbers of that sentence or those two sentences from > which the sentence is derived with truth preserving rules. > > Mikko > > The proof is (Curry/Howard Correspondence) between programs and proofs, thus H has an initial state performs a sequence of state transitions and ends in a final state rejecting its input as non-halting. *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 -- -- Copyright 2022 Pete Olcott "Talent hits a target no one else can hit; Genius hits a target no one else can see." Arthur Schopenhauer
[toc] | [prev] | [next] | [standalone]
| From | olcott <NoOne@NoWhere.com> |
|---|---|
| Date | 2022-07-05 08:00 -0500 |
| Message-ID | <r7CdnVkZIPJkqFn_nZ2dnUU7_8xh4p2d@giganews.com> |
| In reply to | #3538 |
On 7/5/2022 7:59 AM, olcott wrote: > On 7/5/2022 3:53 AM, Mikko wrote: >> On 2022-07-04 00:44:23 +0000, olcott said: >> >>> You can't keep ignoring my paper and claiming that I have not proved >>> my point. >> >> In order to make your proof publishable, you should decrate every >> sentence >> in the proof with the numbers of that sentence or those two sentences >> from >> which the sentence is derived with truth preserving rules. >> >> Mikko >> >> > > The proof is (Curry/Howard Correspondence) between programs and proofs, > thus H has an initial state performs a sequence of state transitions and > ends in a final state rejecting its input as non-halting. > > *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 > > 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. -- Copyright 2022 Pete Olcott "Talent hits a target no one else can hit; Genius hits a target no one else can see." Arthur Schopenhauer
[toc] | [prev] | [next] | [standalone]
| From | Richard Damon <Richard@Damon-Family.org> |
|---|---|
| Date | 2022-07-05 19:31 -0400 |
| Message-ID | <fR3xK.19680$BZ1.11971@fx03.iad> |
| In reply to | #3538 |
On 7/5/22 8:59 AM, olcott wrote: > On 7/5/2022 3:53 AM, Mikko wrote: >> On 2022-07-04 00:44:23 +0000, olcott said: >> >>> You can't keep ignoring my paper and claiming that I have not proved >>> my point. >> >> In order to make your proof publishable, you should decrate every >> sentence >> in the proof with the numbers of that sentence or those two sentences >> from >> which the sentence is derived with truth preserving rules. >> >> Mikko >> >> > > The proof is (Curry/Howard Correspondence) between programs and proofs, > thus H has an initial state performs a sequence of state transitions and > ends in a final state rejecting its input as non-halting. > > *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 > > Curry-Hooward would say that P(P) is proved to be Halting (if H(P,P) returns 0), so H(P,P) returning 0 can't be the correct answer for a Halting decider. If you want to try to claim that the input to H(P,P) doesn't represent P(P), then your P is written incorrectly, so your "proof" is still invalid.
[toc] | [prev] | [next] | [standalone]
Page 2 of 3 — ← Prev page 1 [2] 3 Next page →
Back to top | Article view | comp.software-eng
csiph-web