Monad normalisation (Q53725)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry Monad_Normalisation
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | Monad normalisation |
AFP entry Monad_Normalisation |
Statements
Joshua Schneider
0 references
Manuel Eberl
0 references
Andreas Lochbihler
0 references
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.
0 references
5 May 2017
0 references
Monad normalisation (English)
0 references
