Stateful Realizers for Nonstandard Analysis
Bruno Dinis, \'Etienne Miquey

TL;DR
This paper introduces a novel realizability framework for nonstandard analysis using an extended lambda calculus with memory, enabling computational interpretations of nonstandard principles like Idealization and LLPO.
Contribution
It presents a new approach to realizability for nonstandard analysis via a lambda calculus with state, capturing nonstandard principles computationally.
Findings
Provided realizers for Idealization and nonstandard LLPO
Extended lambda calculus with memory models ultrapower slices
Discussed quotienting to replicate Lightstone-Robinson construction
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 -calculus with a memory cell, that contains an integer (the state), in order to indicate in which slice of the ultrapower 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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsMathematical and Theoretical Analysis · Computability, Logic, AI Algorithms · History and Theory of Mathematics
