一句话:为 FO2[<] 定义的正则关系一致化问题给出判定算法,并提出该逻辑可定义语言的新表示。
本文研究有限字上正则关系的 FO2[<] 一致化问题:给定一个二元正则关系,判定其中是否存在一个与其定义域相同、且可由二变量一阶逻辑 FO2[<] 定义的单值(函数式)子关系。作者提出了一种刻画 FO2[<] 可定义语言的新表示,并基于该表示设计了判定算法,从而证明该一致化问题是可判定的。该表示还可用于解决涉及 FO2[<] 的其他问题,例如判定两个正则语言能否被某个 FO2[<] 可定义语言分离。
A uniformisation of a binary relation is a functional relation contained in it, with the same domain. The uniformisation problem asks whether such a uniformisation can be defined in a given formalism. We solve this problem in the context of regular relations over finite words, for the fragment FO2[<] of First-Order Logic with two variables: we provide an algorithm that decides if a given regular relation over finite words admits a uniformisation definable in FO2[<]. The paper provides a new representation of languages definable in FO2[<], which can be used for the decidability of other problems involving this formalism, e.g. the problem of separability of two regular languages by a language definable in FO2[<].