Wu’s positive lamnda-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.
Accattoli, B., Sacerdoti Coen, C., Wu, J.H. (2025). Positive Sharing and Abstract Machines [10.1007/978-981-95-3585-9_6].
Positive Sharing and Abstract Machines
Sacerdoti Coen C.;
2025
Abstract
Wu’s positive lamnda-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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
