1 files changed, 24 insertions, 0 deletions
diff --git a/content/zettel/3c3f7a.md b/content/zettel/3c3f7a.md
new file mode 100644
index 0000000..e5e02fc
--- /dev/null
+++ b/content/zettel/3c3f7a.md
@@ -0,0 +1,24 @@
++++
+title = "Strict evaluation and lazy evaluation are equivalent"
+date = "2023-02-14"
+author = "Yann Herklotz"
+tags = []
+categories = []
+backlinks = ["3c3f7"]
+forwardlinks = []
+zettelid = "3c3f7a"
++++
+
+The main downside of the lazy evaluation approach is actually that there
+are additional constructors, and that the evaluation is less automatic.
+However, unintuitively, they should actually be equivalent from an
+evaluation perspective if one knows that one can evaluate all the
+branches. However, with richer predicates this is not the case anymore,
+which is why we have to use the lazy evaluation approach.
+
+However, when doing a SAT solve, it should be provable that given the
+evaluation of one of the predicates, and that the predicates used are
+the same (or maybe a subset), then one knows that one can evaluate both
+predicates. This is not as clear as I thought it would be though because
+I forgot that executing the leaves is not the same in boolean logic and
+in the rich predicate logic I use in the end.