I am not claiming to solve the Halting Problem. The narrower claim is that one particular shape inside the diagonal argument is worth isolating: a system consumes a prediction about its own current execution, then uses that prediction to control that same execution.
In symbols:
execution -> prediction about that execution -> control of that same execution
I have been calling this pattern Causal Halting. The distinction matters for agent designs with supervisors, monitors, self-evaluation, or retry logic.
Suppose an agent asks a supervisor, during the current run:
Will this run finish?
The supervisor predicts “no”, and the same run changes strategy because of that answer.
This is not just monitoring. The prediction has become part of the causal structure of the thing it predicted:
E = current execution
R = result of predicting E
E -> R -> E
A supervisor observing a run is fine. An external orchestrator stopping a run is fine. A later retry using information from a previous run is fine. The odd case is the current execution consuming a prediction about itself as a control input. That is the boundary I want to make explicit.
Why this resembles diagonalization
Turing’s diagonal proof constructs a program that queries a halting predictor about its own behavior and then inverts the result:
D(y) =
if H(y,y) predicts "halts" then loop
else halt
Running D(D) produces the contradiction. I agree with the usual conclusion: the predictor cannot exist.
But the diagonal also has a specific information-flow shape:
execution of D(D)
-> prediction about D(D)
-> control of D(D)
My question is not “can we beat Turing?” It is: what if this feedback path is treated as a type error rather than as ordinary data flow?
Here is the minimal sketch. Separate four roles:
Code inert program description
Exec live execution event
H halting observation operator
HaltResult causal token produced by H
The key rule is that HaltResult is not ordinary data. It cannot be passed into opaque code or treated as a normal value. It can be discarded, or used by a special branch that records a causal edge.
Observation adds:
E(p,a) -> R(p,a)
Branching on that result inside the current execution adds:
R(p,a) -> E(current)
So the forbidden pattern is:
E(p,a) -> R(p,a) -> E(p,a)
Running D(D) creates exactly this cycle. In this calculus, the diagonal computation is not merely undecidable; it is causally ill-typed.
This is also where the idea can easily be overstated, so here is the counterexample that keeps it honest.
The sanity check
Let e be an ordinary program. Define:
Q_e() =
simulate e(e)
if e(e) halts, halt
else diverge
Q_e uses no H. It does not ask a predictor about its own current execution. Its causal graph is empty, so it is not a causal paradox.
But deciding Q_e for all e would decide the classical Halting Problem.
So ordinary undecidability survives. The distinction is:
This is not a way around Turing. It is a way to avoid putting two different failures in the same bucket.
Is this just renaming?
This is the objection I am most worried about.
Maybe causal_paradox is just a name for “the cases my type system refuses to express.” If so, the contribution is much weaker. A skeptic could say: of course diagonalization disappears after banning the diagonal move. You have not explained undecidability; you have only made one construction illegal.
My reply is not that this defeats the objection. It only narrows the claim.
I think the useful part is not “CHC-0 proves a new limit theorem.” The useful part is that prediction-feedback and semantic hardness behave differently:
the feedback case is visible in a causal graph;
the Q_e case is causally clean but still semantically hard;
stronger proof systems may shrink the unproved set, but they do not change whether a given graph has a feedback cycle.
That feels like structure, not just terminology. But I am not fully confident. It may already be captured cleanly by non-interference, session types, linear logic, or process calculi under a better name.
Agent design implication
For practical agents, I want a simple design heuristic:
Do not let the current execution consume a prediction about itself
as a control input to itself.
Use a supervisor if needed. Use a watchdog. Use an orchestrator. But keep the roles separated:
AgentRun emits progress.
Supervisor observes progress.
External orchestrator decides whether to stop, restart, or schedule a later run.
This may be more architectural hygiene than deep computability theory. It still seems like a useful warning label for agent loops.
I built a small checker for explicit causal graphs, mostly to keep myself honest about the formal shape.
The current checker also handles the first operational extensions: recursive causal summaries and higher-order callbacks with explicit effect annotations. There are now structured checks for process/session descriptions, temporal traces, and probabilistic prediction results.
The current version also has a more practical pipeline:
The scripts do not classify natural language directly. The language model has to write down the causal roles first: what is running, what is observed, what result is produced, and who consumes that result. Only that structured artifact is checked.
There are also small adapters for explicitly annotated OpenTelemetry and LangGraph-style traces. I do not want to oversell that part; the adapters are only useful when the trace already exposes the causal roles.
The latest version also forces the output to say what it is not proving.valid_acyclic only means “no modeled prediction-feedback cycle was found.” It does not mean the agent terminates, is safe, or is correct.
I would especially appreciate feedback on whether this is already a known concept in a cleaner framework, and whether the agent-design heuristic matches any real failure modes people have seen.
Disclosure: The original idea is mine, but it was developed through several rounds of discussion with Codex and Claude. I used them to challenge the framing, refine the argument, and edit the post. The code and final responsibility are mine.
Prediction Feedback Is Not the Same as Undecidability
I am not claiming to solve the Halting Problem. The narrower claim is that one particular shape inside the diagonal argument is worth isolating: a system consumes a prediction about its own current execution, then uses that prediction to control that same execution.
In symbols:
I have been calling this pattern Causal Halting. The distinction matters for agent designs with supervisors, monitors, self-evaluation, or retry logic.
Suppose an agent asks a supervisor, during the current run:
The supervisor predicts “no”, and the same run changes strategy because of that answer.
This is not just monitoring. The prediction has become part of the causal structure of the thing it predicted:
A supervisor observing a run is fine. An external orchestrator stopping a run is fine. A later retry using information from a previous run is fine. The odd case is the current execution consuming a prediction about itself as a control input. That is the boundary I want to make explicit.
Why this resembles diagonalization
Turing’s diagonal proof constructs a program that queries a halting predictor about its own behavior and then inverts the result:
Running
D(D)produces the contradiction. I agree with the usual conclusion: the predictor cannot exist.But the diagonal also has a specific information-flow shape:
My question is not “can we beat Turing?” It is: what if this feedback path is treated as a type error rather than as ordinary data flow?
Here is the minimal sketch. Separate four roles:
The key rule is that
HaltResultis not ordinary data. It cannot be passed into opaque code or treated as a normal value. It can be discarded, or used by a special branch that records a causal edge.Observation adds:
Branching on that result inside the current execution adds:
So the forbidden pattern is:
Running
D(D)creates exactly this cycle. In this calculus, the diagonal computation is not merely undecidable; it is causally ill-typed.This is also where the idea can easily be overstated, so here is the counterexample that keeps it honest.
The sanity check
Let
ebe an ordinary program. Define:Q_euses noH. It does not ask a predictor about its own current execution. Its causal graph is empty, so it is not a causal paradox.But deciding
Q_efor allewould decide the classical Halting Problem.So ordinary undecidability survives. The distinction is:
This is not a way around Turing. It is a way to avoid putting two different failures in the same bucket.
Is this just renaming?
This is the objection I am most worried about.
Maybe
causal_paradoxis just a name for “the cases my type system refuses to express.” If so, the contribution is much weaker. A skeptic could say: of course diagonalization disappears after banning the diagonal move. You have not explained undecidability; you have only made one construction illegal.My reply is not that this defeats the objection. It only narrows the claim.
I think the useful part is not “CHC-0 proves a new limit theorem.” The useful part is that prediction-feedback and semantic hardness behave differently:
the feedback case is visible in a causal graph;
the
Q_ecase is causally clean but still semantically hard;stronger proof systems may shrink the unproved set, but they do not change whether a given graph has a feedback cycle.
That feels like structure, not just terminology. But I am not fully confident. It may already be captured cleanly by non-interference, session types, linear logic, or process calculi under a better name.
Agent design implication
For practical agents, I want a simple design heuristic:
Use a supervisor if needed. Use a watchdog. Use an orchestrator. But keep the roles separated:
This may be more architectural hygiene than deep computability theory. It still seems like a useful warning label for agent loops.
I built a small checker for explicit causal graphs, mostly to keep myself honest about the formal shape.
The current checker also handles the first operational extensions: recursive causal summaries and higher-order callbacks with explicit effect annotations. There are now structured checks for process/session descriptions, temporal traces, and probabilistic prediction results.
The current version also has a more practical pipeline:
The scripts do not classify natural language directly. The language model has to write down the causal roles first: what is running, what is observed, what result is produced, and who consumes that result. Only that structured artifact is checked.
There are also small adapters for explicitly annotated OpenTelemetry and LangGraph-style traces. I do not want to oversell that part; the adapters are only useful when the trace already exposes the causal roles.
The latest version also forces the output to say what it is not proving.
valid_acycliconly means “no modeled prediction-feedback cycle was found.” It does not mean the agent terminates, is safe, or is correct.https://github.com/chrystyan96/causal-halting
Project page:
https://chrystyan96.github.io/causal-halting/
I would especially appreciate feedback on whether this is already a known concept in a cleaner framework, and whether the agent-design heuristic matches any real failure modes people have seen.
Disclosure: The original idea is mine, but it was developed through several rounds of discussion with Codex and Claude. I used them to challenge the framing, refine the argument, and edit the post. The code and final responsibility are mine.