Resource Transition Systems and Full Abstraction for Linear Higher-Order Effectful Systems

TL;DR

This paper develops a new operational semantics called resource transition systems for linear higher-order effectful languages, providing a fully abstract characterization of program equivalence that captures both intensional and extensional behaviors.

Contribution

It introduces resource transition systems for effectful linear languages and proves their soundness and completeness for contextual equivalence.

Findings

Resource transition systems effectively model program behaviors.

They achieve full abstraction for contextual equivalence.

The approach clarifies the interaction between copying, linearity, and effects.

Abstract

We investigate program equivalence for linear higher-order(sequential) languages endowed with primitives for computational effects. More specifically, we study operationally-based notions of program equivalence for a linear $\lambda$-calculus with explicit copying and algebraic effects \emph{\`a la} Plotkin and Power. Such a calculus makes explicit the interaction between copying and linearity, which are intensional aspects of computation, with effects, which are, instead, \emph{extensional}. We review some of the notions of equivalences for linear calculi proposed in the literature and show their limitations when applied to effectful calculi where copying is a first-class citizen. We then introduce resource transition systems, namely transition systems whose states are built over tuples of programs representing the available resources, as an operational semantics accounting for both intensional and extensional interactive behaviors of programs. Our main result is a sound and complete characterization of contextual equivalence as trace equivalence defined on top of resource transition systems.