blob: 6fbbe73a5b3c3c546f571c190004941e97e1e66f (
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
29
30
31
|
+++
title = "Interesting properties of predicate execution"
date = "2023-05-01"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3c3l"]
forwardlinks = ["3c3n", "3c3m1"]
zettelid = "3c3m"
+++
The execution semantics of predicates are tricky to get right. There is
a balance between having flexible execution semantics and being able to
prove the equivalence between two of these predicates. In this context,
I mean that in flexible (non-deterministic) semantics of predicates are
ones where:
``` text
a || true == true
```
regardless of if the value of a is in the map or not, and strict
execution of semantics need to be able to show that:
```{=latex}
\begin{equation*}
\exists b\ldotp m \mathbin{!} a = b
\end{equation*}
```
This is an important distinction, as one allows for *lazy* evaluation of
predicates, but this complicates reasoning about the predicates.
|
