1 files changed, 29 insertions, 0 deletions
diff --git a/content/zettel/3a8g5e.md b/content/zettel/3a8g5e.md
new file mode 100644
index 0000000..d15ab65
--- /dev/null
+++ b/content/zettel/3a8g5e.md
@@ -0,0 +1,29 @@
++++
+title = "Designing a proof with validation"
+author = "Yann Herklotz"
+tags = []
+categories = []
+backlinks = ["3c3m2", "3a8g5g", "3a8g5e1a", "3a8g5d", "2e1c6a"]
+forwardlinks = ["3a8g5f", "3a8g5e1"]
+zettelid = "3a8g5e"
++++
+
+Because of the trickiness of the proof, it would therefore be good to
+integrate some validation into the algorithm, however, it's not quite
+clear where to do this check. One possibility, which might allow for
+quite a few optimisations to not make it too inefficient, is to prove
+the following invariant on the semantics:
+
+$$ \forall d\ s,\ t\ R_{d \rightarrow p_c} \Downarrow s \Longleftrightarrow t\\left( \bigcup_{i \in \text{preds}(p_c)} R_{d \rightarrow i} \cdot c_i \right)\Downarrow s. $$
+
+However, this can be simplified even further by actually only verifying
+the predicates that were generated from the path expressions instead,
+giving the following invariant:
+
+$$ \forall d\ s,\ P_{d \rightarrow p_c} \Downarrow s \Longleftrightarrow \left(\bigvee_{i \in \text{preds}(p_c)} P_{d \rightarrow i} \land c_i \right)\Downarrow s. $$
+
+This property allows us to properly prove the correctness of the
+predicates, because on can use this property to prove that if one of the
+predecessors evaluates to true (which we can assume for the induction),
+then due to the predicate being equivalent to the ors of all the
+predecessors, it means that the current predicate must also be correct.