Existential witness extraction in classical realizability and via a negative translation
Existential witness extraction in classical realizability and via a negative translation
复制标题
经典可实现性和通过否定翻译的存在证人提取
DOI：
10.2168/lmcs-7(2:2)2011
复制
发表时间：
2011
期刊：
影响因子：
--
通讯作者：
Alexandre Miquel
中科院分区：
文献类型：
--
作者：
Alexandre Miquel
我们展示了如何使用 Krivine 的经典可实现性从经典证明中提取存在证据——其中经典证明被解释为带有 call/cc 控制运算符的 lambda_c 项。我们首先回顾经典可实现性的基本框架（在经典二阶算术中），并展示如何用原始数字扩展它以实现更快的计算。然后，我们通过讨论取决于存在公式的形状的几种技术，展示如何在这个框架中执行证人提取。特别是，我们表明，在 Sigma^0_1 情况下，Krivine 的证人提取方法通过非常适合直觉二阶算术的负转换简化为 Friedman 的方法。最后，我们讨论使用 call/cc 而不是否定翻译的优点，特别是从实现的角度来看。
We show how to extract existential witnesses from classical proofs using Krivine's classical realizability--where classical proofs are interpreted as lambda_c-terms with the call/cc control operator. We first recall the basic framework of classical realizability (in classical second-order arithmetic) and show how to extend it with primitive numerals for faster computations. Then we show how to perform witness extraction in this framework, by discussing several techniques depending on the shape of the existential formula. In particular, we show that in the Sigma^0_1-case, Krivine's witness extraction method reduces to Friedman's through a well-suited negative translation to intuitionistic second-order arithmetic. Finally we discuss the advantages of using call/cc rather than a negative translation, especially from the point of view of an implementation.