1 view

Skip to first unread message

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

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

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

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

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

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.

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

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

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.

Jul 2, 2022, 5:26:53 PM7/2/22

to

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

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.

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

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.

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

Jul 3, 2022, 11:30:54 AM7/3/22

to

incompetent.

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

Jul 3, 2022, 11:48:27 AM7/3/22

to

in infinite recursion is not allowed to return to its caller.

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

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

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

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.

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

Jul 4, 2022, 3:21:29 PM7/4/22

to

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.

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.

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.

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]

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.

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".

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.

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.

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.

>

Jul 5, 2022, 10:37:23 PM7/5/22