论文标题
渐近归一化策略
Strategies for Asymptotic Normalization
论文作者
论文摘要
我们提出了一种在终止是渐近的技术来研究归一化策略的技术，也就是说，它似乎是一个限制，与以有限数量的步骤达到正常形式相反。渐近终止发生在几种情况下，例如有效，尤其是概率计算（其中限制是在可能的输出（或无限lambda-calculi）上的分布，其中限制为无限正常形式，例如boehm树。 作为一个具体应用，我们获得了具有独立关注的结果：逐个呼叫的标准化定理（以及 - 以统一的方式 - 针对呼叫的名称）概率lambda-calculus。
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.
