1 files changed, 25 insertions, 0 deletions
diff --git a/content/zettel/3a5b.md b/content/zettel/3a5b.md
new file mode 100644
index 0000000..a07a469
--- /dev/null
+++ b/content/zettel/3a5b.md
@@ -0,0 +1,25 @@
++++
+title = "Backward Simulation"
+author = "Yann Herklotz"
+tags = []
+categories = []
+backlinks = ["3a5a"]
+forwardlinks = ["3a5c"]
+zettelid = "3a5b"
++++
+
+A more relaxed version to prove semantic preservation of the compiler is
+to use backward simulation.
+
+$\forall B,\ C \Downarrow B \implies S \Downarrow B$
+
+However, this is also too strict, as some important optimisations
+violate this property. One example is dead code elimination, meaning if
+*S* contains dead code that also contains undefined behaviour, then C
+will not contain that undefined behaviour anymore and will therefore
+behave in a different way. To restrict that, we can therefore first
+assume that if the behaviour of the program is safe, then the backward
+simulation will hold.
+
+Therefore, assuming that the behaviour of the source is safe, we can
+then prove the same backward simulation.