+++
title = "Bisimulation"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3a5"]
forwardlinks = ["3a5b"]
zettelid = "3a5a"
+++

The strongest property to prove is bisimulation, meaning the following
property holds for some behaviour *B*.

$\forall B,\ S \Downarrow B \iff C \Downarrow B$

However, this is too strong for the notion of semantic preservation of
the compiler, because that means that both the source and compiled
output languages have to be deterministic.