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.

On 7/5/2022 6:21 PM, dklei...@gmail.com wrote:
> On Tuesday, July 5, 2022 at 12:31:47 PM UTC-7, olcott wrote:
>> On 7/5/2022 1:50 PM, dklei...@gmail.com wrote:
>>>
>>> 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/
> .>
> We have been here before. A list of op-codes is not a formal language
> description.

Read the rest of the 500 pages.

>>
>>> 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.
>>
> You don't need to compile. The readers whom you want to convince can
> read and follow C. That's the level mathematics is done at.

The halt decider itself must have machine code.

>>
>> 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.
> .>
> Nobody cares about that "bijection" and messing with it wastes everybody's
> time.

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

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

--
Ben.

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

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

On 7/5/22 7:37 PM, olcott wrote:
> On 7/5/2022 6:21 PM, dklei...@gmail.com wrote:
>> On Tuesday, July 5, 2022 at 12:31:47 PM UTC-7, olcott wrote:
>>> On 7/5/2022 1:50 PM, dklei...@gmail.com wrote:
>>>>
>>>> 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/
>> .>
>> We have been here before. A list of op-codes is not a formal language
>> description.
>
>
> Read the rest of the 500 pages.
>
>>>
>>>> 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.
>>>
>> You don't need to compile. The readers whom you want to convince can
>> read and follow C. That's the level mathematics is done at.
>
> The halt decider itself must have machine code.

Yes, and that machine code becomes PART of the program P, so H needs to
handle the actual behavor of that code.

THus, if H(P,P) returns 0 when called by main, it will also return 0
when called by P, and thus when H emulates P(P), it needs to emulate the
call to H(P,P) as something that returns 0.

Your claim that it is somehow different violates your claim that H is a
pure function of its input actually implemented in x86 assembly code.

>
>>>
>>> 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.
>> .>
>> Nobody cares about that "bijection" and messing with it wastes
>> everybody's
>> time.
>
> 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.
>

Right, we can verify that since H(P,P) returns 0 to main, it also
returns 0 to P(P), and your arguement is proven incorrect because it
assumes that H does two different things given the same input which is a
logical imposibility given that it is claimed to be a pure function.

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

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?

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

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

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

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.

You don't seem to understand that a proof is not an executing program.
There is never a reason to compile. The reader can follow along in the C
and accept or reject the proof. That's the mathematical way.

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

> You don't seem to understand that a proof is not an executing program.
> There is never a reason to compile. The reader can follow along in the C
> and accept or reject the proof. That's the mathematical 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

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.
So what matters is humans reading formal languages.

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.

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

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

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

On 7/7/22 3:39 PM, 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

You only think this because you don't really understand what you can do
in assembly.

>
>> You don't seem to understand that a proof is not an executing program.
>> There is never a reason to compile. The reader can follow along in the C
>> and accept or reject the proof. That's the mathematical way.
>
>

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.

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

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.

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.

Where is the infinite loop?

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

On Friday, July 8, 2022 at 5:54:51 AM UTC-7, 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.
>
> Where is the infinite loop?
>
I took it out. There was never any point to it anyway. But easy
to put back. Just replace the "return 1" with an
infinite loop. But why bother.

On 7/8/2022 12:59 PM, dklei...@gmail.com wrote:
> On Friday, July 8, 2022 at 5:54:51 AM UTC-7, 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.
>>
>> Where is the infinite loop?
>>
> I took it out. There was never any point to it anyway. But easy
> to put back. Just replace the "return 1" with an
> infinite loop. But why bother.

If you change Strachey then we are no longer talking about Strachey.
I proved that the original Strachey is non-halting.

--
Copyright 2022 Pete Olcott

"Talent hits a target no one else can hit;
Genius hits a target no one else can see."
Arthur Schopenhauer

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

--
Copyright 2022 Pete Olcott

"Talent hits a target no one else can hit;
Genius hits a target no one else can see."
Arthur Schopenhauer

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
>

*THIS IS IRREFUTABLY CORRECT*
From a purely software engineering perspective T(Strachey_P) does
correctly predict that its complete and correct x86 emulation of its
input would never reach the "ret" instruction (final state) of this
input, therefore T(Strachey_P) correctly rejects this input as non-halting.

--
Copyright 2022 Pete Olcott

"Talent hits a target no one else can hit;
Genius hits a target no one else can see."
Arthur Schopenhauer