+++
title = "Semantic invariance property"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3a8g5b"]
forwardlinks = ["3a8e", "3a8g5d", "3a8g5c1"]
zettelid = "3a8g5c"
+++

A semantic invariance property needs to be found, which can be proven to
be true at any point in the graph. This then makes it easier to prove
the correctness of the predicates, as the semantic property can be used
instead if all the preconditions are met.

The other benefit is that this property can be proven by induction on
the semantics themselves, which means that one can assume that it is
true for the previous state, and prove that it still holds for the next
state. Afterwards, one also needs to prove that it holds for the initial
state of the semantics, just like how the equations lemma was proven
([\#3a8e]).

The invariance property that needs to be proven for the correctness
proof between the predicates and the path expressions is the following:

```{=latex}
\begin{align}
\forall p_c\ r_s\ &m,\\
(\forall d\ &R_{d\ \rightarrow p_c}\ P,\\
&(\forall p, \text{path}\ d\ p\ p_c \implies
  p \in \sigma(R_{d \rightarrow p_c}))\\
&\implies t\ R_{d\ \rightarrow p_c}\ P \\
&\implies \text{sdom}\ d\ p_c \\
&\implies P \Downarrow (r_s, m) = T)\\
\implies &\text{path_prop}\ p_c\ r_s\ m
\end{align}
```

  [\#3a8e]: /zettel/3a8e