Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Stateful Realizers for Nonstandard Analysis

Bruno Dinis, Étienne Miquey

TL;DR

The paper develops a stateful realizability framework for nonstandard arithmetic by merging Lightstone–Robinson ultrapower techniques with a memory state in an extended λ-calculus. This enables a computational interpretation of nonstandard principles such as Idealization and a nonstandard LLPO, and it establishes a glueing structure via slices that leads to an evidenced-frame presentation and connections to higher-order logic. Key results include the introduction of a value-restriction operator to manage computation with state, a concrete realization of natural-number behavior in the nonstandard setting, and a detailed treatment of Transfer, Overspill, and Idealization, together with a LLPO$^{\mathrm{st}}$ realization and a disjunction mechanism. The quotienting approach to mimic Lightstone–Robinson is explored, highlighting both its expressive advantages and the limitations it imposes on realizability composition, with links to forcing and categorical realizability frameworks. Overall, the work provides a computable bridge between nonstandard analysis and realizability theory, offering concrete realizers for nonstandard principles and a structured semantic foundation for further higher-order extensions.

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

Stateful Realizers for Nonstandard Analysis

TL;DR

The paper develops a stateful realizability framework for nonstandard arithmetic by merging Lightstone–Robinson ultrapower techniques with a memory state in an extended λ-calculus. This enables a computational interpretation of nonstandard principles such as Idealization and a nonstandard LLPO, and it establishes a glueing structure via slices that leads to an evidenced-frame presentation and connections to higher-order logic. Key results include the introduction of a value-restriction operator to manage computation with state, a concrete realization of natural-number behavior in the nonstandard setting, and a detailed treatment of Transfer, Overspill, and Idealization, together with a LLPO realization and a disjunction mechanism. The quotienting approach to mimic Lightstone–Robinson is explored, highlighting both its expressive advantages and the limitations it imposes on realizability composition, with links to forcing and categorical realizability frameworks. Overall, the work provides a computable bridge between nonstandard analysis and realizability theory, offering concrete realizers for nonstandard principles and a structured semantic foundation for further higher-order extensions.

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.
Paper Structure (18 sections, 30 theorems, 70 equations, 1 figure)

This paper contains 18 sections, 30 theorems, 70 equations, 1 figure.

Table of Contents

  1. Introduction
  2. The ultrapower construction
  3. Realizability in a nutshell
  4. Heyting second-order arithmetic
  5. Realizability interpretation of HA2
  6. Introducing value restriction
  7. Realizability with slices
  8. Stateful computations
  9. Stateful realizability interpretation
  10. Glueing
  11. The induced evidenced frame
  12. Nonstandard principles in realizability with slices
  13. Natural numbers
  14. Nonstandard reasoning principles
  15. Idealization
  16. ...and 3 more sections

Key Result

Proposition 3.3

If $A$ and $A'$ are two formulas of HA2 such that $A \cong A'$, then for all valuations $\rho$ closing both $A$ and $A'$ we have $|A|_\rho = |A'|_\rho$.

Figures (1)

  • Figure 1: Type system

Theorems & Definitions (80)

  • Definition 2.1
  • Definition 2.2
  • Definition 3.1: Valuation
  • Definition 3.2: Realizability interpretation
  • Proposition 3.3: Miquel11
  • proof
  • Definition 3.4: Substitution
  • Definition 3.5
  • Definition 3.6
  • Theorem 3.7: Adequacy Miquel11
  • ...and 70 more