1 files changed, 55 insertions, 0 deletions
diff --git a/content/zettel/3a8g5e1a.md b/content/zettel/3a8g5e1a.md
new file mode 100644
index 0000000..5dd7043
--- /dev/null
+++ b/content/zettel/3a8g5e1a.md
@@ -0,0 +1,55 @@
++++
+title = "PTrue preservation for γ-functions"
+author = "Yann Herklotz"
+tags = []
+categories = []
+backlinks = ["3a8g5e1"]
+forwardlinks = ["3a8g5e"]
+zettelid = "3a8g5e1a"
++++
+
+When using γ-functions, one needs to prove that for a join-point, the
+`PTrue` property is preserved accross the semantics. For the η-function
+when there is no join-point, this was quite straightforward as no
+previous nodes had to be examined, there was only one. However, when
+proving the γ-function, there are multiple predecessors. Even though we
+have the `pred_correct` property, which has been validated by the SAT
+solver ([\#3a8g5e]), there is no guarantee that each of the predecessors
+will be evaluated to a `Some` value. Therefore, when we do the global
+`or` of all the predecessors, and say that this implies the correctness
+of the predicate at this point, we cannot be sure that we are evaluating
+that predicate to a value.
+
+Furthermore, it is actually most likely that we will not evaluate that
+predicate to a value, because there are various conditions and variables
+that remain undefined at that point. This means that various conditions
+will evaluate to a `None` value.
+
+There are three different possible solutions to this:
+
+1.  Evaluate each predecessor with the original `eval_predicate`
+    function, but then or them together lazily using a slightly
+    different evaluation function. This evaluation function will take
+    into account the fact that some predicates will be able to return
+    `None`. The main problem with this is that this doesn't make it easy
+    to guarantee that the current predicate will return a `Some` value
+    with the same state. Instead, the current predicate would probably
+    also have to be evaluated lazily.
+2.  Evaluate the whole predicate lazily, and only care about the truth
+    value of correctness at the output. This is definitely a better
+    solution than the previous, even though it probably requires more
+    changes. One main problem with this solution is that it may not be
+    possible to prove the required correctness proof using the SAT
+    solver.
+3.  Finally, another solution would be to keep track of the evaluation
+    of each of the conditions, and therefore show that each condition is
+    evaluating to a `Some` value. Then, proving that when we encounter a
+    predicate that we must have traversed it previously, and due to the
+    fact that SSA guarantees that if the definition of a point dominates
+    the current point, then it's value is the value is known to be the
+    same as at the definition point, one can show that the condition at
+    the current point will also evaluate to a `Some` value. This is
+    probably the most realistic, but quite a difficult solution with a
+    lot of work involved to get it to work.
+
+  [\#3a8g5e]: /zettel/3a8g5e