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

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