Dr. Niels Frits Willem Voorneveld: Describing Algebraic Effects: Deriving Algebras from Equations
Source: Mathematics and theoretical computing seminar
In this talk, we will study a way to derive from a set of equational axioms, an Eilenberg-Moore algebra which complements it. This method uses true-false effect trees, which are effect trees with a bottom and a top leaf. We apply this method to several examples of effects, including nondeterminism, probability, global store, timer, and some combinations thereof, and see how the usual equational axioms give rise to algebras featured in previous works.
In general, the algebra derived from this method is not always suitable for specifying behavioural equivalence. We will discuss two additional conditions that need be met for this to be the case, which luckily hold for the examples of effects given above. Lastly, we will briefly look at a method to extract a set of Boolean modalities from an algebra, which potentially could be used to specify behavioural equivalence via a Boolean logic. However, this last method does not work for some examples of effects, for instance the combination of nondeterminism with probability.