summaryrefslogtreecommitdiffstats
path: root/content/zettel/3a5a.md
blob: 797451271ff32405b7348a17f67683ca3716c5aa (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
+++
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.