一句话：提出基于局部推理与图邻域的鲁棒性条件，逐步证明观察等价性，并推广到受限上下文与归约步数。
论文研究观察等价性的证明问题，特别是其脆弱性与上下文量化带来的困难。作者提出一种逐步、基于局部推理的新方法：利用图论中的邻域概念，将“鲁棒性”形式化为观察等价的充分条件，从而把全局上下文推理约化为局部检查。其操作机制是受 Girard 交互几何启发的超图重写抽象机，函数抽象、应用等语言特征由超图重写规则描述。该方法还能证明推广的观察等价性：既可将量化限制在语法受限的上下文，也可按归约步数作定量约束。作者以带高阶状态的按值调用 lambda 演算为例展示了该证明方法。
We propose a new step-wise approach to proving observational equivalence, and in particular reasoning about fragility of observational equivalence. Our approach is based on what we call local reasoning. The local reasoning exploits the graphical concept of neighbourhood, and it extracts a new, formal, concept of robustness as a key sufficient condition of observational equivalence. Moreover, our proof methodology is capable of proving a generalised notion of observational equivalence. The generalised notion can be quantified over syntactically restricted contexts instead of all contexts, and also quantitatively constrained in terms of the number of reduction steps. The operational machinery we use is given by a hypergraph-rewriting abstract machine inspired by Girard's Geometry of Interaction. The behaviour of language features, including function abstraction and application, is provided by hypergraph-rewriting rules. We demonstrate our proof methodology using the call-by-value lambda-calculus equipped with (higher-order) state.
@article{paperbot3423,
title = {A robust graph-based approach to observational equivalence},
author = {Dan R. Ghica and Koko Muroya and Todd Waugh Ambridge},
journal = {Logical Methods in Computer Science},
volume = {Volume 21, Issue 2},
year = {2025},
doi = {10.46298/lmcs-21(2:8)2025}
}