论文标题
无限树的定期匹配问题
Regular matching problems for infinite trees
论文作者
论文摘要
我们研究了普通树语言的匹配问题，即“ $ \存在σ：σ（l）\ subseteq r $？”其中$ l，r $是有限排名字母$σ$和$ \ nathcal {x} $的常规树语言，其中$ \ nathcal {x} $是变量的字母，$σ$是替代品，是$σ（x）$的$σ（x）$是$ t（x）$ in $ t in $ t for $ t（for for $ t（for）。 \ Mathcal {x} $。在这里，$ h $表示一组“孔”，用于定义树木的“排序”串联。康威（Conway）在1971年出版的经典教科书“常规代数和有限机器”中研究了有限单词的语言的特殊情况。是可决定的。此外，只有许多最大解决方案有限，最大解决方案是常规替代，并且可以有效地计算。当$ l，r $是有限和无限树的普通语言时，我们会扩展康威的结果，而从Engelfriet和Schmidt的意义上则将语言替换应用到内而外（1977/78）。 More precisely, we show that if $L\subseteq T(Σ\cup\mathcal{X})$ and $R\subseteq T(Σ)$ are regular tree languages over finite or infinite trees, then the problem "$\exists σ\forall x\in \mathcal{X}: σ(x)\neq \emptyset\wedge σ_ {\ mathrm {io}}（l）\ subseteq r $？”是可决定的。在这里，$σ_ {\ mathrm {io}}}（l）$ in $σ_ {\ mathrm {io} $的下标（io} $）$是指“ Inside-Out-Out”。此外，只有许多最大解决方案$σ$有限，最大解决方案是常规替换，可以有效地计算。外部扩展的相应问题$σ_ {\ mathrm {oi}} $即使在有限树的受限设置中也是开放的。
We study the matching problem of regular tree languages, that is, "$\exists σ:σ(L)\subseteq R$?" where $L,R$ are regular tree languages over the union of finite ranked alphabets $Σ$ and $\mathcal{X}$ where $\mathcal{X}$ is an alphabet of variables and $σ$ is a substitution such that $σ(x)$ is a set of trees in $T(Σ\cup H)\setminus H$ for all $x\in \mathcal{X}$. Here, $H$ denotes a set of "holes" which are used to define a "sorted" concatenation of trees. Conway studied this problem in the special case for languages of finite words in his classical textbook "Regular algebra and finite machines" published in 1971. He showed that if $L$ and $R$ are regular, then the problem "$\exists σ\forall x\in \mathcal{X}: σ(x)\neq \emptyset\wedge σ(L)\subseteq R$?" is decidable. Moreover, there are only finitely many maximal solutions, the maximal solutions are regular substitutions, and they are effectively computable. We extend Conway's results when $L,R$ are regular languages of finite and infinite trees, and language substitution is applied inside-out, in the sense of Engelfriet and Schmidt (1977/78). More precisely, we show that if $L\subseteq T(Σ\cup\mathcal{X})$ and $R\subseteq T(Σ)$ are regular tree languages over finite or infinite trees, then the problem "$\exists σ\forall x\in \mathcal{X}: σ(x)\neq \emptyset\wedge σ_{\mathrm{io}}(L)\subseteq R$?" is decidable. Here, the subscript "$\mathrm{io}$" in $σ_{\mathrm{io}}(L)$ refers to "inside-out". Moreover, there are only finitely many maximal solutions $σ$, the maximal solutions are regular substitutions and effectively computable. The corresponding question for the outside-in extension $σ_{\mathrm{oi}}$ remains open, even in the restricted setting of finite trees.
