Refutation of Strachey’s 1965 Proof Based on Self-Referential Conflation
as a Category (Type) Error
This document refutes Christopher Strachey’s 1965 argument in “An Impossible Program” by leveraging the assumption that self-referential conflation of a halt decider and its input constitutes a category (type) error. The refutation demonstrates that Strachey’s proof, which relies on
a self-referential program construction, is invalid in a typed system
where such conflation is prohibited.
---
1. Strachey’s 1965 Argument
In “An Impossible Program” (The Computer Journal, Vol. 7, No. 4, p. 313, 1965), Strachey presents a proof of the undecidability of the halting problem. The argument assumes a halt decider T, which determines whether
any program P halts on a given input. Strachey constructs a program Strachey_P as follows:
void Strachey_P() {
L: if (T(Strachey_P)) goto L;
return;
}
Here, T(Strachey_P) checks whether Strachey_P halts. The proof analyzes Strachey_P’s behavior:
- If T(Strachey_P) returns true (Strachey_P halts), Strachey_P loops infinitely (does not halt).
- If T(Strachey_P) returns false (Strachey_P does not halt), Strachey_P halts.
This contradiction implies that T cannot exist, proving the halting
problem undecidable.
---
2. Assumption: Self-Referential Conflation as a Type Error
The refutation assumes that the self-referential call T(Strachey_P) within Strachey_P constitutes a category (type) error. A type error occurs when
an operation is applied to arguments of an inappropriate type. Here, conflating the halt decider T with its input Strachey_P (by allowing Strachey_P to embed T(Strachey_P)) is argued to violate type constraints, rendering Strachey_P ill-formed.
---
3. Refutation
The refutation proceeds by demonstrating that Strachey_P is invalid in a typed system due to a type error, undermining the contradiction in Strachey’s proof.
3.1. Type System
In a typed context, the halt decider T has a type signature:
T: (Program, Input) → Boolean
where Program is the type of valid program descriptions, and Input is the type of program inputs. Strachey_P, as a program, must be of type Program
to be a valid argument to T. The call T(Strachey_P) requires Strachey_P to
be a well-defined program description.
3.2. Self-Reference as a Type Error
Strachey_P’s definition includes T(Strachey_P), meaning Strachey_P depends on its own description as an argument to T. This self-reference creates a circular dependency:
- Strachey_P’s type cannot be resolved without evaluating T(Strachey_P).
- T(Strachey_P) requires Strachey_P to be a fully defined Program.
In a strict type system, such circular definitions are rejected as type errors, as they violate referential transparency. Strachey_P is thus not a well-formed program, as its type is undefined due to the self-referential conflation.
3.3. Impact on Strachey’s Proof
Strachey’s proof assumes Strachey_P is a valid program. If T(Strachey_P)
is a type error, Strachey_P is ill-formed and cannot be used to derive a contradiction. The proof’s logic collapses, as the contradictory behavior (halting or not halting) depends on an invalid program. Therefore, the argument fails to demonstrate that T cannot exist.
3.4. Implications
By excluding self-referential programs like Strachey_P due to type errors, the proof’s universality is challenged. A halt decider T might exist for non-self-referential programs in a typed system, suggesting that
Strachey’s proof does not establish undecidability in such contexts.
3.5. Critical Examination
- Counterargument: Turing machines, as used by Strachey, are untyped, allowing self-referential programs without type errors.
- Response: Imposing a type discipline on the computational model (e.g., typed lambda calculus) restricts self-reference. In such systems,
Strachey_P is invalid, and the proof does not hold.
- Limitation: This refutation targets Strachey’s specific construction and does not disprove the halting problem’s undecidability, which is supported by other proofs (e.g., Turing 1936).
---
4. Conclusion
Based on the assumption that self-referential conflation is a type error, Strachey’s 1965 proof is refuted. The program Strachey_P is ill-formed due to the type error in T(Strachey_P), invalidating the contradiction. This highlights the role of type systems in computational arguments and shows
that Strachey’s proof fails in typed contexts where self-reference is restricted.
On 4/21/25 6:21 AM, Mr Flibble wrote:
Refutation of Strachey’s 1965 Proof Based on Self-Referential
Conflation as a Category (Type) Error
This document refutes Christopher Strachey’s 1965 argument in “An
Impossible Program” by leveraging the assumption that self-referential
conflation of a halt decider and its input constitutes a category
(type) error. The refutation demonstrates that Strachey’s proof, which
relies on a self-referential program construction, is invalid in a
typed system where such conflation is prohibited.
---
1. Strachey’s 1965 Argument In “An Impossible Program” (The Computer >> Journal, Vol. 7, No. 4, p. 313,
1965), Strachey presents a proof of the undecidability of the halting
problem. The argument assumes a halt decider T, which determines
whether any program P halts on a given input. Strachey constructs a
program Strachey_P as follows:
void Strachey_P() {
L: if (T(Strachey_P)) goto L; return;
}
Here, T(Strachey_P) checks whether Strachey_P halts. The proof analyzes
Strachey_P’s behavior:
- If T(Strachey_P) returns true (Strachey_P halts), Strachey_P loops
infinitely (does not halt).
- If T(Strachey_P) returns false (Strachey_P does not halt), Strachey_P
halts.
This contradiction implies that T cannot exist, proving the halting
problem undecidable.
---
2. Assumption: Self-Referential Conflation as a Type Error The
refutation assumes that the self-referential call T(Strachey_P) within
Strachey_P constitutes a category (type) error. A type error occurs
when an operation is applied to arguments of an inappropriate type.
Here, conflating the halt decider T with its input Strachey_P (by
allowing Strachey_P to embed T(Strachey_P)) is argued to violate type
constraints, rendering Strachey_P ill-formed.
And where do you get that assumption from? It is valid logic to
temporarily assume a statement true to prove that it leads to a
contradiction and thus can't be true.
It is NOT valid to just assume it to be true and then use its Truth to
prove something else is true.
You are just showing your ignorance of the topic.
---
3. Refutation The refutation proceeds by demonstrating that Strachey_P
is invalid in a typed system due to a type error, undermining the
contradiction in Strachey’s proof.
But only by an unproven assumption.
3.1. Type System In a typed context, the halt decider T has a type
signature:
T: (Program, Input) → Boolean
where Program is the type of valid program descriptions, and Input is
the type of program inputs. Strachey_P, as a program, must be of type
Program to be a valid argument to T. The call T(Strachey_P) requires
Strachey_P to be a well-defined program description.
Which it is, at least if T is.
3.2. Self-Reference as a Type Error Strachey_P’s definition includes
T(Strachey_P), meaning Strachey_P depends on its own description as an
argument to T. This self-reference creates a circular dependency:
- Strachey_P’s type cannot be resolved without evaluating
T(Strachey_P).
Your "type" was that it was a program. That is not a dynamically
determined category, but a statically determined one.
Note, that if T was a program, its actual response is solely determined
by the input it is given.
- T(Strachey_P) requires Strachey_P to be a fully defined Program.
In a strict type system, such circular definitions are rejected as type
errors, as they violate referential transparency. Strachey_P is thus
not a well-formed program, as its type is undefined due to the
self-referential conflation.
And it is, as program definition is based on fully defining the code of
said program, and the code of Strachey_P is fully defined and built by
legal processes.
Your "Type System" is not "strictly" defined, but improperly defined.
3.3. Impact on Strachey’s Proof Strachey’s proof assumes Strachey_P is >> a valid program. If T(Strachey_P) is a type error, Strachey_P is
ill-formed and cannot be used to derive a contradiction. The proof’s
logic collapses, as the contradictory behavior (halting or not halting)
depends on an invalid program. Therefore, the argument fails to
demonstrate that T cannot exist.
But it IS a valid program, as the definition of a valid program is being built on valid construction processes.
What "Error" was made in the construction of Strachey_P?
The only way for Strachey_P to be an invalid program is for T to not be
a valid one.
3.4. Implications By excluding self-referential programs like
Strachey_P due to type errors, the proof’s universality is challenged.
A halt decider T might exist for non-self-referential programs in a
typed system, suggesting that Strachey’s proof does not establish
undecidability in such contexts.
But you didn't prove your point, as there was no type error of the types defined by the problem.
3.5. Critical Examination - Counterargument: Turing machines, as used
by Strachey, are untyped, allowing self-referential programs without
type errors.
Actually, Turing Machines don't support "references" at all, so there
can't BE a self-refeential program. We just are allowed to give programs descriptions of themselves as part of "for any input".
And since Halt Deciders are DEFINED to answer about any program
described to them, you can't limit that domain with a type that doesn't
cover ALL programs.
- Response: Imposing a type discipline on the computational model
(e.g., typed lambda calculus) restricts self-reference. In such
systems, Strachey_P is invalid, and the proof does not hold.
But you need to impose a VALID type system. A Prgram defined to take as
an input *ALL* programs (via their description) must still take in *ALL* programs to be valid for its definition.
- Limitation: This refutation targets Strachey’s specific construction
and does not disprove the halting problem’s undecidability, which is
supported by other proofs (e.g., Turing 1936).
Whch means you really are admitting you aren't doing anything,
---
4. Conclusion Based on the assumption that self-referential conflation
is a type error, Strachey’s 1965 proof is refuted. The program
Strachey_P is ill-formed due to the type error in T(Strachey_P),
invalidating the contradiction. This highlights the role of type
systems in computational arguments and shows that Strachey’s proof
fails in typed contexts where self-reference is restricted.
Right, based on a false assumption you can prove a false claim.
Congradulations, you just proved that bad logic leads to bad
conclusions, and that your "type system" just isn't a useful tool the
way you are using it.
It seems you only have a hammer, and thus see everything as a Nail, even
if it is actually a screw.
On Mon, 21 Apr 2025 06:54:33 -0400, Richard Damon wrote:
On 4/21/25 6:21 AM, Mr Flibble wrote:
Refutation of Strachey’s 1965 Proof Based on Self-Referential
Conflation as a Category (Type) Error
This document refutes Christopher Strachey’s 1965 argument in “An
Impossible Program” by leveraging the assumption that self-referential >>> conflation of a halt decider and its input constitutes a category
(type) error. The refutation demonstrates that Strachey’s proof, which >>> relies on a self-referential program construction, is invalid in a
typed system where such conflation is prohibited.
---
1. Strachey’s 1965 Argument In “An Impossible Program” (The Computer >>> Journal, Vol. 7, No. 4, p. 313,
1965), Strachey presents a proof of the undecidability of the halting
problem. The argument assumes a halt decider T, which determines
whether any program P halts on a given input. Strachey constructs a
program Strachey_P as follows:
void Strachey_P() {
L: if (T(Strachey_P)) goto L; return;
}
Here, T(Strachey_P) checks whether Strachey_P halts. The proof analyzes
Strachey_P’s behavior:
- If T(Strachey_P) returns true (Strachey_P halts), Strachey_P loops
infinitely (does not halt).
- If T(Strachey_P) returns false (Strachey_P does not halt), Strachey_P
halts.
This contradiction implies that T cannot exist, proving the halting
problem undecidable.
---
2. Assumption: Self-Referential Conflation as a Type Error The
refutation assumes that the self-referential call T(Strachey_P) within
Strachey_P constitutes a category (type) error. A type error occurs
when an operation is applied to arguments of an inappropriate type.
Here, conflating the halt decider T with its input Strachey_P (by
allowing Strachey_P to embed T(Strachey_P)) is argued to violate type
constraints, rendering Strachey_P ill-formed.
And where do you get that assumption from? It is valid logic to
temporarily assume a statement true to prove that it leads to a
contradiction and thus can't be true.
It is NOT valid to just assume it to be true and then use its Truth to
prove something else is true.
You are just showing your ignorance of the topic.
---
3. Refutation The refutation proceeds by demonstrating that Strachey_P
is invalid in a typed system due to a type error, undermining the
contradiction in Strachey’s proof.
But only by an unproven assumption.
3.1. Type System In a typed context, the halt decider T has a type
signature:
T: (Program, Input) → Boolean
where Program is the type of valid program descriptions, and Input is
the type of program inputs. Strachey_P, as a program, must be of type
Program to be a valid argument to T. The call T(Strachey_P) requires
Strachey_P to be a well-defined program description.
Which it is, at least if T is.
3.2. Self-Reference as a Type Error Strachey_P’s definition includes
T(Strachey_P), meaning Strachey_P depends on its own description as an
argument to T. This self-reference creates a circular dependency:
- Strachey_P’s type cannot be resolved without evaluating
T(Strachey_P).
Your "type" was that it was a program. That is not a dynamically
determined category, but a statically determined one.
Note, that if T was a program, its actual response is solely determined
by the input it is given.
- T(Strachey_P) requires Strachey_P to be a fully defined Program.
In a strict type system, such circular definitions are rejected as type
errors, as they violate referential transparency. Strachey_P is thus
not a well-formed program, as its type is undefined due to the
self-referential conflation.
And it is, as program definition is based on fully defining the code of
said program, and the code of Strachey_P is fully defined and built by
legal processes.
Your "Type System" is not "strictly" defined, but improperly defined.
3.3. Impact on Strachey’s Proof Strachey’s proof assumes Strachey_P is >>> a valid program. If T(Strachey_P) is a type error, Strachey_P is
ill-formed and cannot be used to derive a contradiction. The proof’s
logic collapses, as the contradictory behavior (halting or not halting)
depends on an invalid program. Therefore, the argument fails to
demonstrate that T cannot exist.
But it IS a valid program, as the definition of a valid program is being
built on valid construction processes.
What "Error" was made in the construction of Strachey_P?
The only way for Strachey_P to be an invalid program is for T to not be
a valid one.
3.4. Implications By excluding self-referential programs like
Strachey_P due to type errors, the proof’s universality is challenged. >>> A halt decider T might exist for non-self-referential programs in a
typed system, suggesting that Strachey’s proof does not establish
undecidability in such contexts.
But you didn't prove your point, as there was no type error of the types
defined by the problem.
3.5. Critical Examination - Counterargument: Turing machines, as used
by Strachey, are untyped, allowing self-referential programs without
type errors.
Actually, Turing Machines don't support "references" at all, so there
can't BE a self-refeential program. We just are allowed to give programs
descriptions of themselves as part of "for any input".
And since Halt Deciders are DEFINED to answer about any program
described to them, you can't limit that domain with a type that doesn't
cover ALL programs.
- Response: Imposing a type discipline on the computational model
(e.g., typed lambda calculus) restricts self-reference. In such
systems, Strachey_P is invalid, and the proof does not hold.
But you need to impose a VALID type system. A Prgram defined to take as
an input *ALL* programs (via their description) must still take in *ALL*
programs to be valid for its definition.
- Limitation: This refutation targets Strachey’s specific construction >>> and does not disprove the halting problem’s undecidability, which is
supported by other proofs (e.g., Turing 1936).
Whch means you really are admitting you aren't doing anything,
---
4. Conclusion Based on the assumption that self-referential conflation
is a type error, Strachey’s 1965 proof is refuted. The program
Strachey_P is ill-formed due to the type error in T(Strachey_P),
invalidating the contradiction. This highlights the role of type
systems in computational arguments and shows that Strachey’s proof
fails in typed contexts where self-reference is restricted.
Right, based on a false assumption you can prove a false claim.
Congradulations, you just proved that bad logic leads to bad
conclusions, and that your "type system" just isn't a useful tool the
way you are using it.
It seems you only have a hammer, and thus see everything as a Nail, even
if it is actually a screw.
A circular dependency is like a circular argument or circular reasoning:
not logically sound.
/Flibble
On Mon, 21 Apr 2025 06:54:33 -0400, Richard Damon wrote:
On 4/21/25 6:21 AM, Mr Flibble wrote:
Refutation of Strachey’s 1965 Proof Based on Self-Referential
Conflation as a Category (Type) Error
This document refutes Christopher Strachey’s 1965 argument in “An
Impossible Program” by leveraging the assumption that self-referential >>> conflation of a halt decider and its input constitutes a category
(type) error. The refutation demonstrates that Strachey’s proof, which >>> relies on a self-referential program construction, is invalid in a
typed system where such conflation is prohibited.
---
1. Strachey’s 1965 Argument In “An Impossible Program” (The Computer >>> Journal, Vol. 7, No. 4, p. 313,
1965), Strachey presents a proof of the undecidability of the halting
problem. The argument assumes a halt decider T, which determines
whether any program P halts on a given input. Strachey constructs a
program Strachey_P as follows:
void Strachey_P() {
L: if (T(Strachey_P)) goto L; return;
}
Here, T(Strachey_P) checks whether Strachey_P halts. The proof analyzes
Strachey_P’s behavior:
- If T(Strachey_P) returns true (Strachey_P halts), Strachey_P loops
infinitely (does not halt).
- If T(Strachey_P) returns false (Strachey_P does not halt), Strachey_P
halts.
This contradiction implies that T cannot exist, proving the halting
problem undecidable.
---
2. Assumption: Self-Referential Conflation as a Type Error The
refutation assumes that the self-referential call T(Strachey_P) within
Strachey_P constitutes a category (type) error. A type error occurs
when an operation is applied to arguments of an inappropriate type.
Here, conflating the halt decider T with its input Strachey_P (by
allowing Strachey_P to embed T(Strachey_P)) is argued to violate type
constraints, rendering Strachey_P ill-formed.
And where do you get that assumption from? It is valid logic to
temporarily assume a statement true to prove that it leads to a
contradiction and thus can't be true.
It is NOT valid to just assume it to be true and then use its Truth to
prove something else is true.
You are just showing your ignorance of the topic.
---
3. Refutation The refutation proceeds by demonstrating that Strachey_P
is invalid in a typed system due to a type error, undermining the
contradiction in Strachey’s proof.
But only by an unproven assumption.
3.1. Type System In a typed context, the halt decider T has a type
signature:
T: (Program, Input) → Boolean
where Program is the type of valid program descriptions, and Input is
the type of program inputs. Strachey_P, as a program, must be of type
Program to be a valid argument to T. The call T(Strachey_P) requires
Strachey_P to be a well-defined program description.
Which it is, at least if T is.
3.2. Self-Reference as a Type Error Strachey_P’s definition includes
T(Strachey_P), meaning Strachey_P depends on its own description as an
argument to T. This self-reference creates a circular dependency:
- Strachey_P’s type cannot be resolved without evaluating
T(Strachey_P).
Your "type" was that it was a program. That is not a dynamically
determined category, but a statically determined one.
Note, that if T was a program, its actual response is solely determined
by the input it is given.
- T(Strachey_P) requires Strachey_P to be a fully defined Program.
In a strict type system, such circular definitions are rejected as type
errors, as they violate referential transparency. Strachey_P is thus
not a well-formed program, as its type is undefined due to the
self-referential conflation.
And it is, as program definition is based on fully defining the code of
said program, and the code of Strachey_P is fully defined and built by
legal processes.
Your "Type System" is not "strictly" defined, but improperly defined.
3.3. Impact on Strachey’s Proof Strachey’s proof assumes Strachey_P is >>> a valid program. If T(Strachey_P) is a type error, Strachey_P is
ill-formed and cannot be used to derive a contradiction. The proof’s
logic collapses, as the contradictory behavior (halting or not halting)
depends on an invalid program. Therefore, the argument fails to
demonstrate that T cannot exist.
But it IS a valid program, as the definition of a valid program is being
built on valid construction processes.
What "Error" was made in the construction of Strachey_P?
The only way for Strachey_P to be an invalid program is for T to not be
a valid one.
3.4. Implications By excluding self-referential programs like
Strachey_P due to type errors, the proof’s universality is challenged. >>> A halt decider T might exist for non-self-referential programs in a
typed system, suggesting that Strachey’s proof does not establish
undecidability in such contexts.
But you didn't prove your point, as there was no type error of the types
defined by the problem.
3.5. Critical Examination - Counterargument: Turing machines, as used
by Strachey, are untyped, allowing self-referential programs without
type errors.
Actually, Turing Machines don't support "references" at all, so there
can't BE a self-refeential program. We just are allowed to give programs
descriptions of themselves as part of "for any input".
And since Halt Deciders are DEFINED to answer about any program
described to them, you can't limit that domain with a type that doesn't
cover ALL programs.
- Response: Imposing a type discipline on the computational model
(e.g., typed lambda calculus) restricts self-reference. In such
systems, Strachey_P is invalid, and the proof does not hold.
But you need to impose a VALID type system. A Prgram defined to take as
an input *ALL* programs (via their description) must still take in *ALL*
programs to be valid for its definition.
- Limitation: This refutation targets Strachey’s specific construction >>> and does not disprove the halting problem’s undecidability, which is
supported by other proofs (e.g., Turing 1936).
Whch means you really are admitting you aren't doing anything,
---
4. Conclusion Based on the assumption that self-referential conflation
is a type error, Strachey’s 1965 proof is refuted. The program
Strachey_P is ill-formed due to the type error in T(Strachey_P),
invalidating the contradiction. This highlights the role of type
systems in computational arguments and shows that Strachey’s proof
fails in typed contexts where self-reference is restricted.
Right, based on a false assumption you can prove a false claim.
Congradulations, you just proved that bad logic leads to bad
conclusions, and that your "type system" just isn't a useful tool the
way you are using it.
It seems you only have a hammer, and thus see everything as a Nail, even
if it is actually a screw.
A circular dependency is like a circular argument or circular reasoning:
not logically sound.
On 2025-04-21 11:18:23 +0000, Mr Flibble said:
On Mon, 21 Apr 2025 06:54:33 -0400, Richard Damon wrote:
On 4/21/25 6:21 AM, Mr Flibble wrote:
Refutation of Strachey’s 1965 Proof Based on Self-Referential
Conflation as a Category (Type) Error
This document refutes Christopher Strachey’s 1965 argument in “An
Impossible Program” by leveraging the assumption that
self-referential conflation of a halt decider and its input
constitutes a category (type) error. The refutation demonstrates that
Strachey’s proof, which relies on a self-referential program
construction, is invalid in a typed system where such conflation is
prohibited.
---
1. Strachey’s 1965 Argument In “An Impossible Program” (The Computer >>>> Journal, Vol. 7, No. 4, p. 313,
1965), Strachey presents a proof of the undecidability of the halting
problem. The argument assumes a halt decider T, which determines
whether any program P halts on a given input. Strachey constructs a
program Strachey_P as follows:
void Strachey_P() {
L: if (T(Strachey_P)) goto L; return;
}
Here, T(Strachey_P) checks whether Strachey_P halts. The proof
analyzes Strachey_P’s behavior:
- If T(Strachey_P) returns true (Strachey_P halts), Strachey_P loops
infinitely (does not halt).
- If T(Strachey_P) returns false (Strachey_P does not halt),
Strachey_P halts.
This contradiction implies that T cannot exist, proving the halting
problem undecidable.
---
2. Assumption: Self-Referential Conflation as a Type Error The
refutation assumes that the self-referential call T(Strachey_P)
within Strachey_P constitutes a category (type) error. A type error
occurs when an operation is applied to arguments of an inappropriate
type.
Here, conflating the halt decider T with its input Strachey_P (by
allowing Strachey_P to embed T(Strachey_P)) is argued to violate type
constraints, rendering Strachey_P ill-formed.
And where do you get that assumption from? It is valid logic to
temporarily assume a statement true to prove that it leads to a
contradiction and thus can't be true.
It is NOT valid to just assume it to be true and then use its Truth to
prove something else is true.
You are just showing your ignorance of the topic.
---
3. Refutation The refutation proceeds by demonstrating that
Strachey_P is invalid in a typed system due to a type error,
undermining the contradiction in Strachey’s proof.
But only by an unproven assumption.
3.1. Type System In a typed context, the halt decider T has a type
signature:
T: (Program, Input) → Boolean where Program is the type of valid
program descriptions, and Input is the type of program inputs.
Strachey_P, as a program, must be of type Program to be a valid
argument to T. The call T(Strachey_P) requires Strachey_P to be a
well-defined program description.
Which it is, at least if T is.
3.2. Self-Reference as a Type Error Strachey_P’s definition includes >>>> T(Strachey_P), meaning Strachey_P depends on its own description as
an argument to T. This self-reference creates a circular dependency:
- Strachey_P’s type cannot be resolved without evaluating
T(Strachey_P).
Your "type" was that it was a program. That is not a dynamically
determined category, but a statically determined one.
Note, that if T was a program, its actual response is solely
determined by the input it is given.
- T(Strachey_P) requires Strachey_P to be a fully defined Program.
In a strict type system, such circular definitions are rejected as
type errors, as they violate referential transparency. Strachey_P is
thus not a well-formed program, as its type is undefined due to the
self-referential conflation.
And it is, as program definition is based on fully defining the code
of said program, and the code of Strachey_P is fully defined and built
by legal processes.
Your "Type System" is not "strictly" defined, but improperly defined.
3.3. Impact on Strachey’s Proof Strachey’s proof assumes Strachey_P >>>> is a valid program. If T(Strachey_P) is a type error, Strachey_P is
ill-formed and cannot be used to derive a contradiction. The proof’s >>>> logic collapses, as the contradictory behavior (halting or not
halting) depends on an invalid program. Therefore, the argument fails
to demonstrate that T cannot exist.
But it IS a valid program, as the definition of a valid program is
being built on valid construction processes.
What "Error" was made in the construction of Strachey_P?
The only way for Strachey_P to be an invalid program is for T to not
be a valid one.
3.4. Implications By excluding self-referential programs like
Strachey_P due to type errors, the proof’s universality is
challenged. A halt decider T might exist for non-self-referential
programs in a typed system, suggesting that Strachey’s proof does not >>>> establish undecidability in such contexts.
But you didn't prove your point, as there was no type error of the
types defined by the problem.
3.5. Critical Examination - Counterargument: Turing machines, as used
by Strachey, are untyped, allowing self-referential programs without
type errors.
Actually, Turing Machines don't support "references" at all, so there
can't BE a self-refeential program. We just are allowed to give
programs descriptions of themselves as part of "for any input".
And since Halt Deciders are DEFINED to answer about any program
described to them, you can't limit that domain with a type that
doesn't cover ALL programs.
- Response: Imposing a type discipline on the computational model
(e.g., typed lambda calculus) restricts self-reference. In such
systems, Strachey_P is invalid, and the proof does not hold.
But you need to impose a VALID type system. A Prgram defined to take
as an input *ALL* programs (via their description) must still take in
*ALL*
programs to be valid for its definition.
- Limitation: This refutation targets Strachey’s specific
construction and does not disprove the halting problem’s
undecidability, which is supported by other proofs (e.g., Turing
1936).
Whch means you really are admitting you aren't doing anything,
---
4. Conclusion Based on the assumption that self-referential
conflation is a type error, Strachey’s 1965 proof is refuted. The
program Strachey_P is ill-formed due to the type error in
T(Strachey_P), invalidating the contradiction. This highlights the
role of type systems in computational arguments and shows that
Strachey’s proof fails in typed contexts where self-reference is
restricted.
Right, based on a false assumption you can prove a false claim.
Congradulations, you just proved that bad logic leads to bad
conclusions, and that your "type system" just isn't a useful tool the
way you are using it.
It seems you only have a hammer, and thus see everything as a Nail,
even if it is actually a screw.
A circular dependency is like a circular argument or circular
reasoning:
not logically sound.
A circular argument is not like a circular argument. A circular argument means either that there is an unjustified assumption and thus the
argument is fallacious or that the proof is redundant and therefore not needed.
Dependency is not a logical concept. Statements of dependency always
involve an extra-logical knowledge or assumption. Whether such
statements are are true or false must be determined from such
extra-logical knowledge or assumptions with valid use of logic.
Mikko <[email protected]> writes:
On 2025-04-21 11:18:23 +0000, Mr Flibble said:[...]
A circular dependency is like a circular argument or circular
reasoning:
not logically sound.
A circular argument is not like a circular argument.
Are you sure about that? 8-)}
I think you meant to write that a circular *dependency* is not like a circular argument.
On Tue, 22 Apr 2025 11:39:42 +0300, Mikko wrote:
On 2025-04-21 11:18:23 +0000, Mr Flibble said:
On Mon, 21 Apr 2025 06:54:33 -0400, Richard Damon wrote:
On 4/21/25 6:21 AM, Mr Flibble wrote:
Refutation of Strachey’s 1965 Proof Based on Self-Referential
Conflation as a Category (Type) Error
This document refutes Christopher Strachey’s 1965 argument in “An >>>>> Impossible Program” by leveraging the assumption that
self-referential conflation of a halt decider and its input
constitutes a category (type) error. The refutation demonstrates that >>>>> Strachey’s proof, which relies on a self-referential program
construction, is invalid in a typed system where such conflation is
prohibited.
---
1. Strachey’s 1965 Argument In “An Impossible Program” (The Computer
Journal, Vol. 7, No. 4, p. 313,
1965), Strachey presents a proof of the undecidability of the halting >>>>> problem. The argument assumes a halt decider T, which determines
whether any program P halts on a given input. Strachey constructs a
program Strachey_P as follows:
void Strachey_P() {
L: if (T(Strachey_P)) goto L; return;
}
Here, T(Strachey_P) checks whether Strachey_P halts. The proof
analyzes Strachey_P’s behavior:
- If T(Strachey_P) returns true (Strachey_P halts), Strachey_P loops >>>>> infinitely (does not halt).
- If T(Strachey_P) returns false (Strachey_P does not halt),
Strachey_P halts.
This contradiction implies that T cannot exist, proving the halting
problem undecidable.
---
2. Assumption: Self-Referential Conflation as a Type Error The
refutation assumes that the self-referential call T(Strachey_P)
within Strachey_P constitutes a category (type) error. A type error
occurs when an operation is applied to arguments of an inappropriate >>>>> type.
Here, conflating the halt decider T with its input Strachey_P (by
allowing Strachey_P to embed T(Strachey_P)) is argued to violate type >>>>> constraints, rendering Strachey_P ill-formed.
And where do you get that assumption from? It is valid logic to
temporarily assume a statement true to prove that it leads to a
contradiction and thus can't be true.
It is NOT valid to just assume it to be true and then use its Truth to >>>> prove something else is true.
You are just showing your ignorance of the topic.
---
3. Refutation The refutation proceeds by demonstrating that
Strachey_P is invalid in a typed system due to a type error,
undermining the contradiction in Strachey’s proof.
But only by an unproven assumption.
3.1. Type System In a typed context, the halt decider T has a type
signature:
T: (Program, Input) → Boolean where Program is the type of valid
program descriptions, and Input is the type of program inputs.
Strachey_P, as a program, must be of type Program to be a valid
argument to T. The call T(Strachey_P) requires Strachey_P to be a
well-defined program description.
Which it is, at least if T is.
3.2. Self-Reference as a Type Error Strachey_P’s definition includes >>>>> T(Strachey_P), meaning Strachey_P depends on its own description as
an argument to T. This self-reference creates a circular dependency: >>>>> - Strachey_P’s type cannot be resolved without evaluating
T(Strachey_P).
Your "type" was that it was a program. That is not a dynamically
determined category, but a statically determined one.
Note, that if T was a program, its actual response is solely
determined by the input it is given.
- T(Strachey_P) requires Strachey_P to be a fully defined Program.
In a strict type system, such circular definitions are rejected as
type errors, as they violate referential transparency. Strachey_P is >>>>> thus not a well-formed program, as its type is undefined due to the
self-referential conflation.
And it is, as program definition is based on fully defining the code
of said program, and the code of Strachey_P is fully defined and built >>>> by legal processes.
Your "Type System" is not "strictly" defined, but improperly defined.
3.3. Impact on Strachey’s Proof Strachey’s proof assumes Strachey_P >>>>> is a valid program. If T(Strachey_P) is a type error, Strachey_P is
ill-formed and cannot be used to derive a contradiction. The proof’s >>>>> logic collapses, as the contradictory behavior (halting or not
halting) depends on an invalid program. Therefore, the argument fails >>>>> to demonstrate that T cannot exist.
But it IS a valid program, as the definition of a valid program is
being built on valid construction processes.
What "Error" was made in the construction of Strachey_P?
The only way for Strachey_P to be an invalid program is for T to not
be a valid one.
3.4. Implications By excluding self-referential programs like
Strachey_P due to type errors, the proof’s universality is
challenged. A halt decider T might exist for non-self-referential
programs in a typed system, suggesting that Strachey’s proof does not >>>>> establish undecidability in such contexts.
But you didn't prove your point, as there was no type error of the
types defined by the problem.
3.5. Critical Examination - Counterargument: Turing machines, as used >>>>> by Strachey, are untyped, allowing self-referential programs without >>>>> type errors.
Actually, Turing Machines don't support "references" at all, so there
can't BE a self-refeential program. We just are allowed to give
programs descriptions of themselves as part of "for any input".
And since Halt Deciders are DEFINED to answer about any program
described to them, you can't limit that domain with a type that
doesn't cover ALL programs.
- Response: Imposing a type discipline on the computational model
(e.g., typed lambda calculus) restricts self-reference. In such
systems, Strachey_P is invalid, and the proof does not hold.
But you need to impose a VALID type system. A Prgram defined to take
as an input *ALL* programs (via their description) must still take in
*ALL*
programs to be valid for its definition.
- Limitation: This refutation targets Strachey’s specific
construction and does not disprove the halting problem’s
undecidability, which is supported by other proofs (e.g., Turing
1936).
Whch means you really are admitting you aren't doing anything,
---
4. Conclusion Based on the assumption that self-referential
conflation is a type error, Strachey’s 1965 proof is refuted. The
program Strachey_P is ill-formed due to the type error in
T(Strachey_P), invalidating the contradiction. This highlights the
role of type systems in computational arguments and shows that
Strachey’s proof fails in typed contexts where self-reference is
restricted.
Right, based on a false assumption you can prove a false claim.
Congradulations, you just proved that bad logic leads to bad
conclusions, and that your "type system" just isn't a useful tool the
way you are using it.
It seems you only have a hammer, and thus see everything as a Nail,
even if it is actually a screw.
A circular dependency is like a circular argument or circular
reasoning:
not logically sound.
A circular argument is not like a circular argument. A circular argument
means either that there is an unjustified assumption and thus the
argument is fallacious or that the proof is redundant and therefore not
needed.
Dependency is not a logical concept. Statements of dependency always
involve an extra-logical knowledge or assumption. Whether such
statements are are true or false must be determined from such
extra-logical knowledge or assumptions with valid use of logic.
Do you take milk and sugar with your extra-logical tea?
| Sysop: | Keyop |
|---|---|
| Location: | Huddersfield, West Yorkshire, UK |
| Users: | 715 |
| Nodes: | 16 (0 / 16) |
| Uptime: | 166:26:45 |
| Calls: | 12,096 |
| Calls today: | 4 |
| Files: | 15,001 |
| Messages: | 6,517,807 |