交互可实现性、单子和见证抽取
Interactive Realizability, Monads and Witness Extraction
摘要：
在这篇论文中，我们收集了一些关于“交互式可实现性”的结果，可实现性语义扩展的布劳威尔-海廷-柯尔莫戈罗夫解释（子）经典逻辑，更确切地说，一阶直觉算术（海廷算术，HA）扩展的法律的排除中间限制简单的存在公式公式（EM 1），一个系统的动机是其利益证明挖掘。我们描述了一个经典的证明涉及实数的交互式解释。我们证明的陈述是关于实平面上的点的一个简单但非平凡的事实。证明使用EM 1来推导实数上的排序的性质，这是不可判定的，因此从构造性的角度来看是有问题的。我们提出了一组新的自然演绎推导约简，可以从HA + EM 1中简单存在公式的封闭推导中提取证人。我们提出的约简的灵感来自于通过提出可证伪的假设并检查它们来学习的非正式思想，以及交互式的可实现性解释。我们提取证人直接从推导HA + EM 1减少，没有编码推导的可实现性解释。我们给出了一个新的介绍互动的可实现性与更明确的语法。我们表示交互式的实现者通过一个抽象的框架，适用于一元的方法在函数编程修改的可实现性，以获得不太严格的概念，可实现性是适合于经典逻辑。特别是，我们使用状态和异常单子的组合，以捕捉从错误中学习的交互式实现器的性质。
英文摘要：
In this dissertation we collect some results about "interactive realizability", a realizability semantics that extends the Brouwer-Heyting-Kolmogorov interpretation to (sub-)classical logic, more precisely to first-order intuitionistic arithmetic (Heyting Arithmetic, HA) extended by the law of the excluded middle restricted to simply existential formulas formulas (EM1), a system motivated by its interest in proof mining. We describe the interactive interpretation of a classical proof involving real numbers. The statement we prove is a simple but non-trivial fact about points in the real plane. The proof employs EM1 to deduce properties of the ordering on the real numbers, which is undecidable and thus problematic from a constructive point of view. We present a new set of reductions for derivations in natural deduction that can extract witnesses from closed derivations of simply existential formulas in HA + EM1. The reduction we present are inspired by the informal idea of learning by making falsifiable hypothesis and checking them, and by the interactive realizability interpretation. We extract the witnesses directly from derivations in HA + EM1 by reduction, without encoding derivations by a realizability interpretation. We give a new presentation of interactive realizability with a more explicit syntax. We express interactive realizers by means of an abstract framework that applies the monadic approach used in functional programming to modified realizability, in order to obtain less strict notions of realizability that are suitable to classical logic. In particular we use a combination of the state and exception monads in order to capture the learning-from-mistakes nature of interactive realizers.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
