paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Probabilistic Rewriting and Asymptotic Behaviour: on Termination and Unique Normal Forms

概率重写与渐近行为:终止性与唯一范式
LMCS vol.Volume 18, Issue 22022匹配度 3/10 · 该论文研究概率重写系统的终止性与唯一范式等形式语义性质,属于PL理论/形式化验证方向,但与用户核心关注的LLM/Agent静态分析、浮点程序分析及贝叶斯程序分析交叉较少,缺少工程落地或LLM工具化线索。引用 7 inbox
Claudia Faggian
crossref: 2026-09-10

AI 速览

一句话:为概率重写系统建立分析终止性、唯一极限分布与唯一范式的证明技术,并用于比较归约策略。

概率重写系统虽在操作语义上重要,但其抽象分析工具仍很有限。本文研究概率重写的渐近行为,核心问题是归约结果是否唯一,即是否存在唯一极限分布(以及相应的唯一范式)。作者围绕终止性与唯一范式建立一组证明技术,用以分析和比较不同归约策略;其目标不是给出具体算法实现,而是为概率演算(如概率 lambda 演算)提供操作分析工具,因为这类演算的求值存在多种归约选择,因而可能产生不同归约路径。摘要未报告实验评估,贡献主要在理论框架与证明方法。

问题
概率重写系统缺少成熟的抽象分析工具,难以判断不同归约路径是否收敛到唯一结果(唯一极限分布/唯一范式)。
方法
围绕终止性与唯一范式,发展一套证明技术来分析和比较不同归约策略,用于概率演算的操作语义分析。
评估
摘要未报告具体实现或实验评估;工作属于面向概率 lambda 演算等概率演算的理论证明技术研究。
原文摘要(Abstract)

While a mature body of work supports the study of rewriting systems, abstract tools for Probabilistic Rewriting are still limited. In this paper we study the question of uniqueness of the result (unique limit distribution), and develop a set of proof techniques to analyze and compare reduction strategies. The goal is to have tools to support the operational analysis of probabilistic calculi (such as probabilistic lambda-calculi) where evaluation allows for different reduction choices (hence different reduction paths).

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@article{paperbot1706,
  title = {Probabilistic Rewriting and Asymptotic Behaviour: on Termination and Unique Normal Forms},
  author = {Claudia Faggian},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 18, Issue 2},
  year = {2022},
  doi = {10.46298/lmcs-18(2:5)2022}
}