(Optimal) Duplication is not Elementary Recursive

In 1998 Asperti and Mairson proved that the cost of reducing a lambda-term using an optimal lambda-reducer (a la L´evy) cannot be bound by any elementary function in the number of shared-beta steps. We prove in this paper that an analogous result r Lamping’s abstract algorithm. That is, there is no elementary function in the number of shared beta steps bounding the number of duplication steps of the optimal reducer. This theorem vindicates the oracle of Lamping’s algorithm as the culprit for the negative result of Asperti and Mairson. The result is obtained using as a technical tool Elementary Affine Logic. Key words: complexity, elementary affine logic, graph rewriting, optimal reduction

• Type: Conference
• Year: 2000
• Where: POPL
• Authors: Andrea Asperti, Paolo Coppola, Simone Martini
• Keywords: Elementary Affine Logic, Elementary Function, Lamping’s Abstract Algorithm, POPL 2000, Programming Languages