低层概率编程：指称语义与非确定性控制的探索

"这篇学术论文探讨了低层概率编程的指称语义和非确定性控制，重点关注在处理非结构化控制、一般递归和非确定性等方面的问题。作者提出了一个支持这些特性的指称语义框架，并利用控制流超图来解释概率选择和非确定性选择。该框架允许对非确定性以不同的方式处理，包括程序状态和状态转换器间的非确定性。论文引入了一种基于次概率核幂域的新形式化非确定性方法，并证明了语义对象具有一种称为广义凸性的概念，它是传统凸性的推广。此外，作者还应用这个框架来为概率程序构建静态分析的代数基础。关键词包括概率编程、指称语义、控制流超图、非确定性和幂域。" 本文是关于概率编程领域的一篇研究，主要关注如何为包含非结构化控制、一般递归和非确定性的低层命令式概率程序建立形式语义。概率编程是一个强大的工具，广泛应用于随机算法、加密协议、认知模型和机器学习等领域。然而，为这类程序提供准确的语义模型是一项技术上复杂的任务。 作者王迪、Jan Ho Rummann和Thomas Reps来自卡内基梅隆大学、威斯康星大学和GrammaTech公司，他们提出了一种新的语义框架，该框架能够处理(i)低级别命令式程序中的非结构化控制流，(ii)广泛使用的递归编程范式，以及(iii)非确定性，这对于模拟对抗行为尤其有用。他们通过控制流超图这一概念来表示程序的执行路径，这既考虑了概率选择也考虑了非确定性选择。 在处理非确定性时，他们开发了一种基于次概率核的幂域形式化方法。这种方法允许语义在保持某些代数性质的同时，有多种实例化方式。特别是，它可以支持在程序状态或状态转换器之间的非确定性选择。幂域中的语义对象满足广义凸性，这是一种对传统凸性的扩展，有助于理解和分析程序的行为。 论文中，作者还概述了一个代数框架，可用于概率程序的静态分析。静态分析对于理解程序的行为、检测潜在错误和优化性能至关重要。这种分析工具的建立是基于他们提出的语义模型，可以进一步支持和推动概率编程领域的研究和应用。 这篇论文为低层概率编程提供了深入的理论基础，其贡献在于提出了一个灵活且强大的语义框架，能够处理各种复杂性，特别是非确定性和概率性并存的情况。这对于未来在概率编程语言设计、编译器优化和分析技术上的进步具有重要意义。