On the complexity of the correctness problem for non-zeroness test instruction sequences

TL;DR

This paper investigates the computational complexity of verifying whether simple instruction sequences correctly perform the non-zeroness test on natural numbers, revealing the difficulty of correctness verification in this context.

Contribution

It establishes the time complexity of correctness verification for instruction sequences implementing the non-zeroness test, under various restrictions, for all natural number inputs.

Findings

Correctness verification is computationally complex.

Time complexity varies with sequence restrictions.

Results apply to functions from binary strings to binary outputs.

Abstract

This paper concerns the question to what extent it can be efficiently determined whether an arbitrary program correctly solves a given problem. This question is investigated with programs of a very simple form, namely instruction sequences, and a very simple problem, namely the non-zeroness test on natural numbers. The instruction sequences concerned are of a kind by which, for each $n > 0$, each function from $\{0,1\}^n$ to $\{0,1\}$ can be computed. The established results include the time complexities of the problem of determining whether an arbitrary instruction sequence correctly implements the restriction to $\{0,1\}^n$ of the function from $\{0,1\}^*$ to $\{0,1\}$ that models the non-zeroness test function, for $n > 0$, under several restrictions on the arbitrary instruction sequence.