一句话:证明连续 r-正则函数在无处稠密闭零集外局部仿射,且可微 r-正则函数必为仿射,并给出 PSPACE 判定。
论文研究由 Büchi 自动机接受 base-r 表示、从而定义在 [0,1] 上的 r-正则函数。问题在于理解这类连续函数的结构,并判定其可微性。作者证明:连续 r-正则函数在一个无处稠密且 Lebesgue 零测的子集之外局部仿射;由此推出每个可微的 r-正则函数都是仿射函数。进一步,检查一个 r-正则函数是否可微可在 PSPACE 内完成。证明方法关键依赖于 Charlier、Leroy 与 Rigo 发展的自动机理论与度量几何之间的联系。
Following Chaudhuri, Sankaranarayanan, and Vardi, we say that a function $f:[0,1] \to [0,1]$ is $r$-regular if there is a B\"{u}chi automaton that accepts precisely the set of base $r \in \mathbb{N}$ representations of elements of the graph of $f$. We show that a continuous $r$-regular function $f$ is locally affine away from a nowhere dense, Lebesgue null, subset of $[0,1]$. As a corollary we establish that every differentiable $r$-regular function is affine. It follows that checking whether an $r$-regular function is differentiable is in $\operatorname{PSPACE}$. Our proofs rely crucially on connections between automata theory and metric geometry developed by Charlier, Leroy, and Rigo.
DOI 原文 · arXiv · PDF(开放获取) · DBLP
@article{abs-1901-03366,
title = {Continuous Regular Functions},
author = {Alexi Block Gorman and Philipp Hieronymi and Elliot Kaplan and Ruoyu Meng and Erik Walsberg and Zihe Wang and Ziqin Xiong and Hongru Yang},
journal = {Logical Methods in Computer Science},
volume = {Volume 16, Issue 1},
year = {2020},
doi = {10.23638/lmcs-16(1:17)2020}
}