Interaction Equivalence

TL;DR

This paper introduces interaction equivalence, a new form of program equivalence inspired by game semantics, which accounts for interaction steps and forms an equational theory related to B"ohm tree equality.

Contribution

It presents the first observational characterization of B"ohm tree equality without enriching context features, using interaction-based techniques.

Findings

Interaction equivalence is an equational theory.

It characterizes B"ohm tree equality.

First such characterization without extra context features.

Abstract

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.