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.
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11567/224934
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 18
  • ???jsp.display-item.citation.isi??? ND
social impact