Correctness Problem

computation

Definition

Correctness Problem

The correctness problem is a decision problem that asks, for a given program $\Pi$ and two strings $I,O$, whether $\Pi$ halts on input $I$ and outputs output $O$.

It is undecidable and semi-decidable.

Properties

Undecidability

Undecidability of Correctness Problem

The correctness problem is undecidable.

Given an instance $(\Pi ,I)$ of the halting problem, construct an instance $({\Pi }^{\prime },I_1,I_2)$ of the correctness problem, where $I_1=I_2=I$ and ${\Pi }^{\prime }$ is defined as follows:

procedure Π':
  Input: input string I1, output string I2
  Output: I2 if Π halts on I1, otherwise no output
 
  simulate Π on input I1
  if Π halts then return I2
  else loop forever

Completeness ( $\Rightarrow$) If $\Pi$ halts on input $I$, then the constructed program ${\Pi }^{\prime }$ also halts on input $I_1=I$ and outputs $I_2=I$. Hence $({\Pi }^{\prime },I,I)$ is a positive instance of the correctness problem.

Soundness ( $\Leftarrow$) If $({\Pi }^{\prime },I,I)$ is a positive instance of the correctness problem, then ${\Pi }^{\prime }$ halts on input $I_1=I$ and outputs $I_2=I$. By construction, ${\Pi }^{\prime }$ can only output $I_2$ after $\Pi$ has halted on input $I_1$. Hence $(\Pi ,I)$ is a positive instance of the halting problem.