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

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.