Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Bisimulation: add a note about requirements of bisimulation #785

Draft
wants to merge 1 commit into
base: dev
Choose a base branch
from
Draft

Bisimulation: add a note about requirements of bisimulation #785

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 5 additions & 1 deletion src/plfa/part2/Bisimulation.lagda.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down