Given a program, finding another program that has the same input to output map is much easier than given two programs, determining if they have the same input to output map.
This is interesting. Do you have any sources that discuss why this is so?
I have a short proof: suppose we have some program, A. And some program that provably does nothing, B.
Run first B, then A. Presto, a new program with output identical to A. Depending on whether A is a black box or some structure you can reason about, you can also hoist B up into the body of A. Again, provably output identical to A.
The underlying reason this is easier than proving general equivalence of programs is that we picked specific program B with a well-known behavior. Trying to prove two programs equivalent would be trying to reason about all possible modifications, rather than some one specific patch.
I have a short proof: suppose we have some program, A. And some program that provably does nothing, B.
Run first B, then A. Presto, a new program with output identical to A. Depending on whether A is a black box or some structure you can reason about, you can also hoist B up into the body of A. Again, provably output identical to A.
The underlying reason this is easier than proving general equivalence of programs is that we picked specific program B with a well-known behavior. Trying to prove two programs equivalent would be trying to reason about all possible modifications, rather than some one specific patch.