Halting problem proofs refuted on the basis of software engineering
1 view
Skip to first unread message
olcott
Jul 2, 2022, 11:34:42 AM7/2/22
to
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
--
Copyright 2022 Pete Olcott
"Talent hits a target no one else can hit;
Genius hits a target no one else can see."
Arthur Schopenhauer
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
--
Copyright 2022 Pete Olcott
"Talent hits a target no one else can hit;
Genius hits a target no one else can see."
Arthur Schopenhauer
Mr Flibble
Jul 2, 2022, 12:26:40 PM7/2/22
to
{
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
olcott
Jul 2, 2022, 12:42:56 PM7/2/22
to
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));
}
[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
olcott
Jul 2, 2022, 1:16:06 PM7/2/22
to
On 7/2/2022 12:10 PM, Mr Flibble wrote:
> 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)
H0 correctly determines that Infinite_Loop() never halts
H correctly determines that Infinite_Recursion() never halts
H correctly determines that P() never halts
*This is necessarily true thus impossibly false*
Every simulating halt decider that correctly simulates its input until
it correctly determines that this simulated input would never reach its
final state, correctly rejects this 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
--
> 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)
H0 correctly determines that Infinite_Loop() never halts
H correctly determines that Infinite_Recursion() never halts
H correctly determines that P() never halts
Every simulating halt decider that correctly simulates its input until
it correctly determines that this simulated input would never reach its
final state, correctly rejects this 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
Mr Flibble
Jul 2, 2022, 1:26:50 PM7/2/22
to
On Sat, 2 Jul 2022 12:15:58 -0500
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
wrong for Px() which is not a pathological input. Px() halts.
/Flibble
olcott
Jul 2, 2022, 1:30:11 PM7/2/22
to
correct x86 emulation of its input would never reach the "ret"
instruction of this input because of the pathological relationship
between H and Px.
Mr Flibble
Jul 2, 2022, 2:28:45 PM7/2/22
to
On Sat, 2 Jul 2022 12:30:03 -0500
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
problem and [Strachey 1965] as it does not try to do the opposite of
what H decides.
/Flibble
olcott
Jul 2, 2022, 2:41:22 PM7/2/22
to
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
Mr Flibble
Jul 2, 2022, 2:44:46 PM7/2/22
to
On Sat, 2 Jul 2022 13:41:14 -0500
[snip]
P does but Px does not. I am talking about Px not P.
P does but Px does not. I am talking about Px not P.
olcott
Jul 2, 2022, 5:26:53 PM7/2/22
to
Mr Flibble
Jul 2, 2022, 6:05:34 PM7/2/22
to
On Sat, 2 Jul 2022 16:26:45 -0500
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
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
olcott
Jul 2, 2022, 6:13:08 PM7/2/22
to
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.
Mr Flibble
Jul 3, 2022, 10:27:47 AM7/3/22
to
On Sat, 2 Jul 2022 17:13:01 -0500
Your H does not "correctly predict" that Px() does reach its final
state and so should accept the input as halting.
/Flibble
state and so should accept the input as halting.
/Flibble
olcott
Jul 3, 2022, 10:58:06 AM7/3/22
to
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.
Mr Flibble
Jul 3, 2022, 11:21:44 AM7/3/22
to
On Sun, 3 Jul 2022 09:57:57 -0500
Not EVERY simulating halt decider, only YOURS gets the answer wrong.
Px() halts.
/Flibble
Px() halts.
/Flibble
olcott
Jul 3, 2022, 11:30:54 AM7/3/22
to
incompetent.
Mr Flibble
Jul 3, 2022, 11:45:40 AM7/3/22
to
On Sun, 3 Jul 2022 10:30:45 -0500
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
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
olcott
Jul 3, 2022, 11:48:27 AM7/3/22
to
in infinite recursion is not allowed to return to its caller.
Mr Flibble
Jul 3, 2022, 11:51:07 AM7/3/22
to
On Sun, 3 Jul 2022 10:48:18 -0500
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 problem; there is no infinite recursion in [Strachey 1965] and
associated proofs.
/Flibble
olcott
Jul 3, 2022, 12:05:30 PM7/3/22
to
long as it correctly predicts the behavior of the input.
*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.
*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
https://www.researchgate.net/publication/361701808_Halting_problem_proofs_refuted_on_the_basis_of_software_engineering
Mr Flibble
Jul 3, 2022, 12:07:03 PM7/3/22
to
On Sun, 3 Jul 2022 11:05:21 -0500
Your H does not correctly predict the behavior of Px() as Px() always
halts yet your H incorrectly says it doesn't.
/Flibble
halts yet your H incorrectly says it doesn't.
/Flibble
olcott
Jul 4, 2022, 12:57:28 PM7/4/22
to
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:
>>>>> 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.
> 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.
> 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
>>>>>>
>>>>>> *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.
>>>>>>
>>>>> 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
>>
>> https://www.researchgate.net/publication/361701808_Halting_problem_proofs_refuted_on_the_basis_of_software_engineering
>>
> 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.
olcott
Jul 4, 2022, 3:17:38 PM7/4/22
to
On 7/4/2022 1:42 PM, dklei...@gmail.com wrote:
> 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
> 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
olcott
Jul 4, 2022, 3:21:29 PM7/4/22
to
olcott
Jul 4, 2022, 7:08:12 PM7/4/22
to
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 Monday, July 4, 2022 at 9:57:28 AM UTC-7, olcott wrote:
> 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*
> 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.
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.
olcott
Jul 5, 2022, 8:59:19 AM7/5/22
to
On 7/5/2022 3:53 AM, Mikko wrote:
> 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.
> 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
>
>> You can't keep ignoring my paper and claiming that I have not proved
>> my point.
>
> 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.
olcott
Jul 5, 2022, 9:00:49 AM7/5/22
to
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
>
>
> 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.
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.
olcott
Jul 5, 2022, 3:31:47 PM7/5/22
to
On 7/5/2022 1:50 PM, dklei...@gmail.com wrote:
> 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]
> 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;
}
[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]
olcott
Jul 5, 2022, 4:42:34 PM7/5/22
to
On 7/5/2022 3:24 PM, André G. Isaak wrote:
> On 2022-07-05 12:50, dklei...@gmail.com wrote:
> 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.
The start state, state transitions inbetween and the final state of a
computation can be construed as a formal proof from premises to conclusion.
> On 2022-07-05 12:50, dklei...@gmail.com wrote:
>> 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.
>>
>> 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,
>> language. And much easier to follow.
>
> 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*
https://www.researchgate.net/publication/361701808_Halting_problem_proofs_refuted_on_the_basis_of_software_engineering
The start state, state transitions inbetween and the final state of a
computation can be construed as a formal proof from premises to conclusion.
Richard Damon
Jul 5, 2022, 7:29:29 PM7/5/22
to
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".
Richard Damon
Jul 5, 2022, 7:31:26 PM7/5/22
to
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)
> 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
>
>
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.
olcott
Jul 5, 2022, 8:01:17 PM7/5/22
to
On 7/5/2022 6:53 PM, Ben Bacarisse wrote:
> 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.
> 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.
> "dklei...@gmail.com" <dklei...@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
>
>> 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.
>
> 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
>> Your task would be much easier were you to use C as the formal
>> language. And much easier to follow.
>
> 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.
olcott
Jul 5, 2022, 8:50:18 PM7/5/22
to
On 7/5/2022 6:53 PM, Ben Bacarisse wrote:
> "dklei...@gmail.com" <dklei...@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".
>
> "dklei...@gmail.com" <dklei...@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
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
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.
>
olcott
Jul 5, 2022, 10:37:23 PM7/5/22