模态推理 = 度量推理：基于 Lawvere 的视角

分级模态类型系统与协效应（coeffects）正成为处理以代码使用为核心作用的上下文相关计算的标准形式化工具。然而，与此类语言的指称语义和操作语义相比，模态与协效应语言的程序等价理论仍相当不成熟。这引发了一个问题：通常的程序等价理论有多少可以在模态场景下给出。在本文中，我们展示了共归纳等价可以推广到模态设定，并通过将 Abramsky 的应用互模拟推广到协效应行为来实现这一点。为实现这一目标，我们基于新颖的协单子松弛扩张（comonadic lax extension）概念发展了三元程序关系的一般理论，并在此基础上定义了 Abramsky 应用互模拟的模态推广（我们称之为模态应用互模拟）。我们证明此种关系是一个同余，从而获得了一种用于推理模态与协效应行为的组合技术。但这并非故事的终点：我们还建立了模态程序关系与程序距离之间的对应。该对应表明模态应用互模拟与（适当扩展的）应用互模拟距离相重合，从而揭示出模态程序等价与程序距离只是同一枚硬币的两面。