Stateful Realizers for Nonstandard Analysis
From MaRDI portal
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.
Cites work
- scientific article; zbMATH DE number 5851813 (Why is no real title available?)
- scientific article; zbMATH DE number 3166227 (Why is no real title available?)
- scientific article; zbMATH DE number 4002093 (Why is no real title available?)
- scientific article; zbMATH DE number 4038137 (Why is no real title available?)
- scientific article; zbMATH DE number 177651 (Why is no real title available?)
- scientific article; zbMATH DE number 3473961 (Why is no real title available?)
- scientific article; zbMATH DE number 3275554 (Why is no real title available?)
- scientific article; zbMATH DE number 2236625 (Why is no real title available?)
- A Constructive Proof of Dependent Choice, Compatible with Classical Logic
- A functional interpretation for nonstandard arithmetic
- A functional interpretation with state
- A model for intuitionistic non-standard arithmetic
- Bar recursion in classical realisability: dependent choice and continuum hypothesis
- Bounded functional interpretation
- Bounded modified realizability
- Constructive forcing, CPS translations and witness extraction in interactive realizability
- Continuity between Cauchy and Bolzano: issues of antecedents and priority
- Existential witness extraction in classical realizability and via a negative translation
- Implicative algebras: a new foundation for realizability and forcing
- Internal set theory: A new approach to nonstandard analysis
- Interpreting weak Kőnig's lemma in theories of nonstandard arithmetic
- Intuitionistic nonstandard bounded modified realisability and functional interpretation
- Leibniz's infinitesimals: their fictionality, their modern implementations, and their foes from Berkeley to Russell and beyond
- Minimal models of Heyting arithmetic
- Neutrices and External Numbers
- Non-standard analysis
- Nonstandard functional interpretations and categorical models
- Nonstandardness and the bounded functional interpretation
- On the Interpretation of Non-Finitist Proofs--Part I
- On the computational content of the axiom of choice
- On the interpretation of intuitionistic number theory
- Radically Elementary Probability Theory. (AM-117)
- Realizability algebras: a program to well order \(\mathbb R\)
- Realizability interpretation and normalization of typed call-by-need \(\lambda\)-calculus with control
- Realizability. An introduction to its categorical side
- Stateful Realizers for Nonstandard Analysis
- The duality of computation
- The effects of effects on constructivism
- Typed lambda-calculus in classical Zermelo-Fraenkel set theory
- Zur Deutung der intuitionistischen Logik
- ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
Cited in
(2)
This page was built for publication: Stateful Realizers for Nonstandard Analysis
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6135755)
