Skip to content

Semi-Decision with Explicit Unknown

Semi-decision protocol — instantiates Computability Boundary Mapping

Runs a sound one-sided recognizer that confirms YES when it can, but returns an explicit UNKNOWN at a declared resource bound instead of looping forever or faking a NO.

Semi-Decision with Explicit Unknown wraps a one-sided recognizer so it always returns a usable answer. A semi-decision procedure can confirm membership when it holds — it will eventually say YES for a true yes-instance — but may run forever on a no-instance, never able to certify NO. This protocol keeps the sound YES and replaces the forever-loop with an explicit, honest UNKNOWN emitted at a declared resource bound, so the caller receives exactly one of {YES, UNKNOWN} and the procedure always halts. Its defining move is that it refuses to fake a NO: where a naive checker guesses "no" when it gives up, this one distinguishes "confirmed yes" from "couldn't confirm" and treats the second as an admission, never a decision.

Example

A number-theory tool answers "does this Diophantine equation have a positive-integer solution?" Existence of integer solutions is undecidable in general — Hilbert's tenth problem — but the yes-side is semi-decidable: if a solution exists, a systematic search over candidate tuples will eventually reach it. The tool runs that search and, on finding a solution, returns YES together with the witnessing values. Because it can never be sure no solution exists, it neither loops forever nor reports a false NO; after a declared budget — a candidate ceiling or a wall-clock limit — it returns UNKNOWN. A downstream planner reads UNKNOWN as "unresolved: escalate, or widen the budget and retry," never as "no solution exists." The tool is total (it always halts) over a problem that has no total decider, and it is honest in exactly the place a lesser tool would manufacture certainty.

How it works

  • Run the sound yes-side recognizer — the search or check that can only ever confirm membership.
  • On confirmation, return YES, ideally carrying a checkable witness.
  • Enforce a termination condition — a bound on steps, time, or search depth — that guarantees the procedure halts.
  • On hitting the bound unconfirmed, return UNKNOWN — never NO.

The honesty is structural, not a matter of discipline: the output alphabet has no unqualified NO in it, so a caller cannot mistake exhaustion of the budget for refutation.

Tuning parameters

  • Resource bound — the budget after which UNKNOWN is emitted; a larger bound resolves more instances but costs more and still never certifies NO.
  • Search strategy — how the yes-side is explored (breadth-first, dovetailed, heuristic-guided); it changes which yes-instances get confirmed within the budget, never soundness.
  • Witness requirement — whether a YES must carry a checkable witness; witnesses make each YES independently verifiable at some bookkeeping cost.
  • Unknown semantics — whether UNKNOWN is terminal or a request for a larger budget or a different mode; the latter turns the procedure into one stage of a router.

When it helps, and when it misleads

Its strength is that it delivers a total, always-halting procedure over a problem with no total decider, and its UNKNOWN is truthful in precisely the spot where a naive tool would fabricate a NO.

Its failure modes are the mirror of that honesty. UNKNOWN can be over-produced — a too-small budget makes almost everything UNKNOWN, leaving the tool always correct and rarely useful — and the one-sidedness is asymmetric: it confirms YES but never NO, so it must never be wired into a context that reads a non-YES as NO.[1] The classic misuse is doing exactly that downstream — silently collapsing UNKNOWN into NO — which reintroduces the false certainty the protocol exists to prevent. The discipline is to propagate UNKNOWN as a first-class value all the way to wherever the decision is finally made.

How it implements the components

Semi-Decision with Explicit Unknown fills the honest-recognition side of the archetype — the components a one-sided, always-halting recognizer produces:

  • one_sided_recognition_contract — it honours a one-sided contract: sound and eventually-complete on the YES side, silent on the other, so it confirms but never refutes.
  • unknown_and_nontermination_policy — it converts potential nontermination into a declared UNKNOWN output, the policy that swaps an infinite loop for an honest admission.
  • termination_condition — the declared resource bound is the termination condition that forces a halt and triggers the UNKNOWN.

It does not route the UNKNOWN onward or pick the next method — that dispatch is Fallback-Mode Router — and it does not supply the raw search it runs on, which Enumeration and Dovetailing provides.

  • Instantiates: Computability Boundary Mapping — delivers a total, honest procedure on the far side of the boundary rather than a false total decider.
  • Consumes: Enumeration and Dovetailing supplies the underlying yes-side search this protocol bounds and wraps.
  • Sibling mechanisms: Fallback-Mode Router · Promise-Problem Restriction · Enumeration and Dovetailing · Abstract Interpretation or Model Checking

Notes

The mirror-image procedure — sound on NO, honest UNKNOWN, never a false YES — is equally valid; choose whichever side you can actually make sound. What you cannot have is a procedure sound on both YES and NO for an undecidable problem: that is just a total decider by another name, and for such a problem it cannot exist. The explicit UNKNOWN is the price of that impossibility, paid honestly.

References

[1] A set is semi-decidable (recursively enumerable) when a procedure can confirm membership for every element that belongs, but may never halt on elements that do not. Diophantine solvability — Hilbert's tenth problem — is the classic case: solutions can be found by search, but their nonexistence cannot in general be certified. ↩