A universal embedding for the higher order structure of computational effects

John Power

Research output: Chapter in Book/Report/Conference proceedingChapter

2 Citations (Scopus)

Abstract

We give a universal embedding of the semantics for the first order fragment of the computational λ-calculus into a semantics for the whole calculus. In category theoretic terms, which are the terms of the paper, this means we give a universal embedding of every small Freyd-category into a closed Freyd-category. The universal property characterises the embedding as the free completion of the Freyd-category as ca [→, Set]-enriched category under conical colimits. This embedding extends the usual Yoneda embedding of a small category with finite products into its free cocompletion, i.e., the usual category theoretic embedding of a model of the first order fragment of the simply typed λ-calculus into a model for the whole calculus, and similarly for the linear λ-calculus. It agrees with an embedding previously given in an ad hoc way without a universal property, so it shows the definitiveness of that construction.
Original languageEnglish
Title of host publicationTyped Lambda Calculi and Applications 6th International Conference, TLCA 2003 Valencia, Spain, June 10–12, 2003 Proceedings
Place of PublicationBerlin
PublisherSpringer
Pages301-315
Number of pages15
Volume2701
DOIs
Publication statusPublished - 2003

Publication series

NameLecture Notes in Computer Science
PublisherSpringer

Fingerprint Dive into the research topics of 'A universal embedding for the higher order structure of computational effects'. Together they form a unique fingerprint.

  • Cite this

    Power, J. (2003). A universal embedding for the higher order structure of computational effects. In Typed Lambda Calculi and Applications 6th International Conference, TLCA 2003 Valencia, Spain, June 10–12, 2003 Proceedings (Vol. 2701, pp. 301-315). (Lecture Notes in Computer Science). Springer. https://doi.org/10.1007/3-540-44904-3_21