Sound Algorithm

Definition

Sound Algorithm

A algorithm is sound if every conclusive result it returns is correct. Given a validity relation $R\subseteq X\times Y$ and an algorithm

$$A:X\to Y\cup \{\perp \},$$

where $\perp$ denotes an inconclusive result, soundness requires

$$\forall x\in X\forall y\in Y:A(x)=y⟹(x,y)\in R.$$

For a decision predicate $P$, the one-sided forms are sound acceptance and sound rejection:

$$\begin{array}{rlrl}A(x)=\mathrm{yes}& ⟹P(x)& & \text{(acceptance)},\\ A(x)=\mathrm{no}& ⟹\neg P(x)& & \text{(rejection)},\\ A(x)& =\perp & & \text{(inconclusive and permitted)}.\end{array}$$

An algorithm is unsound when some conclusive result is false; merely being inconclusive is permitted. Conclusiveness asks whether the algorithm always answers, while soundness asks whether its answers are correct. This is the algorithmic analogue of a sound calculus.