blob: e5e02fc832d2817b7e721705ceeb1b37cbda0e3a (
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
|
+++
title = "Strict evaluation and lazy evaluation are equivalent"
date = "2023-02-14"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3c3f7"]
forwardlinks = []
zettelid = "3c3f7a"
+++
The main downside of the lazy evaluation approach is actually that there
are additional constructors, and that the evaluation is less automatic.
However, unintuitively, they should actually be equivalent from an
evaluation perspective if one knows that one can evaluate all the
branches. However, with richer predicates this is not the case anymore,
which is why we have to use the lazy evaluation approach.
However, when doing a SAT solve, it should be provable that given the
evaluation of one of the predicates, and that the predicates used are
the same (or maybe a subset), then one knows that one can evaluate both
predicates. This is not as clear as I thought it would be though because
I forgot that executing the leaves is not the same in boolean logic and
in the rich predicate logic I use in the end.
|
