Deciding the behavior of edited programs

I’ve been thinking about computation and program synthesis a lot recently. Program synthesis is the process of constructing a program based on constraints or example input/output pairs. This problem is extraordinarily difficult; the best methods essentially enumerate all reasonable programs, for some heuristic definition of reasonable, and run them to see if they work. In this situation, it would be convenient if, knowing what a program does, you could make a guess at what an edited version of the program does. Frustratingly, this is undecidable in general.

Suppose you have a universal Turing machine \(U\) that accepts programs in the form of bitstrings. We can define the distance \(d(A, B)\) between two bitstrings according to the Levenshtein metric: the minimum number of insertions, deletions, or substitutions necessary to transform one into the other.

Suppose there exists a halting program \(X(A, B)\) that, given programs \(A\) and \(B\) such that \(d(A, B) = 1\), returns \(1\) if \(B\) has the same halting behavior as \(A\) and \(0\) otherwise. Suppose \(P\) is some program that we know to halt. Let \(Q\) be any other program. Then, construct a chain of programs \(P, P^1, P^2, …, P^k, Q\) such that \(d(P^i, P^{i+1}) = 1\) for any \(i\) between \(1\) and \(k-1\), inclusive, and \(d(P, P^1)=d(P^k, Q)=1\). Essentially, this chain is a list of intermediate programs that we get while transforming \(P\) into \(Q\). There are many such lists, but any particular one will do. Without loss of generality, let’s suppose \(k\) is even; if \(k\) is odd, we could just take the last character \(c\) of \(P^k\) and substitute it with a \(1\), delete the \(1\), and insert \(c\) again to create \(P^{k+1}, P^{k+2}, P^{k+3}\). In this way, the sequence can always be forced to have even length.

Let’s run \(X\) on each adjacent pair of programs and record its output. Then, summing the results, it’s easy to see that \(Q\) halts if and only if the sum is odd. This is undecidable, as it solves the halting problem for an arbitrary program \(Q\), so \(X\) does not exist.

If you liked this post, you can also follow me on Twitter.