Interaction Equivalence
<|reference_start|>Interaction Equivalence: 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.<|reference_end|>
@article{accattoli2024interaction,
    title={Interaction Equivalence},
    author={Beniamino Accattoli, Adrienne Lancelot, Giulio Manzonetto, Gabriele
  Vanoni},
    journal={arXiv preprint arXiv:2409.18709},
    year={2024},
    archivePrefix={arXiv},
    eprint={2409.18709},
    primaryClass={cs.LO cs.PL}
}