blob: 4e30c35d1be875c8911de5bafb45e6b633bbab9f (
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 = "On evaluability of predicates"
date = "2023-02-05"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3c3f4"]
forwardlinks = ["3c3f6"]
zettelid = "3c3f5"
+++
1. First, I need to check if I can have lazy evaluation of predicates
with respect to the equivalence check. I need to verify that
equivalent formulas imply equivalent behaviour with lazy evaluation
of predicates. This might come down to a statement of "There exists
a way to evaluate the current predicate so that it evaluates to the
same version of the other predicate."
2. I currently need to show that all predicates in the forest are
evaluable. This may not be the case in practice, but currently I use
it when merging. However, I think that with the lazy evaluation of
predicates, this might not be needed.
3. Check what the difference is between evaluable and the sem~predpred~
that is in the forest, as that says that one assigns the result of
evaluating the predicates to a predicate register map. This should
imply that they are all evaluable.
|