# Strategy / Technique for Proving Equivalence between Multiple Program Forms

Wondering how to prove different compiled forms of a program to be "effectively the same" or "equivalent".

For example, you can have a program represented as your normal nested function calls, or have the same program represented as a state machine.

In addition, you can inline all of your functions, or leave them nested as is.

This gives 4 combinations:

• nested
• functions
• state machine
• flattened/inlined
• functions
• state machine

All of these are effectively the same program. For the nested program, it might look like this:

- function1
- function2
- functionA
- function3
- function4
- functionB
- functionC
- function5
- functionB
- functionB
- functionA
- function6
- functionC
- functionB


For the inlined "atomic" functions (A, B, and C), you get:

- functionA
- functionB
- functionC
- functionB
- functionB
- functionA
- functionC
- functionB


You can then have both of these as state machine formats.

I am wondering what the general strategy is for proving these forms are equivalent / isomorphic / homomorphic / etc.. Or maybe the strategy is to apply Model Checking (actually no, model checking requires that the program be in state transition system form).

It would be nice to, during debugging, evaluate the program as you have written it (nested functions), but in production to perhaps run it as an inlined state machine, knowing you will get the exact same results.

• In general, the problem is undecidable. (There should be some verification techniques to prove equivalence in the literature, I guess, but I am not familiar with those.) – chi Jul 2 '18 at 13:34