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