Fixed points in quantitative semantics

Research output: Chapter or section in a book/report/conference proceedingChapter in a published conference proceeding

9 Citations (SciVal)
274 Downloads (Pure)


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
Number of pages10
ISBN (Print)9781450343916
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
ISSN (Electronic)2575-5528


Conference31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2016
Country/TerritoryUSA United States
CityNew York


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

Cite this