模态推理=度量推理，通过Lawvere
Modal Reasoning = Metric Reasoning, via Lawvere
摘要：
分级模态类型、系统和协同效应正在成为处理上下文相关计算的标准形式，其中代码使用起着核心作用。然而，模态语言和协同语言的程序等价理论，如果与这些语言的指称语义和操作语义相比，则相当不发达。这就提出了一个问题，即普通程序等价的理论在多大程度上可以在模态场景中给出。在这项工作中，我们表明，共归纳等价可以扩展到一个模态设置，我们这样做，通过推广阿布拉姆斯基的应用双相似coeffective行为。为了实现这一目标，我们开发了一个通用的理论，三元程序关系的基础上的新概念的comonadic宽松的扩展，在此之上，我们定义了一个模态扩展的Abramsky的应用bisimilarity（我们称之为模态应用bisimilarity）。我们证明这样的关系是一个一致性，这种方式获得一个组合技术推理模态和coeffective行为。但这并不是故事的结束：我们还建立了模态程序关系和程序距离之间的对应关系。这种对应关系表明模态应用双相似性和（适当扩展的）应用双相似性距离一致，这种方式揭示了模态程序等价性和程序距离只是同一枚硬币的两面。
英文摘要：
Graded modal types systems and coeffects are becoming a standard formalism to deal with context-dependent computations where code usage plays a central role. The theory of program equivalence for modal and coeffectful languages, however, is considerably underdeveloped if compared to the denotational and operational semantics of such languages. This raises the question of how much of the theory of ordinary program equivalence can be given in a modal scenario. In this work, we show that coinductive equivalences can be extended to a modal setting, and we do so by generalising Abramsky's applicative bisimilarity to coeffectful behaviours. To achieve this goal, we develop a general theory of ternary program relations based on the novel notion of a comonadic lax extension, on top of which we define a modal extension of Abramsky's applicative bisimilarity (which we dub modal applicative bisimilarity). We prove such a relation to be a congruence, this way obtaining a compositional technique for reasoning about modal and coeffectful behaviours. But this is not the end of the story: we also establish a correspondence between modal program relations and program distances. This correspondence shows that modal applicative bisimilarity and (a properly extended) applicative bisimilarity distance coincide, this way revealing that modal program equivalences and program distances are just two sides of the same coin.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
