diff options
Diffstat (limited to 'content/zettel/3c3m2.md')
| -rw-r--r-- | content/zettel/3c3m2.md | 26 |
1 files changed, 26 insertions, 0 deletions
diff --git a/content/zettel/3c3m2.md b/content/zettel/3c3m2.md new file mode 100644 index 0000000..13705ef --- /dev/null +++ b/content/zettel/3c3m2.md @@ -0,0 +1,26 @@ ++++ +title = "Needing strict evaluation for equivalence of predicates" +date = "2023-05-01" +author = "Yann Herklotz" +tags = [] +categories = [] +backlinks = ["3c3m1"] +forwardlinks = ["3a8g5e", "3a8g5g1", "3c3m3"] +zettelid = "3c3m2" ++++ + +Strict evaluation of predicates is important when one wants to prove the +equivalence between two predicates, and therefore be able to conclude +that these predicates will always behave the same given the same inputs. +However, if the evaluation semantics of the predicate relies on the +laziness for evaluation, meaning there are truly paths for which the +return value is unknown, then one might have to resort to three-valued +logic to prove equivalence of two predicates. This is because one needs +to show that of one predicates does not get stuck, that the other +predicate will also not get stuck. This is very similar to the problem +that was encountered during the proof of correctness for GSA +([\#3a8g5e]) and for which we needed to use three-valued logic +([\#3a8g5g1]). + + [\#3a8g5e]: /zettel/3a8g5e + [\#3a8g5g1]: /zettel/3a8g5g1 |