4 ms·
> Proving equivalence between programs is not computable (by easy reduction to the halting problem) It's decidedly not computable for Turing machines (because
by boomlinde 8y ago
> Proving equivalence between programs is not computable (by easy reduction to the halting problem)
It's decidedly not computable for Turing machines (because the input/output space is infinitely large), but you can theoretically compute it for any linear bounded automata.
Certainly not practical for a very large potential input space like the working memory of a PC, but if you can make a trivial enough program to constrain the memory of another and ensure determinism that it is feasibly expensive to verify manually, you can create small LBA and guarantee equivalence to the extent that you verified the constraints checker.