Positive Sharing and Abstract Machines
摘要
Wu’s positive \(\lambda \) -calculus is a recent call-by-value \(\lambda \) -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 \(\lambda \) -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 \(\lambda \) -calculus, which we prove efficient. The optimization is based on a new slicing technique which is dual to the standard structure of machine environments.