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 $\lambda$-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.

翻译：本文提出了一种非标准算术的可实现性解释的新方法。我们在（半）直觉主义可实现性的框架下处理非标准分析，重点关注通过超幂构造非标准分析模型的Lightstone-Robinson方法。特别地，我们考虑扩展了带有存储单元的$\lambda$-演算，该存储单元包含一个整数（状态），以指示计算正在超幂$\cal{M}^{\mathbb{N}}$的哪个切片中进行。我们关注在此设定下可获得的非标准原理（及其计算内容）。具体地，我们为理想化原理和非标准版本的LLPO原理给出了非平凡的实现者。随后，我们讨论如何对该乘积进行商化以模拟Lightstone-Robinson构造。