It has been a long-standing open problem whether the strong λ-calculus is a reasonable computational model, i.e. whether it can be implemented within a polynomial overhead with respect to the number of β-steps on models like Turing machines or RAM. Recently, Accattoli and Dal Lago solved the problem by means of a new form of sharing, called useful sharing, and realised via a calculus with explicit substitutions. This paper presents a new abstract machine for the strong λ-calculus based on useful sharing, the Useful Milner Abstract Machine, and proves that it reasonably implements leftmost-outermost evaluation. It provides both an alternative proof that the λ-calculus is reasonable and an improvement on the technology for implementing strong evaluation.
CITATION STYLE
Accattoli, B. (2016). The useful MAM, a reasonable implementation of the strong λ-calculus. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9803 LNCS, pp. 1–21). Springer Verlag. https://doi.org/10.1007/978-3-662-52921-8_1
Mendeley helps you to discover research relevant for your work.