Positive Sharing and Abstract Machines

Wu’s positive λ-calculus is a recent call-by-value λ-calculus with sharing coming from Miller and Wu’s study of the proof-theoretical concept of focalization. Accattoli and Wu showed that it simplifies a technical aspect of the study of sharing; namely it rules out the recurrent issue of renaming chains, that often causes a quadratic time slowdown. In this paper, we define the natural abstract machine for the positive λ-calculus and show that it suffers from an inefficiency: the quadratic slowdown somehow reappears when analyzing the cost of the machine. We then design an optimized machine for the positive λ-calculus, which we prove efficient. The optimization is based on a new slicing technique which is dual to the standard structure of machine environments.