Church 综合的 Curry-Howard 方法
计算机科学中的逻辑
2023-06-22 v4
摘要
Church 综合问题询问是否存在一个满足给定输入输出规范的有限状态流转换器。对于用无限字上的单子二阶逻辑（MSO）编写的规范，理论上可以使用自动机和游戏算法求解 Church 综合。我们通过 Curry-Howard 对应重新审视 Church 综合，引入了 SMSO，即无限字上 MSO 的直觉主义变体，并借助基于自动机的可实现性模型，证明了其在综合方面是可靠且完备的。
引用
@article{arxiv.1803.08958,
title = {A Curry-Howard Approach to Church's Synthesis},
author = {Cécilia Pradic and Colin Riba},
journal= {arXiv preprint arXiv:1803.08958},
year = {2023}
}