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

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?