blob: eb5ae649cdcb61b38bd41b413517a11bf9d9c993 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
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
|
