blob: db3eefd823cd95adc1839ced199c6b795652ff72 (
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
26
27
28
|
+++
title = "Using lazy evaluation by construction"
date = "2023-02-04"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3c3f3"]
forwardlinks = ["3c3f5"]
zettelid = "3c3f4"
+++
One possible solution to this is to write down lazy evaluation semantics
for the predicate. These are equivalent to the standard evaluation
semantics in the case where all the atoms are evaluable, however, they
can help in the case where one of the atoms may not be evaluable. Then,
as long as one can show that in the cases where this predicate has to be
evaluated, it can be, one can show that the whole predicate will also
always result in a value.
This can be done in the case of the symbolic evaluation of the basic
blocks, because the only cases where one is not certain if one can
evaluate a predicate is when the predicate itself is predicated, and
that predicate evaluates to false. This link is captured by an
implication, and if a lazy implication is used instead, this means that
one can evaluate the predicate eagerly in all cases, even when one
cannot evaluate everyone of the atoms. In addition to that, this can be
done using binary logic and without having to resort to three-valued
logic.
|
