From 2f5f1337edf287a45b2e9c77a75d57848d5da499 Mon Sep 17 00:00:00 2001 From: Fangyi Zhou Date: Thu, 10 Nov 2022 13:31:09 +0000 Subject: [PATCH] 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 --- src/plfa/part2/Bisimulation.lagda.md | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/plfa/part2/Bisimulation.lagda.md b/src/plfa/part2/Bisimulation.lagda.md index 16e2c3afc..83676cce6 100644 --- 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