summaryrefslogtreecommitdiffstats
path: root/content/zettel/3c3g1.md
diff options
context:
space:
mode:
Diffstat (limited to 'content/zettel/3c3g1.md')
-rw-r--r--content/zettel/3c3g1.md25
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