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


Hyland, M., Nagayama, M., Power, J. and Rosolini, G., 2006. A Category Theoretic Formulation for Engeler-style Models of the Untyped λ-Calculus. Electronic Notes in Theoretical Computer Science, 161, pp. 43-57.

Related documents:

This repository does not currently have the full-text of this item.
You may be able to access a copy if URLs are provided below.

Official URL:


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.


Item Type Articles
CreatorsHyland, M., Nagayama, M., Power, J. and Rosolini, G.
DepartmentsFaculty of Science > Computer Science
ID Code26512


Actions (login required)

View Item