References & Citations
Computer Science > Logic in Computer Science
Title: Stateful Realizers for Nonstandard Analysis
(Submitted on 11 Oct 2022 (v1), last revised 24 Apr 2023 (this version, v4))
Abstract: 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.
Submission history
From: Bruno Dinis [view email][v1] Tue, 11 Oct 2022 11:17:00 GMT (109kb)
[v2] Fri, 3 Mar 2023 11:54:47 GMT (116kb)
[v3] Tue, 28 Mar 2023 10:36:06 GMT (117kb)
[v4] Mon, 24 Apr 2023 13:54:33 GMT (118kb,D)
Link back to: arXiv, form interface, contact.