-
Stateful Realizers for Nonstandard Analysis
Authors:
Bruno Dinis,
Étienne Miquey
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 intege…
▽ More
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.
△ Less
Submitted 24 April, 2023; v1 submitted 11 October, 2022;
originally announced October 2022.
-
Revisiting the duality of computation: an algebraic analysis of classical realizability models
Authors:
Étienne Miquey
Abstract:
In an impressive series of papers, Krivine showed at the edge of the last decade how classical realizability provides a surprising technique to build models for classical theories. In particular, he proved that classical realizability subsumes Cohen's forcing, and even more, gives rise to unexpected models of set theories. Pursuing the algebraic analysis of these models that was first undertaken b…
▽ More
In an impressive series of papers, Krivine showed at the edge of the last decade how classical realizability provides a surprising technique to build models for classical theories. In particular, he proved that classical realizability subsumes Cohen's forcing, and even more, gives rise to unexpected models of set theories. Pursuing the algebraic analysis of these models that was first undertaken by Streicher, Miquel recently proposed to lay the algebraic foundation of classical realizability and forcing within new structures which he called implicative algebras. These structures are a generalization of Boolean algebras based on an internal law representing the implication. Notably, implicative algebras allow for the adequate interpretation of both programs (i.e. proofs) and their types (i.e. formulas) in the same structure. The very definition of implicative algebras takes position on a presentation of logic through universal quantification and the implication and, computationally, relies on the call-by-name $λ$-calculus. In this paper, we investigate the relevance of this choice, by introducing two similar structures. On the one hand, we define disjunctive algebras, which rely on internal laws for the negation and the disjunction and which we show to be particular cases of implicative algebras. On the other hand, we introduce conjunctive algebras, which rather put the focus on conjunctions and on the call-by-value evaluation strategy. We finally show how disjunctive and conjunctive algebras algebraically reflect the well-known duality of computation between call-by-name and call-by-value.
△ Less
Submitted 13 January, 2020; v1 submitted 7 October, 2019;
originally announced October 2019.
-
A constructive proof of dependent choice in classical arithmetic via memoization
Authors:
Étienne Miquey
Abstract:
In a recent paper, Herbelin developed dPA${^ω}$, a calculus in which constructive proofs for the axioms of countable and dependent choices could be derived via the memoization of choice functions. However, the property of normalization (and therefore the one of soundness) was only conjectured. The difficulty for the proof of normalization is due to the simultaneous presence of dependent types (for…
▽ More
In a recent paper, Herbelin developed dPA${^ω}$, a calculus in which constructive proofs for the axioms of countable and dependent choices could be derived via the memoization of choice functions. However, the property of normalization (and therefore the one of soundness) was only conjectured. The difficulty for the proof of normalization is due to the simultaneous presence of dependent types (for the constructive part of the choice), of control operators (for classical logic), of coinductive objects (to encode functions of type ${\mathbb{N} \to A}$ into streams (${a_0},{a_1},...$)) and of lazy evaluation with sharing (for memoizing these coinductive objects). Elaborating on previous works, we introduce in this paper a variant of dPA${^ω}$ presented as a sequent calculus. On the one hand, we take advantage of a variant of Krivine classical realizability that we developed to prove the normalization of classical call-by-need. On the other hand, we benefit from dL${_{\hat{tp}}}$, a classical sequent calculus with dependent types in which type safety is ensured by using delimited continuations together with a syntactic restriction. By combining the techniques developed in these papers, we manage to define a realizability interpretation à la Krivine of our calculus that allows us to prove normalization and soundness. This paper goes over the whole process, starting from Herbelin's calculus dPA${^ω}$ until our introduction of its sequent calculus counterpart dLPA${^ω}$.
△ Less
Submitted 18 March, 2019;
originally announced March 2019.
-
A sequent calculus with dependent types for classical arithmetic
Authors:
Étienne Miquey
Abstract:
In a recent paper, Herbelin developed a calculus dPA$^ω$ in which constructive proofs for the axioms of countable and dependent choices could be derived via the encoding of a proof of countable universal quantification as a stream of it components. However, the property of normalization (and therefore the one of soundness) was only conjectured. The difficulty for the proof of normalization is due…
▽ More
In a recent paper, Herbelin developed a calculus dPA$^ω$ in which constructive proofs for the axioms of countable and dependent choices could be derived via the encoding of a proof of countable universal quantification as a stream of it components. However, the property of normalization (and therefore the one of soundness) was only conjectured. The difficulty for the proof of normalization is due to the simultaneous presence of dependent dependent types (for the constructive part of the choice), of control operators (for classical logic), of coinductive objects (to encode functions of type $N\rightarrow A$ into streams $(a_0,a_1,\ldots)$) and of lazy evaluation with sharing (for these coinductive objects).Building on previous works, we introduce in this paper a variant of dPA$^ω$ presented as a sequent calculus. On the one hand, we take advantage of a variant of Krivine classical realizability we developed to prove the normalization of classical call-by-need. On the other hand, we benefit of dL, a classical sequent calculus with dependent types in which type safety is ensured using delimited continuations together with a syntactic restriction. By combining the techniques developed in these papers, we manage to define a realizability interpretation {à} la Krivine of our calculus that allows us to prove normalization and soundness.
△ Less
Submitted 20 December, 2018; v1 submitted 24 May, 2018;
originally announced May 2018.
-
Realizability Interpretation and Normalization of Typed Call-by-Need $$λ$$-calculus With Control
Authors:
Étienne Miquey,
Hugo Herbelin
Abstract:
We define a variant of realizability where realizers are pairs of a term and a substitution. This variant allows us to prove the normalization of a simply-typed call-by-need $$λ$-$calculus with control due to Ariola et al. Indeed, in such call-by-need calculus, substitutions have to be delayed until knowing if an argument is really needed. In a second step, we extend the proof to a call-by-need $…
▽ More
We define a variant of realizability where realizers are pairs of a term and a substitution. This variant allows us to prove the normalization of a simply-typed call-by-need $$λ$-$calculus with control due to Ariola et al. Indeed, in such call-by-need calculus, substitutions have to be delayed until knowing if an argument is really needed. In a second step, we extend the proof to a call-by-need $$λ$$-calculus equipped with a type system equivalent to classical second-order predicate logic, representing one step towards proving the normalization of the call-by-need classical second-order arithmetic introduced by the second author to provide a proof-as-program interpretation of the axiom of dependent choice.
△ Less
Submitted 2 March, 2018;
originally announced March 2018.
-
Classical realizability and arithmetical formulæ
Authors:
Mauricio Guillermo,
Étienne Miquey
Abstract:
In this paper we treat the specification problem in classical realizability (as defined in [20]) in the case of arithmetical formulæ. In the continuity of [10] and [11], we characterize the universal realizers of a formula as being the winning strategies for a game (defined according to the formula). In the first section we recall the definition of classical realizability, as well as a few technic…
▽ More
In this paper we treat the specification problem in classical realizability (as defined in [20]) in the case of arithmetical formulæ. In the continuity of [10] and [11], we characterize the universal realizers of a formula as being the winning strategies for a game (defined according to the formula). In the first section we recall the definition of classical realizability, as well as a few technical results. In Section 5, we introduce in more details the specification problem and the intuition of the game-theoretic point of view we adopt later. We first present a game $G_1$, that we prove to be adequate and complete if the language contains no instructions "quote" [18], using interaction constants to do substitution over execution threads. Then we show that as soon as the language contain "quote", the game is no more complete, and present a second game ${G}_2$ that is both adequate and complete in the general case. In the last Section, we draw attention to a model-theoretic point of view, and use our specification result to show that arithmetical formulæ are absolute for realizability models.
△ Less
Submitted 11 April, 2015; v1 submitted 4 March, 2014;
originally announced March 2014.
