Email Gateway (Aug 22 2022 at 15:28): Email Gateway (Aug 22 2022 at 15:28):From: "Thiemann, Rene" <Rene.Thiemann@uibk.ac.at>
Monad normalisation
by Joshua Schneider, Manuel Eberl, and Andreas Lochbihler
The usual monad laws can directly be used as rewrite rules for Isabelle’s
simplifier to normalise monadic HOL terms and decide equivalences.
In a commutative monad, however, the commutativity law is a
higher-order permutative rewrite rule that makes the simplifier loop.
This AFP entry implements a simproc that normalises monadic
expressions in commutative monads using ordered rewriting. The
simproc can also permute computations across control operators like if
and case.
Enjoy 2/5
Last updated: Apr 20 2024 at 04:19 UTC