词上WQO的PTL-可分性和闭包
PTL-separability and closures for WQOs on words
摘要：
我们引入了一个灵活的类，以及准序（WQO）的话，概括了排序（不一定连续）的子字。每个这样的WQO诱导一类分段可测试语言（PTLs）的布尔组合向上闭集。这样，一系列正则语言类作为PTL出现。此外，每个WQO保证了所有向下闭集的正则性。我们考虑两个问题。首先，我们研究哪些（也许是非正规的）语言类允许一个决策过程，以决定是否两个给定的语言是可分离的PTL相对于一个给定的WQO。其次，我们希望有效地计算关于这些WQO的向下闭包。我们的第一个主要结果是，对于每一个WQO，在温和的假设下，这两个问题减少到同时无界性问题（ESTA），从而解决了许多强大的系统类。在第二个主要结果中，我们应用该框架通过$\mathcal{B}Σ_1[<, \mathsf{mod}]$（一个带有模块谓词的一阶逻辑片段）来证明正则语言的可分性。
英文摘要：
We introduce a flexible class of well-quasi-orderings (WQOs) on words that generalizes the ordering of (not necessarily contiguous) subwords. Each such WQO induces a class of piecewise testable languages (PTLs) as Boolean combinations of upward closed sets. In this way, a range of regular language classes arises as PTLs. Moreover, each of the WQOs guarantees regularity of all downward closed sets. We consider two problems. First, we study which (perhaps non-regular) language classes permit a decision procedure to decide whether two given languages are separable by a PTL with respect to a given WQO. Second, we want to effectively compute downward closures with respect to these WQOs. Our first main result that for each of the WQOs, under mild assumptions, both problems reduce to the simultaneous unboundedness problem (SUP) and are thus solvable for many powerful system classes. In the second main result, we apply the framework to show decidability of separability of regular languages by $\mathcal{B}Σ_1[<, \mathsf{mod}]$, a fragment of first-order logic with modular predicates.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
