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

The paper presents a category-theoretic formulation of Engeler-style models for the untyped λ-calculus, exhibiting an equivalence between distributive laws and extensions of one monad to the Kleisli category of another and exploring 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.\udOne exploits 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 to build models of the untyped λ-calculus, yielding a variant of the Engeler model. When replacing the monad for commutative monoids by that for idempotent commutative monoids, which, on Set, is the finite power set monad, one does not quite get a distributive law, but a little more subtlety yields exactly the original Engeler construction