一句话：定义概率Böhm树与Nakajima树，推广Böhm-out技术以分离概率分布，推进概率λ演算的分离定理。
论文研究按名调用概率λ演算中的观察等价：若任意上下文中两项的头归约以相同概率收敛，则二者观察等价。作者的目标是把经典的分离定理推广到这一概率设定。为此，论文定义概率Böhm树和概率Nakajima树，并将著名的Böhm-out技术与一些处理、分离概率分布的新技术结合。其核心贡献在于为概率λ演算提供新的语义分析工具，用树结构刻画项的潜在行为，并通过分离构造区分观察不等价项，从而给出概率分离定理的证明框架。
We study the notion of observational equivalence in the call-by-name probabilistic λ-calculus, where two terms are said observationally equivalent if under any context, their head reductions converge with the same probability. Our goal is to generalise the separation theorem to this probabilistic setting. To do so we define probabilistic Böhm trees and probabilistic Nakajima trees, and we mix the well-known Böhm-out technique with some new techniques to manipulate and separate probability distributions.
DOI 原文 ·
@inproceedings{paperbot4309,
title = {Probabilistic Böhm Trees and Probabilistic Separation},
author = {Thomas Leventis},
booktitle = {LICS},
year = {2018},
doi = {10.1145/3209108.3209126}
}