一个经过验证的概率密度函数编译器

Bhat 等人开发了一个归纳编译器，用于计算由简单概率函数语言编写的程序所描述的概率空间的密度函数。在本工作中，我们在定理证明器 Isabelle 中为该语言的一个修改版本实现了这样一个编译器，并给出了其相对于源语言和目标语言语义的可靠性的形式化证明。结合 Isabelle 针对归纳谓词的代码生成功能，这产生了一个完全验证的、可执行的密度编译器。该证明分两步完成，采用了标准的求精方法：首先，定义了一个在定理证明器的逻辑中直接建模的抽象函数进行工作的抽象编译器，并证明其可靠性。然后，将该编译器求精为一个返回目标语言表达式的具体版本。