1 files changed, 31 insertions, 0 deletions
diff --git a/content/zettel/3c3m.md b/content/zettel/3c3m.md
new file mode 100644
index 0000000..6fbbe73
--- /dev/null
+++ b/content/zettel/3c3m.md
@@ -0,0 +1,31 @@
++++
+title = "Interesting properties of predicate execution"
+date = "2023-05-01"
+author = "Yann Herklotz"
+tags = []
+categories = []
+backlinks = ["3c3l"]
+forwardlinks = ["3c3n", "3c3m1"]
+zettelid = "3c3m"
++++
+
+The execution semantics of predicates are tricky to get right. There is
+a balance between having flexible execution semantics and being able to
+prove the equivalence between two of these predicates. In this context,
+I mean that in flexible (non-deterministic) semantics of predicates are
+ones where:
+
+``` text
+a || true == true
+```
+
+regardless of if the value of a is in the map or not, and strict
+execution of semantics need to be able to show that:
+
+```{=latex}
+\begin{equation*}
+\exists b\ldotp m \mathbin{!} a = b
+\end{equation*}
+```
+This is an important distinction, as one allows for *lazy* evaluation of
+predicates, but this complicates reasoning about the predicates.