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
32
33
34
35
36
37
38
39
40
41
|
+++
title = "Making the Proof Tractable using the Identity Semantics"
date = "2022-11-16"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3c3j"]
forwardlinks = ["3c3l", "3c3k1"]
zettelid = "3c3k"
+++
A trick that also had to be pulled to make the proofs of the abstract
interpretation tractable was using an identity semantics to prove basic
properties about `sem_pred_expr`. For some reason, when using the
identity semantics one can nicely compose behaviours of all the
`Applicative` functions.
Essentially we have a function which implements the semantics for our
`predicated A` type, which happens to at least be an Applicative. The
function itself is implemented similarly to a foldMap, but instead of
using a general monoid instance to combine the elements, it just keeps
the element that evaluates to true. This could be the monoid instance,
but it requires to introspect into the current context:
``` coq
sem_pred_expr
: forall A B,
PTree.t pred_pexpr -> (Abstr.ctx -> A -> B -> Prop) ->
Abstr.ctx -> predicated A -> B -> Prop
```
Then, once the predicates are evaluated, it's not quite a monoid
instance, because you are getting an element out of a list based on the
evaluation of the predicate.
However, you could also see it as reducing a list of things to the list
of things that evaluated to true, in which case the monoid instance
would still hold. Then, we are just converting the monoid to a maybe and
checking that the list only contained one element. That would mean that
the evaluation should take in predicated instructions and to the
predicate evaluation, but also evaluate the expression.
|
