Re: Refutation of Strachey’s 1965 Proof Based on Self-Referential Conflation as a Category (Type) Error

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