无限字上带后继的一阶片段
形式语言与自动机理论
2015-03-17 v1 计算机科学中的逻辑
摘要
我们考虑一阶逻辑的片段，并允许有限字和无限字同时作为模型。除相等关系外，唯一的二元关系是顺序比较<和后继谓词+1。我们根据代数和拓扑性质给出了片段Sigma2 = Sigma2[<,+1]和FO2 = FO2[<,+1]的特征刻画。为此，我们引入了无限字上的因子拓扑。结果表明，语言L属于FO2和Sigma2的交集当且仅当L是某个FO2语言的内部。对称地，语言属于FO2和Pi2的交集当且仅当它是某个FO2语言的拓扑闭包。片段Delta2（定义为Sigma2和Pi2的交集）恰好包含FO2中的闭开语言。特别地，在无限字上，Delta2是FO2的真子类。我们的刻画给出了所有这些片段在有限字和无限字上成员关系问题的可判定性；作为推论，我们也得到了无限字上的可判定性。此外，我们给出了有限字上点深度3/2的一个新的可判定代数刻画。有限字上点深度3/2的可判定性最早由Gla{\ss}er和Schmitz在STACS 2000上证明，无限字上FO2成员关系问题的可判定性由Wilke在1998年的教授资格论文中证明，而无限字上Sigma2的可判定性此前未知。
引用
@article{arxiv.1101.0115,
title = {First-order Fragments with Successor over Infinite Words},
author = {Jakub Kallas and Manfred Kufleitner and Alexander Lauser},
journal= {arXiv preprint arXiv:1101.0115},
year = {2015}
}
备注
Presented at STACS 2011