Dr. Niels Frits Willem Voorneveld: Describing Algebraic Effects: Deriving Algebras from Equations

Abstract: We will look at two different methods for specifying behavioural equivalence for programs with algebraic effects. One method is to assume some equational axioms, and use these to define a relation on algebraic expressions, capable of determining equivalence between terms. Another method is to choose some Eilenberg-Moore algebra, and use that to formulate a quantitative logic capable of determining whether two terms are not equivalent. We say that an algebra "complements" a set of equational axioms, if the two give rise to the same notion of behavioural equivalence.

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.