2018/10/01 by Beniamino Accattoli · 1 citation
Computer Science · #Logic, programming, and type systems #Logic, Reasoning, and Knowledge #Advanced Algebra and Logic
paper · pdf · doi:10.1016/j.entcs.2018.10.003
openalex publication_date 2018/10/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/31
This divulgative paper is about time cost models for the λ -calculus. To allow the definition of standard complexity classes such as P or EXP directly in the λ -calculus, a cost models has to be reasonable, that is, polynomially related to the one of Turing machines. For the λ -calculus the existence of an evaluation strategy whose number of steps is a reasonable cost model has been a long-standing open problem. Positive answers to special cases were known since 1995, but a solution for the general case has been provided only in 2014. The problem is peculiar because some of its aspects are somewhat counterintuitive. This paper is devoted to explain the subtleties of this fundamental topic. The key point that is often misunderstood, and that is here discussed at length, is that being efficient and being reasonable are two unrelated properties of evaluation strategies. A second focus of the paper is the relationship between standard and reasonable strategies.