Stateful Realizers for Nonstandard Analysis

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