Chapter 9: Optimal Beta-Reduction
In this chapter we discuss optimal beta-reduction, a rather poorly known technology for reducing lambda terms in the optimal number of steps.