Add content

1 files changed, 26 insertions, 0 deletions

diff --git a/content/zettel/3c3g6.md b/content/zettel/3c3g6.md
new file mode 100644
index 0000000..cbdf84f
--- /dev/null
+++ b/content/zettel/3c3g6.md
@@ -0,0 +1,26 @@
++++
+title = "The need for abstract predicates"
+date = "2022-07-19"
+author = "Yann Herklotz"
+tags = []
+categories = []
+backlinks = ["3c3g5"]
+forwardlinks = ["3c3g7", "3c3g6a"]
+zettelid = "3c3g6"
++++
+
+In the previous version of the abstract language with predicated
+expressions, the predicates were concrete, which is wrong because they
+will then always be executed with respect to the original context. The
+way this can be fixed is by also keeping track of abstract predicates,
+however, then one ends up with predicates that might themselves be
+predicated. Currently, the idea is to recombine these into a predicate
+whenever this is needed, by anding all the elements in the list
+together. This generates massive predicates because at each exit and
+each predicate assignment, the predicates are multiplied together. Most
+of the time, these predicates are very easy to solve, however, after
+using the tseytin transformation, many additional variables are added
+which makes it much harder to solve.
+
+In general though, it seems like this analysis is at least correct,
+meaning it can find bugs hopefully.