论文标题
咖喱和霍华德见了Borel
Curry and Howard Meet Borel
论文作者
论文摘要
我们表明，从咖喱和霍华德的意义上讲，计数命题逻辑的直觉版本对应于概率事件lambda-calculus的表达类型系统，这是一种车辆演算，其中可以模拟对离散随机功能的呼叫和呼叫评估，可以模拟该系统的call-calculus。值得注意的是，（分别是类型）的证明不仅保证了有效性（分别是终止），而且还揭示了潜在的概率。我们最终表明，通过使用交集操作员赋予类型系统，可以获得一个精确捕获兰巴达（Lambda-Terms）概率行为的系统。
We show that an intuitionistic version of counting propositional logic corresponds, in the sense of Curry and Howard, to an expressive type system for the probabilistic event lambda-calculus, a vehicle calculus in which both call-by-name and call-by-value evaluation of discrete randomized functional programs can be simulated. Remarkably, proofs (respectively, types) do not only guarantee that validity (respectively, termination) holds, but also reveal the underlying probability. We finally show that by endowing the type system with an intersection operator, one obtains a system precisely capturing the probabilistic behavior of lambda-terms.
