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

M Hyland, M Nagayama, John Power, G Rosolini

Research output: Contribution to journalArticlepeer-review

18 Citations (SciVal)


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.
Original languageEnglish
Pages (from-to)43-57
Number of pages15
JournalElectronic Notes in Theoretical Computer Science
Publication statusPublished - 31 Aug 2006


Dive into the research topics of 'A Category Theoretic Formulation for Engeler-style Models of the Untyped λ-Calculus'. Together they form a unique fingerprint.

Cite this