一句话：提出交互等价：只计项与上下文的交互步数，证明它是等式理论并刻画为Böhm树等价B。
上下文等价是程序等价的标准概念，且通常构成等式理论；若把计算时间等内涵信息纳入，则会因代价在归约下并不保持不变而破坏等式理论性质。本文在无类型λ演算中提出交互等价，其灵感来自博弈语义：观察项与上下文之间的交互步数，但忽略项与上下文各自的内部步数。作者证明交互等价仍是一种等式理论，并将其精确刻画为B，即由Böhm树相等诱导的著名理论。这是首个无需借助非确定性等额外判别能力来强化上下文即可对B给出的观察式刻画。为证明该结果，论文发展了基于交互的Böhm-out技术和交类型精细化方法。
Contextual equivalence is the de facto standard notion of program equivalence. A key theorem is that contextual equivalence is an equational theory . Making contextual equivalence more intensional, for example taking into account the time cost of the computation, seems a natural refinement. Such a change, however, does not induce an equational theory, for an apparently essential reason: cost is not invariant under reduction. In the paradigmatic case of the untyped λ -calculus, we introduce interaction equivalence . Inspired by game semantics, we observe the number of interaction steps between terms and contexts but–crucially–ignore their internal steps. We prove that interaction equivalence is an equational theory and characterize it as B , the well-known theory induced by Böhm tree equality. It is the first observational characterization of B obtained without enriching the discriminating power of contexts with extra features such as non-determinism. To prove our results, we develop interaction-based refinements of the Böhm-out technique and of intersection types.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-2409-18709,
title = {Interaction Equivalence},
author = {Beniamino Accattoli and Adrienne Lancelot and Giulio Manzonetto and Gabriele Vanoni},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {POPL},
year = {2025},
doi = {10.1145/3704891}
}