paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Formal Languages, Formally and Coinductively

形式语言：形式化与余归纳
LMCS vol.Volume 13, Issue 32017匹配度 2/10 · 论文在Isabelle中余归纳形式化形式语言与Kleene代数，属于定理证明与形式化验证的基础理论工作，但未涉及LLM/Agent、静态分析或程序分析，与用户核心交叉方向（AI→PL改进形式化验证、PL→AI的Agentic程序分析）不匹配。引用 4 inbox
Dmitriy Traytel
定理证明与证明工程逻辑与自动机
dblp: 2026-09-10crossref: 2026-09-10arxiv: 2026-09-10

AI 速览

一句话：在 Isabelle 中以无限 trie 的余归纳表示形式语言，定义正则运算并证明 Kleene 代数公理，证明自动化优于词集合视角。

传统上形式语言被定义为词的集合，而近年来出现了一种余代数/余归纳的替代表示：以按字母表分支的无限 trie（前缀树）来表示语言。该表示已被用于获得语言理论中经典结果的紧凑而优雅的证明。本文在 Isabelle 证明助手中系统研究这一表示：在无限 trie 上定义正则运算，并用余递归与余归纳证明这些运算满足 Kleene 代数公理。通过这一机器化形式化，作者实践了余递归与余归纳技术，并证实余归纳视角在形式化中是有益的——与词的集合视角相比，它在证明自动化方面表现出优势。本文是同名 FSCD 2016 论文的扩展版本。

问题
形式语言通常表示为词的集合，但近期研究表明用无限 trie 的余归纳表示可得到更紧凑优雅的语言理论证明；该表示尚未在证明助手中得到系统形式化与检验。
方法
在 Isabelle 证明助手中将形式语言形式化为按字母表分支的无限 trie，定义并运算、连接、Kleene 星等正则运算，并使用余递归与余归纳证明其 Kleene 代数公理。
评估
在 Isabelle 中完成机器化形式化与证明，通过证明 Kleene 代数公理来检验该余归纳表示，并与词的集合视角在证明自动化方面进行对比，确认其优势。
原文摘要（Abstract）

Traditionally, formal languages are defined as sets of words. More recently, the alternative coalgebraic or coinductive representation as infinite tries, i.e., prefix trees branching over the alphabet, has been used to obtain compact and elegant proofs of classic results in language theory. In this article, we study this representation in the Isabelle proof assistant. We define regular operations on infinite tries and prove the axioms of Kleene algebra for those operations. Thereby, we exercise corecursion and coinduction and confirm the coinductive view being profitable in formalizations, as it improves over the set-of-words view with respect to proof automation.Comment: Extended version of homonymous FSCD 2016 paper

链接与引用

DOI 原文 · arXiv · PDF（开放获取） · DBLP

BibTeX 
@article{Traytel17,
  title = {Formal Languages, Formally and Coinductively},
  author = {Dmitriy Traytel},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 13, Issue 3},
  year = {2017},
  doi = {10.23638/lmcs-13(3:28)2017}
}