概率程序的代数程序分析
以下摘要由 AI 根据胶片自动生成。
概率程序的静态分析需要同时处理概率非确定性、恶魔非确定性和抽象非确定性三类汇聚操作，而经典的 Kleene 代数因概率分支导致概率之和超过 1 而不适用。我们提出了 Markov 代数框架（发表于 PLDI’18），其程序指称构成完全偏序集，可扩展支持结构化与非结构化控制流，并对应三种不同的非确定性语义模型。基于此框架还发展出 Newtonian 程序分析方法，支持对概率程序不动点方程的非迭代求解。
以下摘要由 AI 根据胶片自动生成。
概率程序的静态分析需要同时处理概率非确定性、恶魔非确定性和抽象非确定性三类汇聚操作，而经典的 Kleene 代数因概率分支导致概率之和超过 1 而不适用。我们提出了 Markov 代数框架（发表于 PLDI’18），其程序指称构成完全偏序集，可扩展支持结构化与非结构化控制流，并对应三种不同的非确定性语义模型。基于此框架还发展出 Newtonian 程序分析方法，支持对概率程序不动点方程的非迭代求解。