一句话：将 Conway 的正则匹配可判定性结果推广到有限与无限正则树语言，并证明 inside-out 替换下极大解有限且可计算。
论文研究正则树语言的匹配问题，即是否存在变量替换 σ，使 σ(L)⊆R，其中 L、R 是有限秩字母表与变量并集上的正则树语言，σ 将每个变量映为非空树集合并采用 Engelfriet 与 Schmidt 的 inside-out 替换语义。Conway 曾对有限字语言证明该类问题可判定且仅有有限多个极大解，且极大解为正则替换、可有效计算。本文将该结果推广到有限树和无限树上的正则语言，证明 ∃σ∀x: σ(x)≠∅ ∧ σ_io(L)⊆R 可判定；极大解仍有限、正则且可计算。对于 outside-in 扩展 σ_oi，即使在有限树情形下相应问题仍开放。
We study the matching problem of regular tree languages, that is, "$\exists \sigma:\sigma(L)\subseteq R$?" where $L,R$ are regular tree languages over the union of finite ranked alphabets $\Sigma$ and $\mathcal{X}$ where $\mathcal{X}$ is an alphabet of variables and $\sigma$ is a substitution such that $\sigma(x)$ is a set of trees in $T(\Sigma\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 \sigma \forall x\in \mathcal{X}: \sigma(x)\neq \emptyset\wedge \sigma(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(\Sigma\cup\mathcal{X})$ and $R\subseteq T(\Sigma)$ are regular tree languages over finite or infinite trees, then the problem "$\exists \sigma \forall x\in \mathcal{X}: \sigma(x)\neq \emptyset\wedge \sigma_{\mathrm{io}}(L)\subseteq R$?" is decidable. Here, the subscript "$\mathrm{io}$" in $\sigma_{\mathrm{io}}(L)$ refers to "inside-out". Moreover, there are only finitely many maximal solutions $\sigma$, the maximal solutions are regular substitutions and effectively computable. The corresponding question for the outside-in extension $\sigma_{\mathrm{oi}}$ remains open, even in the restricted setting of finite trees.
@article{paperbot1730,
title = {Regular matching problems for infinite trees},
author = {Carlos Camino and Volker Diekert and Besik Dundua and Mircea Marin and Géraud Sénizergues},
journal = {Logical Methods in Computer Science},
volume = {Volume 18, Issue 1},
year = {2022},
doi = {10.46298/lmcs-18(1:25)2022}
}