+++ 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