SHF: Small: Semantics of Higher Order Probabilistic Programs

概率编程是一种强大的编程范例，它侧重于使用随机性来建模不确定性。最近，由于在机器学习和大数据集统计分析方面的新应用，这一主题重新引起了人们的兴趣。最近几年出现了几种新的概率编程语言，如丘奇、圣公会和风险投资公司，它们允许统计学家构建统计模型、采样概率分布、事件条件和执行贝叶斯推理。这些语言的快速发展产生了对用于规范和推理概率程序行为的良好的语义基础和逻辑工具的需求。描述具有高阶特征的概率程序的行为以及采样和条件调节的机制提出了巨大的数学挑战。最近提出了各种不同的数学结构来捕捉这些语言最显著的特性，它们在精神上相似，但在执行上明显不同。该项目的目标是在每一种情况下隔离起作用的基本原则，并最终确定是否以及如何协调这些不同的方法。该项目研究有用的语义和逻辑工具，以指导概率语言和逻辑的未来发展。该项目提供了基础知识和洞察力，将为下一代具有条件和贝叶斯推理的高阶概率编程语言的设计提供信息，以及对这些语言的编译技术和运行时支持。该项目的研究成果和软件产品将公开提供。项目人员将每年组织两次夏季研究研讨会，通过提供概率编程和贝叶斯推理的入门讲座参与，并与感兴趣的学生一起监督后续项目。该奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

Probabilistic programming is a powerful programming paradigm that focuses on the use of randomness to model uncertainty. The topic has enjoyed a recent resurgence of interest spurred by new applications in machine learning and statistical analysis of large datasets. Several new probabilistic programming languages such as Church, Anglican, and Venture have emerged in the last few years that allow statisticians to construct statistical models, sample probability distributions, condition on events, and perform Bayesian inference. The rapid development of these languages has created a need for sound semantic foundations and logical tools for specification and reasoning about probabilistic program behavior. Describing the behavior of probabilistic programs with higher-order features and mechanisms for sampling and conditioning presents enormous mathematical challenges. A variety of diverse mathematical structures for capturing the most salient properties of these languages have recently been proposed, similar in spirit but diverging markedly in execution. The objective of this project is to isolate the fundamental principles at work in each case and ultimately determine whether and how these diverse approaches can be reconciled. The project investigates useful semantic and logical tools to guide the future development of probabilistic languages and logics. The project provides fundamental knowledge and insights that will inform the design of next-generation higher-order probabilistic programming languages with conditioning and Bayesian inference, along with compiler technology and runtime support for these languages. The research results and software artifact from this project will be made publicly available. The project personnel will organize two annual summer research workshops, and participate by giving introductory lectures on probabilistic programming and Bayesian inference, and supervise followup projects with interested students.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.