On Monday, July 4, 2022 at 9:57:28 AM UTC-7, olcott wrote:
On 7/4/2022 11:36 AM, [email protected] wrote:There is a great deal more to a mathematical proof than a formal
On Sunday, July 3, 2022 at 5:44:32 PM UTC-7, olcott wrote:
On 7/3/2022 6:10 PM, [email protected] wrote:Your paper is not acceptable as a proof of anything. But that is to
On Sunday, July 3, 2022 at 12:51:41 PM UTC-7, olcott wrote:
On 7/3/2022 2:35 PM, [email protected] wrote:It might if any such halt deciders existed. You need to prove such "halt >>>>> deciders" exist.
On Sunday, July 3, 2022 at 9:05:30 AM UTC-7, olcott wrote:
This "general principle is" a trivial definition: A simulation of a >>>>>>> called routine that stops when it can predict that the routine
*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.
will never return is called a halt decider.
In words of one syllable - so what?
It refutes conventional halting problem proofs
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
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:
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.
On Monday, July 4, 2022 at 4:08:12 PM UTC-7, olcott wrote:
On 7/4/2022 1:42 PM, [email protected] wrote:
On Monday, July 4, 2022 at 9:57:28 AM UTC-7, olcott wrote:It would seem that *Curry–Howard correspondence*
On 7/4/2022 11:36 AM, [email protected] wrote:There is a great deal more to a mathematical proof than a formal
On Sunday, July 3, 2022 at 5:44:32 PM UTC-7, olcott wrote:
On 7/3/2022 6:10 PM, [email protected] wrote:Your paper is not acceptable as a proof of anything. But that is to
On Sunday, July 3, 2022 at 12:51:41 PM UTC-7, olcott wrote:
On 7/3/2022 2:35 PM, [email protected] wrote:It might if any such halt deciders existed. You need to prove such "halt
On Sunday, July 3, 2022 at 9:05:30 AM UTC-7, olcott wrote:
This "general principle is" a trivial definition: A simulation of a >>>>>>>>> called routine that stops when it can predict that the routine >>>>>>>>> will never return is called a halt decider.
*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.
In words of one syllable - so what?
It refutes conventional halting problem proofs
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
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: >>>>
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.
I am afraid you don't see mathematical proof like a mathematician
might. A good and simple example is the theorem that proves all
Burnside three groups are finite.
But if you do want to use the Curry-Howard correspondence as a
proof method you must either reference the formal x86 language
formulation or yourself supply such a formal language description.
Your task would be much easier were you to use C as the formal
language. And much easier to follow.
On 2022-07-05 12:50, [email protected] wrote:
On Monday, July 4, 2022 at 4:08:12 PM UTC-7, olcott wrote:
On 7/4/2022 1:42 PM, [email protected] wrote:
On Monday, July 4, 2022 at 9:57:28 AM UTC-7, olcott wrote:It would seem that *Curry–Howard correspondence*
On 7/4/2022 11:36 AM, [email protected] wrote:There is a great deal more to a mathematical proof than a formal
On Sunday, July 3, 2022 at 5:44:32 PM UTC-7, olcott wrote:
On 7/3/2022 6:10 PM, [email protected] wrote:Your paper is not acceptable as a proof of anything. But that is to >>>>>> be expected because my standard is mathematical proof and
On Sunday, July 3, 2022 at 12:51:41 PM UTC-7, olcott wrote:
On 7/3/2022 2:35 PM, [email protected] wrote:It might if any such halt deciders existed. You need to prove
On Sunday, July 3, 2022 at 9:05:30 AM UTC-7, olcott wrote: >>>>>>>>>>>
*This general principle refutes conventional halting problem >>>>>>>>>>> proofs*This "general principle is" a trivial definition: A simulation >>>>>>>>>> of a
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
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
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:
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.
I am afraid you don't see mathematical proof like a mathematician
might. A good and simple example is the theorem that proves all
Burnside three groups are finite.
But if you do want to use the Curry-Howard correspondence as a
proof method you must either reference the formal x86 language
formulation or yourself supply such a formal language description.
Your task would be much easier were you to use C as the formal
language. And much easier to follow.
If he really wants to use (and if he actually understood) Curry-Howard,
he'd be better off using Scheme or Haskell or something like that...
But it wouldn't make a difference. He has not provided an actual proof
NOR an actual program, so talking about some alleged correspondence
between two imaginary entities is hardly going to enlighten anyone.
André
On 7/5/2022 3:24 PM, André G. Isaak wrote:
On 2022-07-05 12:50, [email protected] wrote:
On Monday, July 4, 2022 at 4:08:12 PM UTC-7, olcott wrote:
On 7/4/2022 1:42 PM, [email protected] wrote:
On Monday, July 4, 2022 at 9:57:28 AM UTC-7, olcott wrote:It would seem that *Curry–Howard correspondence*
On 7/4/2022 11:36 AM, [email protected] wrote:There is a great deal more to a mathematical proof than a formal
On Sunday, July 3, 2022 at 5:44:32 PM UTC-7, olcott wrote:
On 7/3/2022 6:10 PM, [email protected] wrote:Your paper is not acceptable as a proof of anything. But that is to >>>>>>> be expected because my standard is mathematical proof and
On Sunday, July 3, 2022 at 12:51:41 PM UTC-7, olcott wrote: >>>>>>>>>> On 7/3/2022 2:35 PM, [email protected] wrote:
It might if any such halt deciders existed. You need to prove >>>>>>>>> such "haltOn Sunday, July 3, 2022 at 9:05:30 AM UTC-7, olcott wrote: >>>>>>>>>>>>
*This general principle refutes conventional halting problem >>>>>>>>>>>> proofs*This "general principle is" a trivial definition: A
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. >>>>>>>>>>>>
simulation of a
called routine that stops when it can predict that the routine >>>>>>>>>>> will never return is called a halt decider.
In words of one syllable - so what?
It refutes conventional halting problem proofs
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
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:
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.
I am afraid you don't see mathematical proof like a mathematician
might. A good and simple example is the theorem that proves all
Burnside three groups are finite.
But if you do want to use the Curry-Howard correspondence as a
proof method you must either reference the formal x86 language
formulation or yourself supply such a formal language description.
Your task would be much easier were you to use C as the formal
language. And much easier to follow.
If he really wants to use (and if he actually understood)
Curry-Howard, he'd be better off using Scheme or Haskell or something
like that...
But it wouldn't make a difference. He has not provided an actual proof
NOR an actual program, so talking about some alleged correspondence
between two imaginary entities is hardly going to enlighten anyone.
André
Welcome back you are one of my competent reviewers.
*My most recent paper provides complete proof of this*
From a purely software engineering perspective (anchored in the
semantics of the x86 language) it is proven that H(P,P) correctly
predicts that its correct and complete x86 emulation of its input would
never reach the "ret" instruction (final state) of this input.
*Halting problem proofs refuted on the basis of software engineering* https://www.researchgate.net/publication/361701808_Halting_problem_proofs_refuted_on_the_basis_of_software_engineering
*Only to those having the required software engineering prerequisites*
The start state, state transitions inbetween and the final state of a computation can be construed as a formal proof from premises to conclusion.
"[email protected]" <[email protected]> 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.
"[email protected]" <[email protected]> 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.
"[email protected]" <[email protected]> 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.
On Tuesday, July 5, 2022 at 9:02:28 PM UTC-7, olcott wrote:
On 7/5/2022 11:00 PM, [email protected] wrote:I know what a directed graph is and I don't see why you mention them.
On Tuesday, July 5, 2022 at 5:01:17 PM UTC-7, olcott wrote:
Why? What is impossible to do in C?
The halt decider must have machine code
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?
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 Thursday, July 7, 2022 at 12:39:41 PM UTC-7, olcott wrote:
On 7/7/2022 2:19 PM, [email protected] wrote:
On Wednesday, July 6, 2022 at 2:13:47 PM UTC-7, olcott wrote:*I will repeat this point several times because you keep not getting it*
On 7/6/2022 3:58 PM, [email protected] wrote:
On Tuesday, July 5, 2022 at 9:02:28 PM UTC-7, olcott wrote: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
On 7/5/2022 11:00 PM, [email protected] wrote:I know what a directed graph is and I don't see why you mention them. >>>>>
On Tuesday, July 5, 2022 at 5:01:17 PM UTC-7, olcott wrote:
Why? What is impossible to do in C?
The halt decider must have machine code
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?
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.
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.
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 Thursday, July 7, 2022 at 2:08:19 PM UTC-7, olcott wrote:
On 7/7/2022 3:54 PM, [email protected] wrote:. . .
On Thursday, July 7, 2022 at 12:39:41 PM UTC-7, olcott wrote:
On 7/7/2022 2:19 PM, [email protected] 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.
Formal language is very different than natural language. But the
So what matters is humans reading formal languages.What are the properties of a formal language that distinguish it from a
natural language?
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 Thursday, July 7, 2022 at 6:34:32 PM UTC-7, olcott wrote:
On 7/7/2022 7:36 PM, [email protected] wrote:int Strachey_P(void) {
On Thursday, July 7, 2022 at 2:08:19 PM UTC-7, olcott wrote:Then we have disagreements that are entirely based on interpreting the
On 7/7/2022 3:54 PM, [email protected] wrote:. . .
On Thursday, July 7, 2022 at 12:39:41 PM UTC-7, olcott wrote:
On 7/7/2022 2:19 PM, [email protected] 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.
vagueness differently.
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.
| Sysop: | Keyop |
|---|---|
| Location: | Huddersfield, West Yorkshire, UK |
| Users: | 715 |
| Nodes: | 16 (3 / 13) |
| Uptime: | 146:26:22 |
| Calls: | 12,091 |
| Calls today: | 4 |
| Files: | 15,000 |
| Messages: | 6,517,503 |