paperbot · PL 论文追踪

全部论文 待读 收藏

P2 First-order tree-to-tree functions

一阶树到树函数
LICS Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science2020匹配度 2/10 · 论文是纯逻辑与自动机理论，研究一阶/MSO 可定义树到树变换的分解定理，与用户关注的静态分析、LLM/Agent 程序分析、浮点程序分析及贝叶斯程序分析无直接关联；仅与形式化方法基础有非常间接的联系。引用 0 inbox
Mikołaj Bojańczyk, Amina Doumane
逻辑与自动机
crossref: 2026-09-12

AI 速览

一句话：证明一阶和 MSO 可定义的树到树变换具有分解定理：均可由基本变换经函数复合等组合子生成。

本文研究可用一阶逻辑或一元二阶逻辑（MSO）定义的树到树变换。核心问题是刻画这类变换的表达能力与结构。作者证明了一个分解定理：每个此类树到树变换都可以从若干基本（prime）变换出发，例如树到树同态或前序遍历，再通过函数复合等组合子构造得到。该结果给出了 FO/MSO 树变换的生成式描述，揭示了其可由简单构件组合而成的结构性质，有助于理解逻辑可定义树转换与自动机/形式语言之间的联系。论文属于理论计算机科学与程序语言中形式语言方向的数学证明结果。

问题
如何刻画由一阶逻辑或 MSO 定义的树到树变换，并理解其结构？
方法
通过证明分解定理，将任意此类变换分解为基本变换（如树到树同态、前序遍历）与组合子（如函数复合）。
评估
以数学证明给出结构性结果，未涉及实验评估。
原文摘要（Abstract）

We study tree-to-tree transformations that can be defined in first-order logic or monadic second-order logic. We prove a decomposition theorem, which shows that every transformation can be obtained from prime transformations, such as tree-to-tree homomorphisms or pre-order traversal, by using combinators such as function composition.

链接与引用

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

BibTeX 
@inproceedings{paperbot5528,
  title = {First-order tree-to-tree functions},
  author = {Mikołaj Bojańczyk and Amina Doumane},
  booktitle = {LICS},
  year = {2020},
  doi = {10.1145/3373718.3394785}
}