Bisimulation: add a note about requirements of bisimulation

[fangyi-zhou]

Two simulations only form a bisimulation when the underlying relation are inverses of each other:
https://cs.stackexchange.com/questions/541/when-are-two-simulations-not-a-bisimulation

This commits adds clarification over the matter, by emphasising the inverse requirement.

Signed-off-by: Fangyi Zhou [email protected]

[wadler]

Thank you. You are correct, the current discussion is too compact. But I think the sudden reference to ~⁻¹ may be confusing to students. I'll have a think about the best way to explain.

[fangyi-zhou]

Thanks for the reply. I agree that the current way to present this subtlety is probably not the best.
Ideally, we first introduce the concept/definition of bisimulation:

Simulation: For every M, M†, and N: If M ~ M† and M —→ N then M† —↠ N† and N ~ N† for some N†.
Bisimulation: For every M, M†, and N: Suppose M ~ M†, if (1) M —→ N then M† —↠ N† and N ~ N† for some N†, and (2) if M† —→ N† then M —↠ N and N ~ N† for some N

then the difference between 2-simulation and bisimulation?