Sujet : Re: Analysis of Richard Damon’s Response – 2025-05-23
De : richard (at) *nospam* damon-family.org (Richard Damon)
Groupes : comp.theoryDate : 24. May 2025, 02:43:28
Autres entêtes
Organisation : i2pn2 (i2pn.org)
Message-ID : <b52a2b4880d5989cae025ecd86b4019cec3742b7@i2pn2.org>
References : 1
User-Agent : Mozilla Thunderbird
On 5/23/25 5:38 PM, Mr Flibble wrote:
Analysis of Richard Damon’s Response – 2025-05-23
=================================================
Overview:
---------
Richard Damon’s response reiterates his classical view that non–Turing
complete systems are not interesting for computability. While correct
within traditional computability theory, this perspective fails to
recognize the practical relevance and modern utility of Flibble’s proposal—
namely, typed Simulating Halt Deciders (SHDs) using the neos framework.
Damon misinterprets the purpose and context of Flibble’s ideas and
undervalues type-safe computation models.
1. Turing Completeness as the Sole Criterion
--------------------------------------------
Damon: "Virtually all questions about COMPUTABILITY are about
computability by Turing Machines."
True in classical theory, but irrelevant in many practical domains like:
- Type-safe verification
- Total functional programming
- Formal proof systems
Flibble is not arguing within classical theory, but offering an
alternative semantic model that avoids paradox by design.
Then stop making comments about The Halting Problem in Computation Theory.
2. Mischaracterization of Type Theory
-------------------------------------
Damon: "Full type theory ALSO requires Turing Completeness..."
False. Systems like Coq and Agda are not Turing complete and are
intentionally restricted for logical soundness. They enforce termination
and stratify universes to prevent paradoxes.
Which are both very limited system processors. Both deal with proving theorems in limited logic systems.
Damon conflates unrestricted computation with type theory, which misses
the purpose of total functional languages and proof assistants.
But full type theory
3. Invalidity ≠ Evasion
------------------------
Damon: "He defines any program that he can't handle as INVALID."
Yes, because Flibble's model imposes semantic constraints. Just as type
checkers reject invalid programs, so too does the typed SHD framework.
This is a protective design, not an evasion.
But that is not the model that people think of when you say "program". Note, once you mention "The Halting Problem", you have put yourself into the broader context of Computation theory, and thus its definition of Program.
This is your problem, your statements just equivocate on the meaning of the words.
4. On Deciders in Programs
--------------------------
Damon: "Programs can't know that something is trying to decide on
them..."
True. But in the Halting Problem, we *simulate* this reference. Flibble
blocks such simulations through stratification, similar to how meta-theory
avoids circularity.
No, The Halting Problem says NOTHING about simulating the "reference".
And thus, Flibble system just breaks when meeting the Halting Problem, as it DEFINES the problem as making a PROGRAM that can decide on PROGRAMS.
If Flibble theory can't handle this, it can't handle the Halting Problem.
PERIIOD.
5. Practicality of Typed SHDs
-----------------------------
Damon: "By forbidding the accessing of deciders in programs, you make
deciders mostly worthless."
No. Deciders remain useful at the meta-level—just like proof checkers and
type validators. They analyze programs externally, not internally.
So, how do you check that your checker is valid?
This preserves decidability while avoiding paradoxes caused by internal
self-reference.
At the cost of making the system under study "small".
6. Flibble's Goal
-----------------
Flibble does not aim to:
- Solve the classical Halting Problem.
- Replace Turing computation.
He aims to:
- Restrict the domain to well-typed, semantically sound programs.
- Prevent malformed constructions.
- Provide analyzable, decidable semantics for safe programs.
Then stop talking about the things you don't intend to talk about.
7. Damon’s Overreach
---------------------
- Conflates philosophical critique with deceit (“you lied”).
- Ignores the relevance of modern type systems in industry.
- Assumes classical theory is the only valid basis for program analysis.
No, when you intentionaly conflate meaning, YOU LIE.
Conclusion:
-----------
Damon's response is valid inside classical computability but fails to
engage with Flibble’s semantic reframing. Flibble proposes a useful, well-
scoped, and philosophically sound alternative to unrestricted computation—
one that prioritizes soundness, static analysis, and decidability over
maximal expressiveness.
Flibble’s model is a contribution to modern formal methods, not a
replacement for classical computation. Damon’s critiques, while
technically sharp, are misapplied in this broader context.
But why does the world need your "theory", when the field already has well established theories in the domain of the reduced field type theory looks at.
Your problem is that you have been taken in by Olcott's misrepresentations, and haven't looked at what is actually currently done.
He lies about having "invented" concepts that are many decades old.