+++
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.