A Category Theoretic Formulation for Engeler-style Models of the Untyped λ-Calculus

We give a category-theoretic formulation of previous termEngelernext term-previous termstylenext termprevious termmodelsnext term for the untyped λ-calculus. In order to do so, we exhibit an equivalence between distributive laws and extensions of one monad to the Kleisli category of another and explore the example of an arbitrary commutative monad together with the monad for commutative monoids. On Set as base category, the latter is the finite multiset monad. We exploit the self-duality of the category Rel, i.e., the Kleisli category for the powerset monad, and the category theoretic structures on it that allow us to build previous termmodelsnext term of the untyped λ-calculus, yielding a variant of the previous termEngelernext termprevious termmodelnext term. We replace the monad for commutative monoids by that for idempotent commutative monoids, which, on Set, is the finite powerset monad. This does not quite yield a distributive law, so requires a little more subtlety, but, subject to that subtlety, it yields exactly the original previous termEngelernext term construction.