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 $\lambda$-calculus, we introduce interaction equivalence. Inspired by game semantics, we observe the number of interaction steps between terms and contexts but -- crucially -- ignore their own internal steps. We prove that interaction equivalence is an equational theory and we characterize it as $B$, the well-known theory induced by B\"ohm tree equality. Ours 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\"ohm-out technique and of intersection types.

翻译：上下文等价性是程序等价性的事实标准概念。一个关键定理表明上下文等价性构成一个等式理论。通过使上下文等价性更具内涵性（例如考虑计算的时间成本）似乎是一种自然的精细化改进。然而，这种改变并不会导出等式理论，其本质原因在于：成本在规约下不具有不变性。在无类型λ演算的范式案例中，我们提出了交互等价性。受博弈语义启发，我们观测项与上下文之间的交互步骤数，但关键之处在于忽略它们自身的内部步骤。我们证明了交互等价性构成一个等式理论，并将其刻画为B——即由Böhm树等价性导出的著名理论。我们的研究首次在不通过非确定性等额外特征增强上下文判别能力的情况下，实现了对B的观测性刻画。为证明结论，我们发展了基于交互的Böhm-out技术与交集类型的精细化方法。