paperbot · PL 论文追踪

全部论文 待读 收藏

P2 A Curry-Howard Approach to Church's Synthesis

Church 合成问题的 Curry-Howard 方法
LMCS vol.Volume 15, Issue 42019匹配度 2/10 · 论文属于逻辑与自动机、程序合成理论，讨论 Church 合成的 Curry-Howard 对应与 MSO 直觉主义变体，与用户关注的静态分析、LLM/Agent 交叉、浮点程序分析或贝叶斯程序分析没有直接交集；仅同属 PL/形式化方法大领域，匹配度低。引用 4 inbox
Cécilia Pradic, Colin Riba
逻辑与自动机程序合成
crossref: 2026-09-10

AI 速览

一句话：引入无穷字上 MSO 的直觉主义变体 SMSO，通过基于自动机的可实现性模型建立其与 Church 合成的可靠性与完备性。

Church 合成问题问是否存在有限状态流转换器满足给定的输入输出规约。对无穷字上的 MSO 规约，该问题理论上可用自动机与博弈算法求解。本文用 Curry-Howard 对应重新审视 Church 合成，引入 SMSO——无穷字上 MSO 的直觉主义变体。借助基于自动机的可实现性（realizability）模型，作者证明 SMSO 相对合成是可靠且完备的，从而将合成问题转化为证明与程序构造问题。

问题
Church 合成问题问是否存在满足给定输入输出规约的有限状态流转换器；对无穷字上的 MSO 规约，理论上可用自动机与博弈算法判定。
方法
通过 Curry-Howard 对应引入无穷字上 MSO 的直觉主义变体 SMSO，并构造基于自动机的可实现性模型来诠释其证明。
评估
证明 SMSO 相对 Church 合成是可靠且完备的，即合成问题的解与 SMSO 中的证明/可实现项相对应。
原文摘要（Abstract）

Church's synthesis problem asks whether there exists a finite-state stream transducer satisfying a given input-output specification. For specifications written in Monadic Second-Order Logic (MSO) over infinite words, Church's synthesis can theoretically be solved algorithmically using automata and games. We revisit Church's synthesis via the Curry-Howard correspondence by introducing SMSO, an intuitionistic variant of MSO over infinite words, which is shown to be sound and complete w.r.t. synthesis thanks to an automata-based realizability model.

链接与引用

DOI 原文 · PDF（开放获取） ·

BibTeX 
@article{paperbot739,
  title = {A Curry-Howard Approach to Church's Synthesis},
  author = {Cécilia Pradic and Colin Riba},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 15, Issue 4},
  year = {2019},
  doi = {10.23638/lmcs-15(4:13)2019}
}