# Program equivalence wherein the programs are known to always halt

Say I have two programs with possibly infinite state spaces and some oracle has asserted that they both always halt. Can I always decide if they're contextually equivalent? If yes, is there a known effective algorithm (or approach that when applied on a case-by-case or language-by-language basis provides an effective algorithm) to do so?

The answer is obviously yes/yes for finite input domains, but for infinite input domains: does the decidability depend at all on how infinitely huge (e.g. countable vs. uncountable) the input domains are?

• This is related to (actually, it is basically a duplicate of) this question. – Damiano Mazza Dec 12 '17 at 21:43
• @DamianoMazza Youch - burned by isomorphism. I'll claim the upper hand in searchable keywords, however. :-P – user Dec 13 '17 at 10:21
• Yes, it can be very hard to find out if a question (or something similar) has already been asked. Sometimes I even have problems retrieving questions I know have been asked! :-) Your question will definitely be easier to find! – Damiano Mazza Dec 13 '17 at 13:13

As a counter-example to this, consider the Context-Free Equivalence problem: it's undecidable to determine, given two context free languages, whether they accept the same set.

If your problem were decidable, we could use it to determine CFL equivalence, since it's always possible to turn a CFL into an always-halting Turing machine.

So even for countably infinite inputs, the problem is undecidable.

It's also worth mentioning that, for standard Turing Machines, all input domains are countably infinite, since they're sets of finite strings.

• Cool, thanks - but re: the last bit: if I have infinite sized inputs (e.g. streams), can't I diagonalize and show that the set of possible inputs is uncountable? (Or am I mis-remembering what an 'input' is allowed to be? I'd think a machine need not look at its whole input - but I could be very wrong and confused) – user Dec 9 '17 at 7:52
• Oh, nvm, you qualified that with 'standard Turing Machines'. – user Dec 9 '17 at 8:00

Consider programs $e_1$, $e_2$ and numbers of time steps $t$.

Let $f_i(t)$ be the output of $e_i$ after $t$ steps, and let $f_i(t)$ output a special message like "none" if there's no output yet.

Then $f_1$ and $f_2$ both always halt, but you can't decide if they always output the same - see Rice's Theorem.

• Would you mind clarifying for me the applicability of Rice's theorem? My reading of the proof sketch by reduction to the halting problem on Wikipedia has that proof inapplicable because my oracle already said they halt, so there's no way to make that reduction (the arbitrary program must halt because my oracle said the enveloping program halts, else I wouldn't be trying to evaluate the equivalence). I haven't quite grokked the other proofs yet. – user Dec 9 '17 at 22:41
• Nevermind, I misread your answer. It might be worth emphasizing that because we're discriminating between 'none' and a value as $t$ goes to $\infty$ we're therefore deciding the halting problem. – user Dec 9 '17 at 23:56
• @user exactly right – Bjørn Kjos-Hanssen Dec 10 '17 at 1:09