Abstract

We will first review the known results on optimal reduction in the lambda-calculus and its relations to linear logic. After discussing Asperti and Mairson's result that optimal lambda-reduction is not Kalmar elementary, we will show that optimal lambda-reduction remains non Kalmar elementary even for lambda-terms typeable in Girard's Elementary Linear Logic.