Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Interaction Equivalence

Beniamino Accattoli, Adrienne Lancelot, Giulio Manzonetto, Gabriele Vanoni

TL;DR

It is proved that interaction equivalence is an equational theory and characterize it as B, the well-known theory induced by Böhm tree equality, the first observational characterization of B obtained without enriching the discriminating power of contexts with extra features such as non-determinism.

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 $λ$-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öhm 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öhm-out technique and of intersection types.

Interaction Equivalence

TL;DR

It is proved that interaction equivalence is an equational theory and characterize it as B, the well-known theory induced by Böhm tree equality, the first observational characterization of B obtained without enriching the discriminating power of contexts with extra features such as non-determinism.

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 -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 , the well-known theory induced by Böhm tree equality. Ours is the first observational characterization of 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.
Paper Structure (80 sections, 37 theorems, 14 equations, 4 figures)

This paper contains 80 sections, 37 theorems, 14 equations, 4 figures.

Table of Contents

  1. Introduction
  2. Equational Contextual Equivalence
  3. Termination $vs$ Time Cost, Equationally
  4. Internal and External
  5. Interaction Equivalence and the Checkers Calculus
  6. Inspecting Black Boxes
  7. Interaction Equivalence and Böhm Trees
  8. Normal Form Bisimilarities
  9. Technical Development
  10. Proof Technique 1: Böhm-Out
  11. Proof Technique 2: Multi Types
  12. The $\lambda$-Calculus
  13. $\lambda$-Terms and Contexts
  14. Rewriting.
  15. Contextual Closure and Reductions.
  16. ...and 65 more sections

Key Result

Theorem 2.6

The head contextual preorder $\sqsubseteq_{}^{\mathrm{ctx}}$ is an inequational $\lambda$-theory. Moreover, it is consistent and extensional.

Figures (4)

  • Figure 1: The $\lambda$-calculus. $\Lambda$ is the set of $\lambda$-terms, $\mathcal{C}$ the class of contexts, $\mathcal{H}$ the subclass of head contexts.
  • Figure 2: The checkers calculus.
  • Figure 3: De Carvalho's multi type system.
  • Figure 4: Checkers multi type system $\vdash^{}_{ }$.

Theorems & Definitions (87)

  • Definition 2.1
  • Definition 2.2: Contextual closure
  • Definition 2.4
  • Definition 2.5
  • Theorem 2.6: Barendregt84
  • Definition 3.1
  • Example 3.3
  • Theorem 3.4: Confluence
  • Lemma 3.5: Substitutivity
  • Example 3.6: The Delicate Role of $\eta$
  • ...and 77 more