2021/05/18 by Fredrik Dahlqvist, Dahlqvist, Fredrik, Renato Neves +1
Computer Science · #68Q01 #Computability, Logic, AI Algorithms #F.3.0 #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.2105.08473
openalex publication_date 2021/05/18 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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\λ-calculus together with a proof that it is sound and complete (in\nfact, an internal language) for a class of enriched autonomous categories. In\nthe case of inequations, we get an internal language for autonomous categories\nenriched over partial orders. In the case of (ultra)metric equations, we get an\ninternal language for autonomous categories enriched over (ultra)metric spaces.\nWe use our results to obtain examples of inequational and metric equational\nsystems for higher-order programs that contain real-time and probabilistic\nbehaviour\n