1
$\begingroup$

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.

Improve this question
$\endgroup$
1
  • $\begingroup$ 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.) $\endgroup$
    – chi
    Jul 2, 2018 at 13:34

0

Reset to default

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.