Adequacy for Infinitary Algebraic Effects (Abstract)

Moggi famously proposed a monadic account of computational effects [Mog89, Mog91, BHM02]; this account includes the computational λ-calculus, a core call-by-value functional programming language. Moggi endowed the computational λ-calculus with an effect-oriented denotational semantics by taking the denotations of terms to be morphisms in the Kleisli category of the monad. The question naturally then arises as to whether one can give a correspondingly general treatment of operational semantics.
In the algebraic theory of effects [PP02, PP04, HPP06], a refinement of Moggi’s theory, the effects are obtained by appropriate operations, and Moggi’s monad is then generated by an equational theory over these operations. In a previous paper with John Power [PP01] we gave a general adequacy theorem for the computational λ-calculus for the case of monads generated by finitary operations. This covers examples such as (probabilistic) nondeterminism and exceptions. The main idea is to evaluate terms symbolically in the absolutely free algebra with the same signature as the equational theory. Without recursion, the evaluated terms are finite; with recursion, they may be infinitely deep.