Path: news.eternal-september.org!eternal-september.org!.POSTED!not-for-mail From: Mikko Newsgroups: comp.theory Subject: =?utf-8?Q?Re:_Refutation_of_Strachey=E2=80=99s_1965_Proof_Based_on_Self-Referential_Conflation_as_a_Category_(Type)_Error?= Date: Tue, 22 Apr 2025 11:39:42 +0300 Organization: - Lines: 189 Message-ID: References: <3%oNP.2703666$nb1.805417@fx01.ams4> <130c384bc4881eb654343d0ccf3ced6905a90fbb@i2pn2.org> <3QpNP.1081604$B61.671277@fx02.ams4> MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 8bit Injection-Date: Tue, 22 Apr 2025 10:39:42 +0200 (CEST) Injection-Info: dont-email.me; posting-host="958cb6175161903e9793602f5c1d3304"; logging-data="254074"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX19hRDMBHO+gviuK53HE/xAR" User-Agent: Unison/2.2 Cancel-Lock: sha1:1b2qE1xCa8rEzC1iNpJXCKY/Kys= 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 ========== REMAINDER OF ARTICLE TRUNCATED ==========