论文标题
非标准分析的状态实现者
Stateful Realizers for Nonstandard Analysis
论文作者
论文摘要
在本文中，我们提出了一种新的方法来实现非标准算术的解释。我们在（半）直觉的可实现性的背景下处理非标准分析，重点是通过超能够通过超能进行非标准分析模型的浅石 - 罗宾森构建。特别是，我们考虑了包含整数（状态）的$λ$ -calculus的扩展，以指出超级$ \ cal {m}^{m}^{\ mathbb {n}} $的分布。我们关注在这种情况下可获得的非标准原则（及其计算内容）。特别是，我们为理想化和LLPO原理的非标准版本提供了非平凡的实现。然后，我们讨论如何对该产品进行标记以模仿Lightstone-Robinson的结构。
In this paper we propose a new approach to realizability interpretations for nonstandard arithmetic. We deal with nonstandard analysis in the context of (semi)intuitionistic realizability, focusing on the Lightstone-Robinson construction of a model for nonstandard analysis through an ultrapower. In particular, we consider an extension of the $λ$-calculus with a memory cell, that contains an integer (the state), in order to indicate in which slice of the ultrapower $\cal{M}^{\mathbb{N}}$ the computation is being done. We pay attention to the nonstandard principles (and their computational content) obtainable in this setting. In particular, we give non-trivial realizers to Idealization and a non-standard version of the LLPO principle. We then discuss how to quotient this product to mimic the Lightstone-Robinson construction.
