一句话:用受限 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。
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.