paperbot · PL 论文追踪

全部论文 待读 收藏

P2 SD-Regular Transducer Expressions for Aperiodic Transformations

面向非周期变换的 SD-正则转换器表达式
LICS 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)2021匹配度 1/10 · 该论文属于纯自动机与形式语言理论,研究一阶可定义函数的转换器表达式刻画,未涉及静态分析、LLM/Agent、浮点程序分析或贝叶斯程序分析等用户核心方向,仅与形式化方法基础有非常间接的联系。引用 0 inbox
Luc Dartois, Paul Gastin, Shankara Narayanan Krishna
crossref: 2026-09-12

AI 速览

一句话:用受限 Kleene 星的 SD-正则转换器表达式刻画一阶可定义函数,推广 Schützenberger 的 SF=AP 结果。

一阶可定义函数可由非周期确定性双向转换器等模型刻画。本文解决用表达式刻画一阶可定义函数的问题,推广 Schützenberger 的 SF=AP 结果。作者定义 SD-正则转换器表达式(SDRTE):Kleene 星仅出现在具有有界同步延迟的前缀码这类非周期语言上,并用无歧义和、Hadamard 积、无歧义 Cauchy 积和 fc-chained Kleene 星等组合子构造。为从非周期确定性双向转换器构造 SDRTE,他们具体化 SD=AP,证明非周期语言可由无歧义且稳定的 SD-正则表达式刻画,并对描述转换器定义域的这种表达式做结构归纳。最后给出基于函数复合的等价形式,可将 fc-chained 星替换为 1-star。

问题
为一阶可定义函数(等价地,非周期确定性双向转换器)提供类似正则表达式的表达式刻画,并推广 Schützenberger 的 SF=AP 结果。
方法
定义 SD-正则转换器表达式(SDRTE),限制 Kleene 星只作用于有界同步延迟前缀码的非周期语言,并用无歧义和、Hadamard 积、无歧义 Cauchy 积与 fc-chained 星等组合子构造;通过具体化 SD=AP 并对稳定无歧义 SD-正则表达式做结构归纳,从非周期双向转换器构造 SDRTE。
评估
以理论构造和等价性证明进行评估:证明 SDRTE 能刻画非周期确定性双向转换器定义的一阶可定义函数,并给出基于函数复合、可将 fc-chained 星替换为 1-star 的等价形式。
原文摘要(Abstract)

FO transductions, aperiodic deterministic two-way transducers, as well as aperiodic streaming string transducers are all equivalent models for first order definable functions. In this paper, we solve the problem of expressions capturing first order definable functions, thereby generalizing the seminal SF=AP (star-free expressions = aperiodic languages) result of Schützenberger. Our result also generalizes a lesser known characterization by Schutzenberger of aperiodic languages by SD-regular expressions (SD=AP). We show that every first order definable function over finite words captured by an aperiodic deterministic two-way transducer can be described with an SD-regular transducer expression (SDRTE). An SDRTE is a regular expression where Kleene stars are used in a restricted way: they can appear only on aperiodic languages which are prefix codes of bounded synchronization delay. SDRTEs are constructed from simple functions using the combinators unambiguous sum (deterministic choice), Hadamard product, and unambiguous versions of the Cauchy product and the fc-chained Kleene-star, where the star is restricted as mentioned. In order to construct an SDRTE associated with an aperiodic deterministic two-way transducer, (i) we concretize Schutzenberger's SD=AP result, by proving that aperiodic languages are captured by SD-regular expressions which are unambiguous and stabilising; (ii) by structural induction on the unambiguous, stabilising SD-regular expressions describing the domain of the transducer, we construct SDRTEs. Finally, we also look at various formalisms equivalent to SDRTEs which use the function composition, allowing to trade the fc-chained star for a 1-star.

链接与引用

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

BibTeX
@inproceedings{paperbot6218,
  title = {SD-Regular Transducer Expressions for Aperiodic Transformations},
  author = {Luc Dartois and Paul Gastin and Shankara Narayanan Krishna},
  booktitle = {LICS},
  year = {2021},
  doi = {10.1109/lics52264.2021.9470738}
}