Projects per year

### 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 language | English |
---|---|

Title of host publication | LICS '16, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science |

Editors | Natarajan Shankar |

Place of Publication | New York, U. S. A. |

Publisher | Association for Computing Machinery |

Pages | 347-356 |

Number of pages | 10 |

ISBN (Print) | 9781450343916 |

DOIs | |

Publication status | Published - 5 Jul 2016 |

Event | 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2016 - New York, USA United States Duration: 5 Jul 2016 → 8 Jul 2016 |

### Publication series

Name | Proceedings - Symposium on Logic in Computer Science |
---|---|

Publisher | IEEE |

ISSN (Electronic) | 2575-5528 |

### Conference

Conference | 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2016 |
---|---|

Country | USA United States |

City | New York |

Period | 5/07/16 → 8/07/16 |

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

## Projects

- 1 Finished

### Semantic Types for Verified Program Behaviour

Engineering and Physical Sciences Research Council

28/02/14 → 31/07/17

Project: Research council

## 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