基于线性逻辑加权关系模型的高阶概率验证研究
计算机科学中的逻辑
2026-05-01 v1
摘要
判定一个概率程序是否几乎必然终止（即概率为1）的问题是（即概率为1）是不可判定的，并且实际上是-完全的。因此，越来越多的文献探索了可以证明此类及相关问题（半）可判定的程序类别。在这项工作中，我们考虑概率高阶递归模式（PHORS）语言的终止问题。利用线性逻辑的加权关系语义，我们将此问题转化为计算与所解释程序相关的合适生成函数。通过这种方式，我们为一类程序建立了几乎必然终止的可判定性，该类程序通过一种带有界指数的类型规则，扩展了Li等人的仿射PHORS。为实现这一点，我们证明了此类程序的生成函数总是代数的，即多项式方程的解，从而提供了一种回答终止问题的有效方法。
引用
@article{arxiv.2604.27986,
title = {On Higher-Order Probabilistic Verification via the Weighted Relational Model of Linear Logic},
author = {Ugo Dal Lago and Guido Fiorillo and Paolo Pistone},
journal= {arXiv preprint arXiv:2604.27986},
year = {2026}
}