参数化函子和单子的余归纳推理
Coinductive reasoning for parametrized functors and monads
- University of Bologna（博洛尼亚大学）
- RIMS, Kyoto University（京都大学）
机构由 AI 辅助整理，请以论文原文为准。
AI总结：
本文发展了参数化函子和单子的松弛扩展理论，提出了一种通过参数调节允许情境的精细等价概念，取代了标准情境等价性，用于行为等价性的推理。
AI中文摘要：
松弛扩展（也称为关系提升）是一种范畴论概念，用于以兼容的方式推理作用于函数和关系的函子。它们在为基于状态的系统的行为等价性建立可靠证明原理方面发挥着核心作用，并且对于建立有效程序的情境等价性也至关重要。在本文中，我们发展了参数化函子和单子的松弛扩展理论，并考虑了行为预序、等价关系或度量的概念，这些概念现在可以通过额外参数进行调节。从操作的角度来看，我们用一种更精细的等价概念取代了标准的情境等价性（即对所有可能情境进行量化），在这种概念中，用户可以通过选定的参数来调节允许的情境。
英文摘要：
Lax extensions (also called relators or relation liftings) are a categorical notion to reason about functors acting on functions and relations in a compatible way. They play a central role to develop sound proof principles for behavioral equivalence of state-based systems and are also important for establishing contextual equivalence for effectful programs. In this paper, we develop the theory of lax extensions for parametrized functors and monads and consider notions of behavioral preorders, equivalence relations or metrics which can now be modulated by additional parameters. From an operational viewpoint, we replace standard contextual equivalence where we quantify over all possible contexts by a refined notion of equivalence where the user can regulate the allowed contexts via chosen parameters.
