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. One 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.
A Category Theoretic Formulation for Engeler-style Models of the Untyped Lambda-Calculus
ROSOLINI, GIUSEPPE
2006-01-01
Abstract
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. One 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.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
