Strategies for Asymptotic Normalization

TL;DR

This paper introduces a technique for analyzing asymptotic normalization strategies in computational systems where termination is approached as a limit, with applications to probabilistic lambda-calculus and infinitary calculi.

Contribution

It develops a novel method for studying asymptotic normalization, including a normalization theorem for probabilistic lambda-calculus under Call-by-Value and Call-by-Name.

Findings

Normalization theorem for probabilistic lambda-calculus

Applicable to effectful and probabilistic computations

Provides a framework for asymptotic termination analysis

Abstract

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.