Bisimulation: add a note about requirements of bisimulation

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]>
plfa · Nov 10, 2022 · 6ee5377 · 6ee5377
1 parent 0f4501f
commit 6ee5377
Showing 1 changed file with 5 additions and 1 deletion.
diff --git a/src/plfa/part2/Bisimulation.lagda.md b/src/plfa/part2/Bisimulation.lagda.md
@@ -57,9 +57,13 @@ in the target:
 This stronger condition is known as _lock-step_ or _on the nose_ simulation.
 
 We are particularly interested in the situation where there is also
-a simulation from the target to the source: every reduction in the
+a simulation from the target to the source, using the inverse relation `~⁻¹`:
+every reduction in the
 target has a corresponding reduction sequence in the source.  This
 situation is called a _bisimulation_.
+It's important to note that two simulations do not always give rise to a
+bisimulation in general, the underlying relation of two simulations needs to be
+inverse of each other to have a bisimulation.
 
 Simulation is established by case analysis over all possible
 reductions and all possible terms to which they are related.  For each