Skip to content

Enumeration and Dovetailing

Semi-decision procedure — instantiates Computability Boundary Mapping

Semi-decides a class by fairly interleaving all candidate computations, halting "yes" the moment one succeeds and otherwise running on — buying a complete yes-side at the cost of no honest "no".

Between "decidable" and "hopeless" lies a class of problems that are recognizable but not decidable: you can confirm a yes-instance but can never, in general, confirm a no. Enumeration and Dovetailing is the procedure that extracts the most from that regime. It enumerates every candidate computation and interleaves them fairly — dovetailing — so that if a witness exists anywhere, it is eventually found and the procedure halts with "yes." Its defining trade is deliberately lopsided: it guarantees a complete, honest answer on the yes-side, and in exchange gives up the no-side entirely — on a no-instance it simply runs forever. It never returns a false "yes," and it never returns "no" at all.

Example

Is a given first-order logic sentence valid — true under every interpretation? Validity is semi-decidable, and dovetailing is how you recognize it. Enumerate all finite proofs in a complete proof system, interleaving them so that no single long proof-search starves the others of time. If the sentence is valid, a proof of it exists and will eventually surface, at which point the procedure halts and reports "valid." If the sentence is not valid, no proof exists, the enumeration never finds one, and the search runs on forever — never delivering a definite "invalid." The recognizer is complete for validity and structurally silent on invalidity; the best it can honestly say about a running no-instance is "not yet."

How it works

The distinguishing device is dovetailing: rather than run candidate 1 to completion — which may never halt and would block everything behind it — the procedure runs one step of candidate 1; then a step each of 1 and 2; then 1, 2, and 3; and so on, so every candidate receives unbounded time and no non-halting candidate can starve the rest. It halts the instant any candidate succeeds. Because a definite "no" is structurally unreachable, the procedure must carry an explicit third state — still running / unknown — and must never let elapsed time masquerade as a negative verdict.

Tuning parameters

  • Enumeration order — which candidates are visited first. A good order surfaces common witnesses fast without ever dropping one, since completeness requires that every candidate is eventually reached.
  • Dovetailing schedule — how compute is shared across active candidates. The schedule must stay fair: starve some candidates and you silently forfeit the completeness that is the method's entire point.
  • Resource cap and unknown policy — whether to run unbounded or cut off with an explicit "unknown" after a budget. Capping makes the procedure usable in practice but must report a truthful "unknown," never a fabricated "no."
  • Witness retention — whether success returns the found proof or program, or merely the fact of success. Returning the witness makes the "yes" independently checkable.

When it helps, and when it misleads

Its strength is an honest, complete recognizer for the yes-side of a class that no decider can handle — it never claims a false "yes," and it never claims a false "no" for the simple reason that it never claims "no" at all. Its failure modes follow from that: unbounded non-termination on no-instances, where you genuinely cannot tell "no" from "not yet," and a subtle loss of completeness if the schedule stops being fair. The classic misuse is reading a timeout as "no" — converting an honest "unknown" into a false negative — or trading away fairness for speed and thereby missing reachable witnesses. The discipline is to remember that a recursively enumerable / semi-decidable[1] class admits recognition, not decision: keep the "unknown" state explicit and the dovetailing schedule fair.

How it implements the components

  • one_sided_recognition_contract — it delivers exactly a one-sided recognizer: it halts and confirms on yes-instances and never falsely rejects, precisely because it never rejects at all.
  • unknown_and_nontermination_policy — its behavior on no-instances is non-termination, so it must carry an explicit "unknown / still running" policy in place of the "no" it structurally cannot give.

It recognizes but does not decide — the finite, fully-decidable case belongs to Bounded-Domain Exhaustive Search, a sound terminating approximation to Abstract Interpretation or Model Checking, and the proof that the class is only semi-decidable comes from Diagonalization Impossibility Proof.

Notes

The closest sibling is Semi-Decision with Explicit Unknown, and the division of labour is worth keeping straight: this mechanism is the engine — how you fairly search an unbounded candidate space without getting stuck — while the semi-decision sibling is the contract that governs how the resulting "yes / unknown" verdict is reported and consumed. Use dovetailing to find the witness; use the explicit-unknown contract to keep the missing "no" honest downstream.

References

[1] A recursively enumerable (semi-decidable) set is one whose members can be listed by a procedure that halts on members but may run forever on non-members — so membership can be recognized but not decided. First-order validity is the canonical example. ↩