Re: Seeking for papers about tagged types vs access to subprograms

["Peter C. Chapin" <PChapin@vtc.vsc.edu>]

On Fri, 17 May 2013, Niklas Holsti wrote:

> A proof seems simple enough, assuming that the set of inputs is infinite 
> and enumerable: if you want to decide whether f1 and f2 are equivalent, 
> make a program P that iteratively generates (enumerates) all possible 
> inputs x; computes f1(x) and f2(x); and stops if f1(x) /= f2(x). This 
> program P halts if and only if f1 /= f2. Since halting is undecidable, 
> so therefore is function equality.

You've shown that the method of enumerating all possible argument values 
and testing f1(x) = f2(x) doesn't work. But perhaps there is some clever 
way to statically analyze the code of f1 and f2 to decide their 
equivalence without having to actually evaluate the functions for all 
possible inputs.

I did a quick Google search on this out of curiosity and it turns out 
there is a body of work in this area related to optimization. That makes 
sense. Optimizers would like to make transformations on a given function 
that generate provably equivalent functions (that are faster or smaller, 
etc). It's easy to see why people into optimization would care about this.

I could imagine some sort of conversation that takes a function to a kind 
of canonical form... maybe repeated applications of certain primitive 
transformations on the code... and then showing equivalence would be a 
matter of comparing the text of the canonical forms of the two functions. 
I doubt it can be done (in general), but it's not immediately obvious to 
me that it can't.

On the other hand, to prove undecidability one could use a reduction 
approach. Assume I had a Turing machine program that could take as input 
two functions (expressed also as Turing machine programs) <f1> and <f2>, 
and accept that input if the two functions are equivalent, rejecting it 
otherwise. Now show how one could transform an arbitrary instance of some 
known undecidable problem, using a Turing machine and in finite time, to 
an instance of the equivalence checking problem. If such a transformation 
could be found, the equivalence checking problem would also be undecidable 
since a solver for it would imply a solver for the original undecidable 
problem.

Niklas, your approach actually does the reduction in the wrong direction. 
You showed how one can transform an instance of the equivalence checking 
problem into an instance of the halting problem. However, that doesn't 
allow you to conclude equivalence checking is undecidable. Maybe that's 
just the wrong way to do it.

Peter