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?