1 files changed, 41 insertions, 0 deletions
diff --git a/content/zettel/3c3k.md b/content/zettel/3c3k.md
new file mode 100644
index 0000000..50a5910
--- /dev/null
+++ b/content/zettel/3c3k.md
@@ -0,0 +1,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.