带参数的 Church 综合问题
计算机科学中的逻辑
2015-07-01 v2
摘要
对于单子序逻辑（Monadic Logic of Order, MLO）的双变量公式 ψ(X,Y)，Church 综合问题关注是否存在并构造一个算子 Y=F(X)，使得 ψ(X,F(X)) 在 Nat 上普遍有效。B"{u}chi 和 Landweber 证明了 Church 综合问题是可判定的；此外，他们表明如果存在一个算子 F 能解决 Church 综合问题，那么该问题也可以由有限状态自动机定义的算子解决，或者等价地由 MLO 公式解决。我们研究了 Church 综合问题的参数化版本。在此版本中，ψ 可能包含一个一元谓词 P 作为参数。我们证明了针对 P 的 Church 综合问题是可计算的，当且仅当<Nat,<,P>的单子理论是可判定的。我们证明了 B"{u}chi-Landweber 定理仅能扩展到最终周期参数。然而，B"{u}chi-Landweber 定理的 MLO 可定义性部分适用于 Church 综合问题的参数化版本。
引用
@article{arxiv.0708.3477,
title = {The Church Synthesis Problem with Parameters},
author = {Alexander Rabinovich},
journal= {arXiv preprint arXiv:0708.3477},
year = {2015}
}