License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2022.16
URN: urn:nbn:de:0030-drops-157362
URL: https://drops.dagstuhl.de/opus/volltexte/2022/15736/
Go to the corresponding LIPIcs Volume Portal

Dahlqvist, Fredrik ; Neves, Renato

An Internal Language for Categories Enriched over Generalised Metric Spaces

pdf-format:
LIPIcs-CSL-2022-16.pdf (0.8 MB)

Abstract

Programs with a continuous state space or that interact with physical processes often require notions of equivalence going beyond the standard binary setting in which equivalence either holds or does not hold. In this paper we explore the idea of equivalence taking values in a quantale 𝒱, which covers the cases of (in)equations and (ultra)metric equations among others.
Our main result is the introduction of a 𝒱-equational deductive system for linear λ-calculus together with a proof that it is sound and complete (in fact, an internal language) for a class of enriched autonomous categories. In the case of inequations, we get an internal language for autonomous categories enriched over partial orders. In the case of (ultra)metric equations, we get an internal language for autonomous categories enriched over (ultra)metric spaces.
We use our results to obtain examples of inequational and metric equational systems for higher-order programs that contain real-time and probabilistic behaviour.

BibTeX - Entry

@InProceedings{dahlqvist_et_al:LIPIcs.CSL.2022.16,
  author =	{Dahlqvist, Fredrik and Neves, Renato},
  title =	{{An Internal Language for Categories Enriched over Generalised Metric Spaces}},
  booktitle =	{30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
  pages =	{16:1--16:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-218-1},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{216},
  editor =	{Manea, Florin and Simpson, Alex},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2022/15736},
  URN =		{urn:nbn:de:0030-drops-157362},
  doi =		{10.4230/LIPIcs.CSL.2022.16},
  annote =	{Keywords: \lambda-calculus, enriched category theory, quantale, equational theory}
}

Keywords: λ-calculus, enriched category theory, quantale, equational theory
Collection: 30th EACSL Annual Conference on Computer Science Logic (CSL 2022)
Issue Date: 2022
Date of publication: 27.01.2022

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI