  There are several ways to define program equivalence for functional programs
with algebraic effects. We consider two complementing ways to specify
behavioural equivalence. One way is to specify a set of axiomatic equations,
and allow proof methods to show that two programs are equivalent. Another way
is to specify an Eilenberg-Moore algebra, which generate tests that could
distinguish programs. These two methods are said to complement each other if
any two programs can be shown to be equivalent if and only if there is no test
to distinguish them.
  In this paper, we study a generic method to formulate from a set of axiomatic
equations an Eilenberg-Moore algebra which complements it. We will look at an
additional condition which must be satisfied for this to work. We then apply
this method to a handful of examples of effects, including probability and
global store, and show they coincide with the usual algebras from the
literature. We will moreover study whether or not it is possible to specify a
set of unary Boolean modalities which could function as distinction-tests
complementing the equational theory.
