论文标题
分解概率的lambda-calculi
Decomposing Probabilistic Lambda-calculi
论文作者
论文摘要
概率的lambda-calculus的概念通常具有规定的减少策略，通常是按名称或呼叫的呼叫，因为演算是不集中的，这些策略会产生不同的结果。这是Lambda-Calculus：Confluence的主要优点之一的突破，这意味着结果与策略的选择无关。我们提出了一个概率的lambda-calculus，其中概率算子分解为两个句法构造：代表概率事件的生成器；和一个根据给定事件的消费者，该术语可在该术语中作用。由此产生的演算是概率事件lambda-calculus，是汇合的，并通过对生成器和消费者结构的概率操作员的不同解释来解释逐个名称和呼叫策略。我们提出了两个减少的概念，一个通过细粒度的本地改写步骤，另一个通过概率事件的产生和消费来提出。微积分的简单类型本质上是标准的，它们传达了强大的归一化。我们演示了如何编码按名称和逐个呼叫概率评估的编码。
A notion of probabilistic lambda-calculus usually comes with a prescribed reduction strategy, typically call-by-name or call-by-value, as the calculus is non-confluent and these strategies yield different results. This is a break with one of the main advantages of lambda-calculus: confluence, which means results are independent from the choice of strategy. We present a probabilistic lambda-calculus where the probabilistic operator is decomposed into two syntactic constructs: a generator, which represents a probabilistic event; and a consumer, which acts on the term depending on a given event. The resulting calculus, the Probabilistic Event Lambda-Calculus, is confluent, and interprets the call-by-name and call-by-value strategies through different interpretations of the probabilistic operator into our generator and consumer constructs. We present two notions of reduction, one via fine-grained local rewrite steps, and one by generation and consumption of probabilistic events. Simple types for the calculus are essentially standard, and they convey strong normalization. We demonstrate how we can encode call-by-name and call-by-value probabilistic evaluation.
