Proving an algorithm is correct necessitates a stratified type system
which recognises a category error present in extant halting problem proofs (self referential conflation of a decider with its input); the halting problem as currently defined is only appropriate for untyped systems, it needs to be constrained to a typed system and when it is all extant
halting problem proofs relying on diagonalization are rendered moot.
The two types of programs are:
(A) halt deciders;
(B) programs being proven by the decider.
Type constraints:
(B) cannot encode (A) due to uni-directionality.
If (B) is a subset of (A) and cannot use (without violating type
constraints) a possibly modified copy of (A) (as done in the
diagonalization proofs) then a new research avenue in the area of
algorithm analysis and program correctness is opened up, uninhibited by
the traditional blocker namely Turing's Halting Problem.
/Flibble
On 8/1/25 8:40 AM, Mr Flibble wrote:
Proving an algorithm is correct necessitates a stratified type system
which recognises a category error present in extant halting problem
proofs (self referential conflation of a decider with its input); the
halting problem as currently defined is only appropriate for untyped
systems, it needs to be constrained to a typed system and when it is
all extant halting problem proofs relying on diagonalization are
rendered moot.
The two types of programs are:
(A) halt deciders;
(B) programs being proven by the decider.
Type constraints:
(B) cannot encode (A) due to uni-directionality.
If (B) is a subset of (A) and cannot use (without violating type
constraints) a possibly modified copy of (A) (as done in the
diagonalization proofs) then a new research avenue in the area of
algorithm analysis and program correctness is opened up, uninhibited by
the traditional blocker namely Turing's Halting Problem.
/Flibble
And the assumption that proof of "correctness" is a necessity, or
requrement of the system is an error.
It is provable that more "problems" exist to try to answer, then there
are programs to try to answer them, and thus, there must exist problems
that can't be answered by a program.
The problem with your definitions, is you can't determine if some chunk
of code IS part of (A), and thus your system can't be used.
On 8/1/25 10:08 AM, Mr Flibble wrote:
On Fri, 01 Aug 2025 10:01:10 -0400, Richard Damon wrote:
On 8/1/25 8:40 AM, Mr Flibble wrote:
Proving an algorithm is correct necessitates a stratified type system
which recognises a category error present in extant halting problem
proofs (self referential conflation of a decider with its input); the
halting problem as currently defined is only appropriate for untyped
systems, it needs to be constrained to a typed system and when it is
all extant halting problem proofs relying on diagonalization are
rendered moot.
The two types of programs are:
(A) halt deciders;
(B) programs being proven by the decider.
Type constraints:
(B) cannot encode (A) due to uni-directionality.
If (B) is a subset of (A) and cannot use (without violating type
constraints) a possibly modified copy of (A) (as done in the
diagonalization proofs) then a new research avenue in the area of
algorithm analysis and program correctness is opened up, uninhibited
by the traditional blocker namely Turing's Halting Problem.
/Flibble
And the assumption that proof of "correctness" is a necessity, or
requrement of the system is an error.
It is provable that more "problems" exist to try to answer, then there
are programs to try to answer them, and thus, there must exist
problems that can't be answered by a program.
The problem with your definitions, is you can't determine if some
chunk of code IS part of (A), and thus your system can't be used.
I could quite easily design a program verification system which has the
type stratification I propose allowing the type constraint I have
defined to be enforced. My universal compiler framework (neos) could
easily achieve this even if the decider and the input are IN THE SAME
SOURCE CODE FILE.
https://neos.dev
/Flibble
Go ahead, TRY to write a program to determine if a given input is a
"Halt Decider".
That has been proven to be impossible.
On Fri, 01 Aug 2025 10:01:10 -0400, Richard Damon wrote:
On 8/1/25 8:40 AM, Mr Flibble wrote:
Proving an algorithm is correct necessitates a stratified type system
which recognises a category error present in extant halting problem
proofs (self referential conflation of a decider with its input); the
halting problem as currently defined is only appropriate for untyped
systems, it needs to be constrained to a typed system and when it is
all extant halting problem proofs relying on diagonalization are
rendered moot.
The two types of programs are:
(A) halt deciders;
(B) programs being proven by the decider.
Type constraints:
(B) cannot encode (A) due to uni-directionality.
If (B) is a subset of (A) and cannot use (without violating type
constraints) a possibly modified copy of (A) (as done in the
diagonalization proofs) then a new research avenue in the area of
algorithm analysis and program correctness is opened up, uninhibited by
the traditional blocker namely Turing's Halting Problem.
/Flibble
And the assumption that proof of "correctness" is a necessity, or
requrement of the system is an error.
It is provable that more "problems" exist to try to answer, then there
are programs to try to answer them, and thus, there must exist problems
that can't be answered by a program.
The problem with your definitions, is you can't determine if some chunk
of code IS part of (A), and thus your system can't be used.
I could quite easily design a program verification system which has the
type stratification I propose allowing the type constraint I have defined
to be enforced. My universal compiler framework (neos) could easily
achieve this even if the decider and the input are IN THE SAME SOURCE CODE FILE.
https://neos.dev
/Flibble
On Fri, 01 Aug 2025 10:01:10 -0400, Richard Damon wrote:
On 8/1/25 8:40 AM, Mr Flibble wrote:
Proving an algorithm is correct necessitates a stratified type system
which recognises a category error present in extant halting problem
proofs (self referential conflation of a decider with its input); the
halting problem as currently defined is only appropriate for untyped
systems, it needs to be constrained to a typed system and when it is
all extant halting problem proofs relying on diagonalization are
rendered moot.
The two types of programs are:
(A) halt deciders;
(B) programs being proven by the decider.
Type constraints:
(B) cannot encode (A) due to uni-directionality.
If (B) is a subset of (A) and cannot use (without violating type
constraints) a possibly modified copy of (A) (as done in the
diagonalization proofs) then a new research avenue in the area of
algorithm analysis and program correctness is opened up, uninhibited by
the traditional blocker namely Turing's Halting Problem.
/Flibble
And the assumption that proof of "correctness" is a necessity, or
requrement of the system is an error.
It is provable that more "problems" exist to try to answer, then there
are programs to try to answer them, and thus, there must exist problems
that can't be answered by a program.
The problem with your definitions, is you can't determine if some chunk
of code IS part of (A), and thus your system can't be used.
I could quite easily design a program verification system which has the
type stratification I propose allowing the type constraint I have defined
to be enforced. My universal compiler framework (neos) could easily
achieve this even if the decider and the input are IN THE SAME SOURCE CODE FILE.
https://neos.dev
/Flibble
On Fri, 01 Aug 2025 10:22:11 -0400, Richard Damon wrote:
On 8/1/25 10:08 AM, Mr Flibble wrote:
On Fri, 01 Aug 2025 10:01:10 -0400, Richard Damon wrote:
On 8/1/25 8:40 AM, Mr Flibble wrote:
Proving an algorithm is correct necessitates a stratified type system >>>>> which recognises a category error present in extant halting problem
proofs (self referential conflation of a decider with its input); the >>>>> halting problem as currently defined is only appropriate for untyped >>>>> systems, it needs to be constrained to a typed system and when it is >>>>> all extant halting problem proofs relying on diagonalization are
rendered moot.
The two types of programs are:
(A) halt deciders;
(B) programs being proven by the decider.
Type constraints:
(B) cannot encode (A) due to uni-directionality.
If (B) is a subset of (A) and cannot use (without violating type
constraints) a possibly modified copy of (A) (as done in the
diagonalization proofs) then a new research avenue in the area of
algorithm analysis and program correctness is opened up, uninhibited >>>>> by the traditional blocker namely Turing's Halting Problem.
/Flibble
And the assumption that proof of "correctness" is a necessity, or
requrement of the system is an error.
It is provable that more "problems" exist to try to answer, then there >>>> are programs to try to answer them, and thus, there must exist
problems that can't be answered by a program.
The problem with your definitions, is you can't determine if some
chunk of code IS part of (A), and thus your system can't be used.
I could quite easily design a program verification system which has the
type stratification I propose allowing the type constraint I have
defined to be enforced. My universal compiler framework (neos) could
easily achieve this even if the decider and the input are IN THE SAME
SOURCE CODE FILE.
https://neos.dev
/Flibble
Go ahead, TRY to write a program to determine if a given input is a
"Halt Decider".
That has been proven to be impossible.
Impossible? Partial deciders are a thing, dear, and certainly not "impossible".
/Flibble
On 8/1/25 10:08 AM, Mr Flibble wrote:
On Fri, 01 Aug 2025 10:01:10 -0400, Richard Damon wrote:
On 8/1/25 8:40 AM, Mr Flibble wrote:
Proving an algorithm is correct necessitates a stratified type system
which recognises a category error present in extant halting problem
proofs (self referential conflation of a decider with its input); the
halting problem as currently defined is only appropriate for untyped
systems, it needs to be constrained to a typed system and when it is
all extant halting problem proofs relying on diagonalization are
rendered moot.
The two types of programs are:
(A) halt deciders;
(B) programs being proven by the decider.
Type constraints:
(B) cannot encode (A) due to uni-directionality.
If (B) is a subset of (A) and cannot use (without violating type
constraints) a possibly modified copy of (A) (as done in the
diagonalization proofs) then a new research avenue in the area of
algorithm analysis and program correctness is opened up, uninhibited
by the traditional blocker namely Turing's Halting Problem.
/Flibble
And the assumption that proof of "correctness" is a necessity, or
requrement of the system is an error.
It is provable that more "problems" exist to try to answer, then there
are programs to try to answer them, and thus, there must exist
problems that can't be answered by a program.
The problem with your definitions, is you can't determine if some
chunk of code IS part of (A), and thus your system can't be used.
I could quite easily design a program verification system which has the
type stratification I propose allowing the type constraint I have
defined to be enforced. My universal compiler framework (neos) could
easily achieve this even if the decider and the input are IN THE SAME
SOURCE CODE FILE.
https://neos.dev
/Flibble
Note, if you try do define it by trying to match to one given Halt
decider, then DDD just needs to alter the code of HHH with some
null-effect change that maintains its responses, and thus defeats the categories.
All you are showing is a lack of understanding of the power of computing systems.
On Fri, 01 Aug 2025 10:24:40 -0400, Richard Damon wrote:
On 8/1/25 10:08 AM, Mr Flibble wrote:
On Fri, 01 Aug 2025 10:01:10 -0400, Richard Damon wrote:
On 8/1/25 8:40 AM, Mr Flibble wrote:
Proving an algorithm is correct necessitates a stratified type system >>>>> which recognises a category error present in extant halting problem
proofs (self referential conflation of a decider with its input); the >>>>> halting problem as currently defined is only appropriate for untyped >>>>> systems, it needs to be constrained to a typed system and when it is >>>>> all extant halting problem proofs relying on diagonalization are
rendered moot.
The two types of programs are:
(A) halt deciders;
(B) programs being proven by the decider.
Type constraints:
(B) cannot encode (A) due to uni-directionality.
If (B) is a subset of (A) and cannot use (without violating type
constraints) a possibly modified copy of (A) (as done in the
diagonalization proofs) then a new research avenue in the area of
algorithm analysis and program correctness is opened up, uninhibited >>>>> by the traditional blocker namely Turing's Halting Problem.
/Flibble
And the assumption that proof of "correctness" is a necessity, or
requrement of the system is an error.
It is provable that more "problems" exist to try to answer, then there >>>> are programs to try to answer them, and thus, there must exist
problems that can't be answered by a program.
The problem with your definitions, is you can't determine if some
chunk of code IS part of (A), and thus your system can't be used.
I could quite easily design a program verification system which has the
type stratification I propose allowing the type constraint I have
defined to be enforced. My universal compiler framework (neos) could
easily achieve this even if the decider and the input are IN THE SAME
SOURCE CODE FILE.
https://neos.dev
/Flibble
Note, if you try do define it by trying to match to one given Halt
decider, then DDD just needs to alter the code of HHH with some
null-effect change that maintains its responses, and thus defeats the
categories.
All you are showing is a lack of understanding of the power of computing
systems.
I find it suspicious that you use Olcott's terminology in your reply (DDD
and HHH): your brain might be frazzled or, a more fun thought, you could
be an Olcott sockpuppet. As I don't follow Olcott's work that closely I
am unsure what DDD and HHH refer to, I use H for decider and P for input.
It would be posssible for neos to disallow P from accessing H programmatically, both H's compile time and runtime representations. Enforcing type stratification at a language level would not be a difficult modification to neos.
/Flibble
On 8/1/25 11:08 AM, Mr Flibble wrote:
On Fri, 01 Aug 2025 10:24:40 -0400, Richard Damon wrote:
On 8/1/25 10:08 AM, Mr Flibble wrote:
On Fri, 01 Aug 2025 10:01:10 -0400, Richard Damon wrote:
On 8/1/25 8:40 AM, Mr Flibble wrote:
Proving an algorithm is correct necessitates a stratified type
system which recognises a category error present in extant halting >>>>>> problem proofs (self referential conflation of a decider with its
input); the halting problem as currently defined is only
appropriate for untyped systems, it needs to be constrained to a
typed system and when it is all extant halting problem proofs
relying on diagonalization are rendered moot.
The two types of programs are:
(A) halt deciders;
(B) programs being proven by the decider.
Type constraints:
(B) cannot encode (A) due to uni-directionality.
If (B) is a subset of (A) and cannot use (without violating type
constraints) a possibly modified copy of (A) (as done in the
diagonalization proofs) then a new research avenue in the area of
algorithm analysis and program correctness is opened up,
uninhibited by the traditional blocker namely Turing's Halting
Problem.
/Flibble
And the assumption that proof of "correctness" is a necessity, or
requrement of the system is an error.
It is provable that more "problems" exist to try to answer, then
there are programs to try to answer them, and thus, there must exist >>>>> problems that can't be answered by a program.
The problem with your definitions, is you can't determine if some
chunk of code IS part of (A), and thus your system can't be used.
I could quite easily design a program verification system which has
the type stratification I propose allowing the type constraint I have
defined to be enforced. My universal compiler framework (neos) could
easily achieve this even if the decider and the input are IN THE SAME
SOURCE CODE FILE.
https://neos.dev
/Flibble
Note, if you try do define it by trying to match to one given Halt
decider, then DDD just needs to alter the code of HHH with some
null-effect change that maintains its responses, and thus defeats the
categories.
All you are showing is a lack of understanding of the power of
computing systems.
I find it suspicious that you use Olcott's terminology in your reply
(DDD and HHH): your brain might be frazzled or, a more fun thought, you
could be an Olcott sockpuppet. As I don't follow Olcott's work that
closely I am unsure what DDD and HHH refer to, I use H for decider and
P for input.
It would be posssible for neos to disallow P from accessing H
programmatically, both H's compile time and runtime representations.
Enforcing type stratification at a language level would not be a
difficult modification to neos.
/Flibble
But it can't prevent P from accessing a copy of H, that has had a non-behavior changing modifcation done to it.
Since that modified version of H should still be considered a Halt
Detector, but neos can't determine that, you can't have that as a
category.
This goes to the problem that the final program doesn't include all the meta-information that might have gone into making it.
For instance, I can make a program that by its construction is provably correct, but if I just give you that program and the initial
specification, you might not be able to prove it to be correct.
This is the essence of the incompleteness theorem.
Since you can't detect that a piece of code uses an algorithm that does
"halt detection", you can't make that a category to partion your code
into spaces.
On Fri, 01 Aug 2025 11:16:01 -0400, Richard Damon wrote:
On 8/1/25 11:08 AM, Mr Flibble wrote:
On Fri, 01 Aug 2025 10:24:40 -0400, Richard Damon wrote:
On 8/1/25 10:08 AM, Mr Flibble wrote:
On Fri, 01 Aug 2025 10:01:10 -0400, Richard Damon wrote:
On 8/1/25 8:40 AM, Mr Flibble wrote:
Proving an algorithm is correct necessitates a stratified type
system which recognises a category error present in extant halting >>>>>>> problem proofs (self referential conflation of a decider with its >>>>>>> input); the halting problem as currently defined is only
appropriate for untyped systems, it needs to be constrained to a >>>>>>> typed system and when it is all extant halting problem proofs
relying on diagonalization are rendered moot.
The two types of programs are:
(A) halt deciders;
(B) programs being proven by the decider.
Type constraints:
(B) cannot encode (A) due to uni-directionality.
If (B) is a subset of (A) and cannot use (without violating type >>>>>>> constraints) a possibly modified copy of (A) (as done in the
diagonalization proofs) then a new research avenue in the area of >>>>>>> algorithm analysis and program correctness is opened up,
uninhibited by the traditional blocker namely Turing's Halting
Problem.
/Flibble
And the assumption that proof of "correctness" is a necessity, or
requrement of the system is an error.
It is provable that more "problems" exist to try to answer, then
there are programs to try to answer them, and thus, there must exist >>>>>> problems that can't be answered by a program.
The problem with your definitions, is you can't determine if some
chunk of code IS part of (A), and thus your system can't be used.
I could quite easily design a program verification system which has
the type stratification I propose allowing the type constraint I have >>>>> defined to be enforced. My universal compiler framework (neos) could >>>>> easily achieve this even if the decider and the input are IN THE SAME >>>>> SOURCE CODE FILE.
https://neos.dev
/Flibble
Note, if you try do define it by trying to match to one given Halt
decider, then DDD just needs to alter the code of HHH with some
null-effect change that maintains its responses, and thus defeats the
categories.
All you are showing is a lack of understanding of the power of
computing systems.
I find it suspicious that you use Olcott's terminology in your reply
(DDD and HHH): your brain might be frazzled or, a more fun thought, you
could be an Olcott sockpuppet. As I don't follow Olcott's work that
closely I am unsure what DDD and HHH refer to, I use H for decider and
P for input.
It would be posssible for neos to disallow P from accessing H
programmatically, both H's compile time and runtime representations.
Enforcing type stratification at a language level would not be a
difficult modification to neos.
/Flibble
But it can't prevent P from accessing a copy of H, that has had a
non-behavior changing modifcation done to it.
Since that modified version of H should still be considered a Halt
Detector, but neos can't determine that, you can't have that as a
category.
This goes to the problem that the final program doesn't include all the
meta-information that might have gone into making it.
For instance, I can make a program that by its construction is provably
correct, but if I just give you that program and the initial
specification, you might not be able to prove it to be correct.
This is the essence of the incompleteness theorem.
Since you can't detect that a piece of code uses an algorithm that does
"halt detection", you can't make that a category to partion your code
into spaces.
In general I agree. We have to weigh the limits that computer science
imposes against the practicalities that software engineering requires.
/Flibble
On 8/1/25 11:36 AM, Mr Flibble wrote:
On Fri, 01 Aug 2025 11:16:01 -0400, Richard Damon wrote:
On 8/1/25 11:08 AM, Mr Flibble wrote:
On Fri, 01 Aug 2025 10:24:40 -0400, Richard Damon wrote:
On 8/1/25 10:08 AM, Mr Flibble wrote:
On Fri, 01 Aug 2025 10:01:10 -0400, Richard Damon wrote:
On 8/1/25 8:40 AM, Mr Flibble wrote:I could quite easily design a program verification system which has >>>>>> the type stratification I propose allowing the type constraint I
Proving an algorithm is correct necessitates a stratified type >>>>>>>> system which recognises a category error present in extant
halting problem proofs (self referential conflation of a decider >>>>>>>> with its input); the halting problem as currently defined is only >>>>>>>> appropriate for untyped systems, it needs to be constrained to a >>>>>>>> typed system and when it is all extant halting problem proofs
relying on diagonalization are rendered moot.
The two types of programs are:
(A) halt deciders;
(B) programs being proven by the decider.
Type constraints:
(B) cannot encode (A) due to uni-directionality.
If (B) is a subset of (A) and cannot use (without violating type >>>>>>>> constraints) a possibly modified copy of (A) (as done in the
diagonalization proofs) then a new research avenue in the area of >>>>>>>> algorithm analysis and program correctness is opened up,
uninhibited by the traditional blocker namely Turing's Halting >>>>>>>> Problem.
/Flibble
And the assumption that proof of "correctness" is a necessity, or >>>>>>> requrement of the system is an error.
It is provable that more "problems" exist to try to answer, then >>>>>>> there are programs to try to answer them, and thus, there must
exist problems that can't be answered by a program.
The problem with your definitions, is you can't determine if some >>>>>>> chunk of code IS part of (A), and thus your system can't be used. >>>>>>
have defined to be enforced. My universal compiler framework
(neos) could easily achieve this even if the decider and the input >>>>>> are IN THE SAME SOURCE CODE FILE.
https://neos.dev
/Flibble
Note, if you try do define it by trying to match to one given Halt
decider, then DDD just needs to alter the code of HHH with some
null-effect change that maintains its responses, and thus defeats
the categories.
All you are showing is a lack of understanding of the power of
computing systems.
I find it suspicious that you use Olcott's terminology in your reply
(DDD and HHH): your brain might be frazzled or, a more fun thought,
you could be an Olcott sockpuppet. As I don't follow Olcott's work
that closely I am unsure what DDD and HHH refer to, I use H for
decider and P for input.
It would be posssible for neos to disallow P from accessing H
programmatically, both H's compile time and runtime representations.
Enforcing type stratification at a language level would not be a
difficult modification to neos.
/Flibble
But it can't prevent P from accessing a copy of H, that has had a
non-behavior changing modifcation done to it.
Since that modified version of H should still be considered a Halt
Detector, but neos can't determine that, you can't have that as a
category.
This goes to the problem that the final program doesn't include all
the meta-information that might have gone into making it.
For instance, I can make a program that by its construction is
provably correct, but if I just give you that program and the initial
specification, you might not be able to prove it to be correct.
This is the essence of the incompleteness theorem.
Since you can't detect that a piece of code uses an algorithm that
does "halt detection", you can't make that a category to partion your
code into spaces.
In general I agree. We have to weigh the limits that computer science
imposes against the practicalities that software engineering requires.
/Flibble
Right, so you argee that you can't define the categories, so your
concept just fails.
Yes, there are alternate discussions about partial deciders and what
they might be able to handle, but that is outside this topic.
On Fri, 01 Aug 2025 11:55:24 -0400, Richard Damon wrote:
On 8/1/25 11:36 AM, Mr Flibble wrote:
On Fri, 01 Aug 2025 11:16:01 -0400, Richard Damon wrote:
On 8/1/25 11:08 AM, Mr Flibble wrote:
On Fri, 01 Aug 2025 10:24:40 -0400, Richard Damon wrote:
On 8/1/25 10:08 AM, Mr Flibble wrote:
On Fri, 01 Aug 2025 10:01:10 -0400, Richard Damon wrote:
On 8/1/25 8:40 AM, Mr Flibble wrote:I could quite easily design a program verification system which has >>>>>>> the type stratification I propose allowing the type constraint I >>>>>>> have defined to be enforced. My universal compiler framework
Proving an algorithm is correct necessitates a stratified type >>>>>>>>> system which recognises a category error present in extant
halting problem proofs (self referential conflation of a decider >>>>>>>>> with its input); the halting problem as currently defined is only >>>>>>>>> appropriate for untyped systems, it needs to be constrained to a >>>>>>>>> typed system and when it is all extant halting problem proofs >>>>>>>>> relying on diagonalization are rendered moot.
The two types of programs are:
(A) halt deciders;
(B) programs being proven by the decider.
Type constraints:
(B) cannot encode (A) due to uni-directionality.
If (B) is a subset of (A) and cannot use (without violating type >>>>>>>>> constraints) a possibly modified copy of (A) (as done in the >>>>>>>>> diagonalization proofs) then a new research avenue in the area of >>>>>>>>> algorithm analysis and program correctness is opened up,
uninhibited by the traditional blocker namely Turing's Halting >>>>>>>>> Problem.
/Flibble
And the assumption that proof of "correctness" is a necessity, or >>>>>>>> requrement of the system is an error.
It is provable that more "problems" exist to try to answer, then >>>>>>>> there are programs to try to answer them, and thus, there must >>>>>>>> exist problems that can't be answered by a program.
The problem with your definitions, is you can't determine if some >>>>>>>> chunk of code IS part of (A), and thus your system can't be used. >>>>>>>
(neos) could easily achieve this even if the decider and the input >>>>>>> are IN THE SAME SOURCE CODE FILE.
https://neos.dev
/Flibble
Note, if you try do define it by trying to match to one given Halt >>>>>> decider, then DDD just needs to alter the code of HHH with some
null-effect change that maintains its responses, and thus defeats
the categories.
All you are showing is a lack of understanding of the power of
computing systems.
I find it suspicious that you use Olcott's terminology in your reply >>>>> (DDD and HHH): your brain might be frazzled or, a more fun thought,
you could be an Olcott sockpuppet. As I don't follow Olcott's work
that closely I am unsure what DDD and HHH refer to, I use H for
decider and P for input.
It would be posssible for neos to disallow P from accessing H
programmatically, both H's compile time and runtime representations. >>>>> Enforcing type stratification at a language level would not be a
difficult modification to neos.
/Flibble
But it can't prevent P from accessing a copy of H, that has had a
non-behavior changing modifcation done to it.
Since that modified version of H should still be considered a Halt
Detector, but neos can't determine that, you can't have that as a
category.
This goes to the problem that the final program doesn't include all
the meta-information that might have gone into making it.
For instance, I can make a program that by its construction is
provably correct, but if I just give you that program and the initial
specification, you might not be able to prove it to be correct.
This is the essence of the incompleteness theorem.
Since you can't detect that a piece of code uses an algorithm that
does "halt detection", you can't make that a category to partion your
code into spaces.
In general I agree. We have to weigh the limits that computer science
imposes against the practicalities that software engineering requires.
/Flibble
Right, so you argee that you can't define the categories, so your
concept just fails.
Yes, there are alternate discussions about partial deciders and what
they might be able to handle, but that is outside this topic.
I agree that if P can (using simulation or some other form of semantic analysis) analyse H using a COPY of H and we are dealing with idealistic turing machines then, yes, the system fails.
/Flibble
Proving an algorithm is correct necessitates a stratified type system
which recognises a category error present in extant halting problem proofs (self referential conflation of a decider with its input); the halting problem as currently defined is only appropriate for untyped systems, it needs to be constrained to a typed system and when it is all extant
halting problem proofs relying on diagonalization are rendered moot.
The two types of programs are:
(A) halt deciders;
(B) programs being proven by the decider.
Type constraints:
(B) cannot encode (A) due to uni-directionality.
Mr Flibble <flibble@red-dwarf.jmc.corp> writes:
Proving an algorithm is correct necessitates a stratified type system
which recognises a category error present in extant halting problem
proofs (self referential conflation of a decider with its input); the
halting problem as currently defined is only appropriate for untyped
systems, it needs to be constrained to a typed system and when it is
all extant halting problem proofs relying on diagonalization are
rendered moot.
The two types of programs are:
(A) halt deciders;
(B) programs being proven by the decider.
At the risk of falling into the trap that you are deliberately misusing standard terms...
Type constraints:
(B) cannot encode (A) due to uni-directionality.
... this constraint is always met as (A) is empty so (B) cannot encode
any element of (A).
On 8/1/2025 7:10 PM, Ben Bacarisse wrote:
Mr Flibble <flibble@red-dwarf.jmc.corp> writes:
Proving an algorithm is correct necessitates a stratified type system
which recognises a category error present in extant halting problem
proofs
(self referential conflation of a decider with its input); the halting
problem as currently defined is only appropriate for untyped systems, it >>> needs to be constrained to a typed system and when it is all extant
halting problem proofs relying on diagonalization are rendered moot.
The two types of programs are:
(A) halt deciders;
(B) programs being proven by the decider.
At the risk of falling into the trap that you are deliberately misusing
standard terms...
Type constraints:
(B) cannot encode (A) due to uni-directionality.
... this constraint is always met as (A) is empty so (B) cannot encode
any element of (A).
*There is a violated type constraint in the Linz proof*
Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.embedded_H ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.∞,
if Ĥ applied to ⟨Ĥ⟩ halts, and
Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.embedded_H ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qn
if Ĥ applied to ⟨Ĥ⟩ does not halt.
The "if" statements are incorrect because
Ĥ is not of the finite string type.
The Linz proof requires Ĥ.embedded_H to report
on its own behavior instead of the behavior of
its input.
Proving an algorithm is correct necessitates a stratified type system
which recognises a category error present in extant halting problem proofs (self referential conflation of a decider with its input); the halting problem as currently defined is only appropriate for untyped systems, it needs to be constrained to a typed system and when it is all extant
halting problem proofs relying on diagonalization are rendered moot.
| Sysop: | Keyop |
|---|---|
| Location: | Huddersfield, West Yorkshire, UK |
| Users: | 546 |
| Nodes: | 16 (2 / 14) |
| Uptime: | 04:19:14 |
| Calls: | 10,386 |
| Calls today: | 1 |
| Files: | 14,057 |
| Messages: | 6,416,606 |