Fixed points in quantitative semantics

Research output: Chapter in Book/Report/Conference proceedingConference contribution

5 Citations (Scopus)
137 Downloads (Pure)

Abstract

We describe an interpretation of recursive computation in a symmetric monoidal category with infinite biproducts and cofree commutative comonoids (for instance, the category of free modules over a complete semiring). Such categories play a significant role in ``quantitative'' models of computation: they bear a canonical complete monoid enrichment, but may not be cpo-enriched, making standard techniques for reasoning about fixed points unavailable. By constructing a bifree algebra for the cofree exponential, we obtain fixed points for morphisms in its co-Kleisli category without requiring any order-theoretic structure. These fixed points corresponding to infinite sums of finitary approximants indexed over the nested finite multisets, each representing a unique call-pattern for computation of the fixed point. We illustrate this construction by using it to give a denotational semantics for PCF with non-deterministic choice and scalar weights from a complete semiring, proving that this is computationally adequate with respect to an operational semantics which evaluates a term by taking a weighted sum of the residues of its terminating reduction paths.
Original languageEnglish
Title of host publicationLICS '16, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science
EditorsNatarajan Shankar
Place of PublicationNew York, U. S. A.
PublisherAssociation for Computing Machinery
Pages347-356
Number of pages10
ISBN (Print)9781450343916
DOIs
Publication statusPublished - 5 Jul 2016
Event31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2016 - New York, USA United States
Duration: 5 Jul 20168 Jul 2016

Publication series

NameProceedings - Symposium on Logic in Computer Science
PublisherIEEE
ISSN (Electronic)2575-5528

Conference

Conference31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2016
CountryUSA United States
CityNew York
Period5/07/168/07/16

Fingerprint Dive into the research topics of 'Fixed points in quantitative semantics'. Together they form a unique fingerprint.

  • Projects

  • Profiles

    Cite this

    Laird, J. (2016). Fixed points in quantitative semantics. In N. Shankar (Ed.), LICS '16, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (pp. 347-356). (Proceedings - Symposium on Logic in Computer Science). Association for Computing Machinery. https://doi.org/10.1145/2933575.2934569