diff options
Diffstat (limited to 'content/zettel/3c3g1.md')
-rw-r--r-- | content/zettel/3c3g1.md | 25 |
1 files changed, 25 insertions, 0 deletions
diff --git a/content/zettel/3c3g1.md b/content/zettel/3c3g1.md new file mode 100644 index 0000000..eb5ae64 --- /dev/null +++ b/content/zettel/3c3g1.md @@ -0,0 +1,25 @@ ++++ +title = "Recursive predicated expressions" +author = "Yann Herklotz" +tags = [] +categories = [] +backlinks = ["3d2b1", "3c3g2", "3c3g"] +forwardlinks = ["2e1c6a", "3c3g2"] +zettelid = "3c3g1" ++++ + +These are expressions of the following type: + +$$ P ::= [p?, P] \ |\ e $$ + +This means that one can either have a list of predicates, linked to more +predicated expressions, or be an expression. The one difficulty with +dealing with such an expression is that the comparison using a SAT +solver becomes basically impossible. This is because one cannot perform +hashing of the predicates, as described in `Ptree` hashing ([\#2e1c6a]). +The hashing of the expressions is necessary to be able to pass the +expressions to the SAT solver in the first place, and because one +doesn't have pure expressions anymore, one cannot define the syntactic +equality operator anymore to compare (and therefore hash) expressions. + + [\#2e1c6a]: /zettel/2e1c6a |