semidecision

Semidecision, also known as semi-decidability or partial decidability, is a concept in computability theory describing a property of certain decision problems. A problem is considered semidecidable if there exists an algorithm, typically a Turing machine, that on input x will halt and accept when x is a yes-instance, but may run forever on no-instances. Equivalently, the set of yes-instances (the language) is recursively enumerable.

In practical terms, a semidecision procedure can confirm positive answers but cannot always provide a definitive yes for negative cases. This means that while the algorithm may eventually recognize members of the language, it does not guarantee termination for inputs outside the language. Decidable problems, by contrast, have procedures that always halt with a correct yes or no answer.

A classic example is the halting problem: given a program and its input, determine whether the program halts. There is a procedure that simulates the program and halts if the program halts, but it may run forever if the program does not halt. Thus the halting problem is semidecidable but not decidable. Another example is the set of provable statements within a consistent formal system; a proof verifier can confirm provability by checking a valid proof, but it may not determine unprovability.

Semidecidable languages are precisely the recursively enumerable (r.e.) sets. The concept is central to discussions of computability, algorithmic verification, and the limits of automation. It highlights that some problems allow verification of positive instances, while universal termination for all inputs may be impossible.