Lukas' Notes

Search titles, aliases and note text. Use # for tags.

Correctness Problem

2 min read

computation

Definition

Correctness Problem

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

It is undecidable and semi-decidable.

Properties

Undecidability

Undecidability of Correctness Problem

The correctness problem is undecidable.

Given an instance of the halting problem, construct an instance of the correctness problem, where and 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 ( )

If halts on input , then the constructed program also halts on input and outputs . Hence is a positive instance of the correctness problem.

Soundness ( )

If is a positive instance of the correctness problem, then halts on input and outputs . By construction, can only output after has halted on input . Hence is a positive instance of the halting problem.

Backlinks