We found a match
Your institution may have access to this item. Find your institution then sign in to continue.
- Title
STATEFUL REALIZERS FOR NONSTANDARD ANALYSIS.
- Authors
DINIS, BRUNO; MIQUEY, ÉTIENNE
- 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 MN 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.
- Subjects
NONSTANDARD mathematical analysis; ARITHMETIC
- Publication
Logical Methods in Computer Science (LMCS), 2023, Vol 19, Issue 2, p1
- ISSN
1860-5974
- Publication type
Article
- DOI
10.46298/LMCS-19(2:7)2023