Interactive Realizability, Monads and Witness Extraction
Interactive Realizability, Monads and Witness Extraction
复制标题
交互式可实现性、Monad 和见证提取
DOI：
--
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
Giovanni Birolo
中科院分区：
文献类型：
--
作者：
Giovanni Birolo
在这篇论文中，我们收集了一些关于“交互式可实现性”的结果，可实现性语义扩展的布劳威尔-海廷-柯尔莫戈罗夫解释（子）经典逻辑，更确切地说，一阶直觉算术（海廷算术，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.