Upper bounds for standardisations and an application

Abstract: "We first present a new proof for the standardisation theorem, a fundamental theorem in [lambda]-calculus. Since our proof is largely built upon structural induction on lambda terms, we can extract some bounds for the number of reduction steps in the standard reduction sequences obtained from transforming any given reduction sequences. This result sharpens the standardisation theorem and establishes a link between lazy and eager evaluation orders in the context of computational complexity. As an application, we establish a super exponential bound for the number of reduction steps in reduction sequences from any given simply typed [lambda]-terms."