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

Higher Order
Lambda Calculus
Fragment
Calculus
Enriched Category
First-order
Colimit
Typed lambda Calculus
Term
Completion
Closed
Model
Semantics

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). Berlin: Springer. https://doi.org/10.1007/3-540-44904-3_21

A universal embedding for the higher order structure of computational effects. / Power, John.

Typed Lambda Calculi and Applications 6th International Conference, TLCA 2003 Valencia, Spain, June 10–12, 2003 Proceedings. Vol. 2701 Berlin : Springer, 2003. p. 301-315 (Lecture Notes in Computer Science).

Research output: Chapter in Book/Report/Conference proceedingChapter

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, Lecture Notes in Computer Science, Springer, Berlin, pp. 301-315. https://doi.org/10.1007/3-540-44904-3_21
Power J. 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. Berlin: Springer. 2003. p. 301-315. (Lecture Notes in Computer Science). https://doi.org/10.1007/3-540-44904-3_21
Power, John. / A universal embedding for the higher order structure of computational effects. Typed Lambda Calculi and Applications 6th International Conference, TLCA 2003 Valencia, Spain, June 10–12, 2003 Proceedings. Vol. 2701 Berlin : Springer, 2003. pp. 301-315 (Lecture Notes in Computer Science).
@inbook{5224094749014066ac0294d78c1a67bf,
title = "A universal embedding for the higher order structure of computational effects",
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.",
author = "John Power",
note = "Typed lambda calculi and applications (Valencia, 2003)",
year = "2003",
doi = "10.1007/3-540-44904-3_21",
language = "English",
volume = "2701",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "301--315",
booktitle = "Typed Lambda Calculi and Applications 6th International Conference, TLCA 2003 Valencia, Spain, June 10–12, 2003 Proceedings",

}

TY - CHAP

T1 - A universal embedding for the higher order structure of computational effects

AU - Power, John

N1 - Typed lambda calculi and applications (Valencia, 2003)

PY - 2003

Y1 - 2003

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

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

UR - http://dx.doi.org/10.1007/3-540-44904-3_21

U2 - 10.1007/3-540-44904-3_21

DO - 10.1007/3-540-44904-3_21

M3 - Chapter

VL - 2701

T3 - Lecture Notes in Computer Science

SP - 301

EP - 315

BT - Typed Lambda Calculi and Applications 6th International Conference, TLCA 2003 Valencia, Spain, June 10–12, 2003 Proceedings

PB - Springer

CY - Berlin

ER -