Weighted models for higher-order computation

Research output: Contribution to journalArticlepeer-review

Abstract

We study a class of quantitative models for higher-order computation: Lafont categories with (infinite) biproducts. Each of these has a complete “internal semiring” and can be enriched over its modules. We describe a semantics of nondeterministic PCF weighted over this semiring in which fixed points are obtained from the bifree algebra over its exponential structure. By characterizing them concretely as infinite sums of approximants indexed over nested finite multisets, we prove computational adequacy. We can construct examples of our semantics by weighting existing models such as categories of games over a complete semiring. This transition from qualitative to quantitative semantics is characterized as a “change of base” of enriched categories arising from a monoidal functor from coherence spaces to modules over a complete semiring. For example, the game semantics of Idealized Algol is coherence space enriched and thus gives rise to to a weighted model, which is fully abstract.

Original languageEnglish
Article number104645
JournalInformation and Computation
Volume275
Early online date12 Nov 2020
DOIs
Publication statusPublished - 31 Dec 2020

Keywords

  • Complete semirings
  • Computational adequacy
  • Fixed points
  • Game semantics
  • Linear logic
  • Quantitative models

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Information Systems
  • Computer Science Applications
  • Computational Theory and Mathematics

Cite this