Rocq中域理论与交互树的结合
Domain Theory Meets Interaction Trees in Rocq
- Univ.\ Lille, CNRS, Centrale Lille, UMR 9189 CRIStAL, F-59000 Lille, France
- Inria, Univ.\ Lille, CNRS, Centrale Lille, UMR 9189 CRIStAL, F-59000 Lille, France
机构由 AI 辅助整理，请以论文原文为准。
AI总结：
本研究在Rocq中提出不依赖内置共归纳的域理论交互树形式化方法，定义归纳式程序等价关系以简化非终止程序推理，证明其正确性并通过叙拉古序列程序示例验证框架。
AI中文摘要：
我们在Rocq证明助手中提出了一种基于域理论的交互树形式化方法。与现有形式化工作不同，我们的方法不依赖Rocq内置的共归纳机制，因此避免了早期研究中出现的复杂问题，例如为符合Rocq的生产率检查器而人为加入静默步、将单子定律视为弱互模拟，以及共归纳互模拟推理。我们将归纳式程序等价关系定义为基元效应上的基础关系关于动作序列和最小上界的同余闭包。这使得我们可以通过将可能不终止程序的等价性归约为其终止近似的等价性，再通过归纳证明这些近似的等价性，从而实现对非终止程序的推理。我们证明了该关系的正确性：只要基础关系正确，等价计算在任何忠实实现这些效应的单子中都具有相同的指称。我们通过展示两个编码叙拉古序列的程序的等价性来说明该框架，而叙拉古序列的终止性是一个尚未解决的数学猜想。
英文摘要：
We present a domain-theoretical formalization of interaction trees in the Rocq prover. Unlike existing formalizations, ours does not rely on Rocq's built-in coinduction. Hence, we avoid complications occurring in earlier works, such as artificially including silent steps to comply with Rocq's productivity checker, treating monad laws as weak bisimulations, and coinductive bisimulation reasoning. We define an inductive program equivalence relation as the congruence closure of a base relation on primitive effects with respect to action sequencing and least upper bounds. This enables reasoning about possibly non-terminating programs by reducing their equivalences to equivalences of their terminating approximations, which are then proved by induction. This relation is proved correct: provided the base relation is correct, equivalent computations have equal denotations in any monad that faithfully implements the effects. We illustrate the framework by showing the equivalence of two programs encoding the Syracuse sequence, whose termination is an open mathematical conjecture.
