TY - JOUR

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

AU - Hyland, M

AU - Nagayama, M

AU - Power, John

AU - Rosolini, G

PY - 2006/8/31

Y1 - 2006/8/31

N2 - 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.

AB - 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.

UR - http://dx.doi.org/10.1016/j.entcs.2006.04.024

U2 - 10.1016/j.entcs.2006.04.024

DO - 10.1016/j.entcs.2006.04.024

M3 - Article

SN - 1571-0661

VL - 161

SP - 43

EP - 57

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

ER -