blob: 13705efa3fbb41688039d9018d4bb59e4009b3bb (
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
|
+++
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
|
