Strategies for Asymptotic Normalization

We present a technique to study normalizing strategies when termination is asymptotic, that is, it appears as a limit, as opposite to reaching a normal form in a finite number of steps. Asymptotic termination occurs in several settings, such as effectful, and in particular probabilistic computation – where the limits are distributions over the possible outputs – or infinitary lambda-calculi – where the limits are infinitary normal forms such as Boehm trees. As a concrete application, we obtain a result which is of independent interest: a normalization theorem for Call-by-Value (and – in a uniform way – for Call-by-Name) probabilistic lambda-calculus.