diff options
Diffstat (limited to 'content/zettel/3c3g6.md')
-rw-r--r-- | content/zettel/3c3g6.md | 26 |
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. |