论文标题
在概率λ-calculus中非懒惰的好处
The Benefit of Being Non-Lazy in Probabilistic λ-calculus
论文作者
论文摘要
我们考虑了概率应用二次性（PAB），这是一种根据特定的操作语义比较概率未遵循的Lambda术语的应用行为的共同关系。使用懒惰的降低策略在功能主体内不降低，该概念已经研究了两个标准参数传递策略（CBV）和呼叫（CBN）（CBN）。特别是，在CBV的上下文对等上，PAB已被证明是完全抽象的，但在懒惰的CBN中不是。我们通过放松懒惰的约束来克服CBN问题：我们证明PAB在标准降低的上下文对等上是完全抽象的。我们的证明是基于Leventis分离定理，使用概率的Nakajima树作为上下文等价类的树状表示。最后，我们还证明了不平等的完全抽象失败，表明概率的应用相似性严格包含在上下文预订中。
We consider the probabilistic applicative bisimilarity (PAB), a coinductive relation comparing the applicative behaviour of probabilistic untyped lambda terms according to a specific operational semantics. This notion has been studied with respect to the two standard parameter passing policies, call-by-value (cbv) and call-by-name (cbn), using a lazy reduction strategy not reducing within the body of a function. In particular, PAB has been proven to be fully abstract with respect to the contextual equivalence in cbv but not in lazy cbn. We overcome this issue of cbn by relaxing the laziness constraint: we prove that PAB is fully abstract with respect to the standard head reduction contextual equivalence. Our proof is based on the Leventis Separation Theorem, using probabilistic Nakajima trees as a tree-like representation of the contextual equivalence classes. Finally, we prove also that the inequality full abstraction fails, showing that the probabilistic applicative similarity is strictly contained in the contextual preorder.
