基于可实现性和1-回溯博弈的交互学习
Interactive Learning Based Realizability and 1-Backtracking Games
摘要：
我们证明了基于交互式学习的经典可实现性（介绍了由Aestheri和Berardi的一阶算术）是健全的Coquand游戏语义。特别是，任何实现的蕴涵和否定的算术公式体现了一个获胜的递归策略的1-回溯版本的塔斯基游戏。我们还给出了一些经典证明的实现子和获胜策略提取的例子。我们还勾画了一些正在进行的工作，如何扩展我们的概念，可实现性，以获得完整的Coquand语义，当它仅限于1-回溯游戏。
英文摘要：
We prove that interactive learning based classical realizability (introduced by Aschieri and Berardi for first order arithmetic) is sound with respect to Coquand game semantics. In particular, any realizer of an implication-and-negation-free arithmetical formula embodies a winning recursive strategy for the 1-Backtracking version of Tarski games. We also give examples of realizer and winning strategy extraction for some classical proofs. We also sketch some ongoing work about how to extend our notion of realizability in order to obtain completeness with respect to Coquand semantics, when it is restricted to 1-Backtracking games.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
