Research

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


Reference:

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:

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

Abstract

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.

Details

Item Type Articles
CreatorsHyland, M., Nagayama, M., Power, J. and Rosolini, G.
DOI10.1016/j.entcs.2006.04.024
DepartmentsFaculty of Science > Computer Science
RefereedYes
StatusPublished
ID Code26512

Export

Actions (login required)

View Item