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.

翻译：我们提出了一种新的逐步方法来证明观测等价性，特别是推理观测等价性的脆弱性。我们的方法基于我们称之为局部推理的技术。该局部推理利用了邻域的图论概念，并从中提取出一种新的、形式化的鲁棒性概念，作为观测等价性的关键充分条件。此外，我们的证明方法能够证明一种广义的观测等价性概念。该广义概念可以量化在语法受限的上下文上，而非所有上下文，并且还可以在归约步数方面进行定量约束。我们使用的操作机制由一个受吉拉尔互动几何启发的超图重写抽象机提供。语言特性（包括函数抽象和应用）的行为由超图重写规则定义。我们使用配备了（高阶）状态的按值调用lambda演算来演示我们的证明方法。