Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/89543
Título: | The syntactic side of autonomous categories enriched over generalised metric spaces |
Autor(es): | Dahlqvist, Fredrik Neves, Renato Jorge Araújo |
Palavras-chave: | categorical logic enriched category theory quantale λ-calculus |
Data: | 2023 |
Editora: | Logical Methods in Computer Science |
Revista: | Logical Methods in Computer Science |
Citação: | Dahlqvist, F., & Neves, R. (2023, December 18). The syntactic side of autonomous categories enriched over generalised metric spaces. Logical Methods in Computer Science. Logical Methods in Computer Science. http://doi.org/10.46298/lmcs-19(4:31)2023 |
Resumo(s): | 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 V, which covers the cases of (in)equations and (ultra)metric equations among others. Our main result is the introduction of a V-equational deductive system for linear λ-calculus together with a proof that it is sound and complete. In fact we go further than this, by showing that linear λ-theories based on this V-equational system form a category equivalent to a category of autonomous categories enriched over ‘generalised metric spaces’. If we instantiate this result to inequations, we get an equivalence with autonomous categories enriched over partial orders. In the case of (ultra)metric equations, we get an equivalence with autonomous categories enriched over (ultra)metric spaces. Additionally, we show that this syntax-semantics correspondence extends to the affine setting. We use our results to develop examples of inequational and metric equational systems for higher-order programming in the setting of real-time, probabilistic, and quantum computing. |
Tipo: | Artigo |
URI: | https://hdl.handle.net/1822/89543 |
DOI: | 10.46298/lmcs-19(4:31)2023 |
ISSN: | 1860-5974 |
Versão da editora: | https://lmcs.episciences.org/12719 |
Arbitragem científica: | yes |
Acesso: | Acesso aberto |
Aparece nas coleções: | HASLab - Artigos em revistas internacionais |
Este trabalho está licenciado sob uma Licença Creative Commons