{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,13]],"date-time":"2025-12-13T23:10:56Z","timestamp":1765667456512,"version":"3.41.2"},"reference-count":0,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>Programs with a continuous state space or that interact with physical\nprocesses often require notions of equivalence going beyond the standard binary\nsetting in which equivalence either holds or does not hold. In this paper we\nexplore the idea of equivalence taking values in a quantale V, which covers the\ncases of (in)equations and (ultra)metric equations among others. Our main\nresult is the introduction of a V-equational deductive system for linear\n{\\lambda}-calculus together with a proof that it is sound and complete. In fact\nwe go further than this, by showing that linear {\\lambda}-theories based on\nthis V-equational system form a category that is equivalent to a category of\nautonomous categories enriched over 'generalised metric spaces'. If we\ninstantiate this result to inequations, we get an equivalence with autonomous\ncategories enriched over partial orders. In the case of (ultra)metric\nequations, we get an equivalence with autonomous categories enriched over\n(ultra)metric spaces. We additionally show that this syntax-semantics\ncorrespondence extends to the affine setting. We use our results to develop\nexamples of inequational and metric equational systems for higher-order\nprogramming in the setting of real-time, probabilistic, and quantum computing.<\/jats:p>","DOI":"10.46298\/lmcs-19(4:31)2023","type":"journal-article","created":{"date-parts":[[2023,12,19]],"date-time":"2023-12-19T18:05:08Z","timestamp":1703009108000},"source":"Crossref","is-referenced-by-count":1,"title":["The syntactic side of autonomous categories enriched over generalised metric spaces"],"prefix":"10.46298","volume":"Volume 19, Issue 4","author":[{"given":"Fredrik","family":"Dahlqvist","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Renato","family":"Neves","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"25203","published-online":{"date-parts":[[2023,12,18]]},"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/12719\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/12719\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,12,19]],"date-time":"2023-12-19T18:05:08Z","timestamp":1703009108000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/10018"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,12,18]]},"references-count":0,"URL":"https:\/\/doi.org\/10.46298\/lmcs-19(4:31)2023","relation":{"has-preprint":[{"id-type":"arxiv","id":"2208.14356v4","asserted-by":"subject"},{"id-type":"arxiv","id":"2208.14356v3","asserted-by":"subject"},{"id-type":"arxiv","id":"2208.14356v2","asserted-by":"subject"}],"is-same-as":[{"id-type":"arxiv","id":"2208.14356","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.2208.14356","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2023,12,18]]},"article-number":"10018"}}