Document Open Access Logo

Realizability with Stateful Computations for Nonstandard Analysis

Authors Bruno Dinis , Étienne Miquey

PDF
Thumbnail PDF

File

LIPIcs.CSL.2021.19.pdf
  • Filesize: 0.66 MB
  • 23 pages

Document Identifiers

Author Details

Bruno Dinis
  • Faculdade de Ciências, University of Lisbon, Portugal
Étienne Miquey
  • ÉNS de Lyon, Université de Lyon, LIP, France

Funding

  • Dinis, Bruno: The author acknowledges the support of FCT - Fundação para a Ciência e Tecnologia under the projects UIDB/04561/2020 and UIDP/04561/2020, and the research center Centro de Matemática, Aplicações Fundamentais e Investigação Operacional, Universidade de Lisboa.
  • Miquey, Étienne: The author was supported by the Paris Ile-de-France Region and the Inria research team Deducteam (LSV, ÉNS Paris-Saclay).

Acknowledgements

The authors would like to thank Alexandre Miquel for suggesting several ideas at the root of this work and Valentin Blot and Mikhail Katz, as well as the anonymous reviewers, for their accurate remarks and suggestions.

Cite AsGet BibTex

Bruno Dinis and Étienne Miquey. Realizability with Stateful Computations for Nonstandard Analysis. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 19:1-19:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.CSL.2021.19

Abstract

In this paper we propose a new approach to realizability interpretations for nonstandard arithmetic. We deal with nonstandard analysis in the context of 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 shall pay attention to the nonstandard principles (and their computational content) obtainable in this setting. We then discuss how this product could be quotiented to mimic the Lightstone-Robinson construction.

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof theory
  • Theory of computation → Constructive mathematics
Keywords
  • realizability
  • nonstandard analysis
  • states
  • glueing
  • ultrafilters
  • Łoś' theorem

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Federico Aschieri. Constructive forcing, CPS translations and witness extraction in interactive realizability. Mathematical Structures in Computer Science, 27(6):993–1031, 2017. URL: https://doi.org/10.1017/S0960129515000468.
  2. Jeremy Avigad. Weak theories of nonstandard arithmetic and analysis. In Reverse mathematics 2001, volume 21 of Lect. Notes Log., pages 19-46. Assoc. Symbol. Logic, La Jolla, CA, 2005. Google Scholar
  3. Jacques Bair, Piotr Błaszczyk, Elías Guillén, Peter Heinig, Vladimir Kanovei, and Mikhail G. Katz. Continuity between Cauchy and Bolzano: issues of antecedents and priority. British Journal for the History of Mathematics, pages 1-18, 2020. URL: https://doi.org/10.1080/26375451.2020.1770015.
  4. Jacques Bair, Piotr Błaszczyk, Robert Ely, Peter Heinig, and Mikhail Katz. Leibniz’s well-founded fictions and their interpetations. Mat. Stud., 49(2):186-224, 2018. Google Scholar
  5. Henk Barendregt. Lambda calculi with types. In S. Abramsky, Dov M. Gabbay, and S. E. Maibaum, editors, Handbook of Logic in Computer Science (Vol. 2), pages 117-309. Oxford University Press, Inc., New York, NY, USA, 1992. Google Scholar
  6. Benno van den Berg, Eyvind Briseid, and Pavol Safarik. A functional interpretation for nonstandard arithmetic. Ann. Pure Appl. Logic, 163(12):1962-1994, 2012. Google Scholar
  7. Jean-Louis Callot. Trois leçons d'analyse infinitésimale. In J.M. Salanskis and H. Sinaceur, editors, Le labyrinthe du continu, pages 369-381. Springer-Verlag, Paris, 1992. Google Scholar
  8. Bruno Dinis and Fernando Ferreira. Interpreting weak Kőnig’s lemma in theories of nonstandard arithmetic. Mathematical Logic Quarterly, 63(1-2):114-123, 2017. URL: https://doi.org/10.1002/malq.201600066.
  9. Bruno Dinis and Jaime Gaspar. Intuitionistic nonstandard bounded modified realisability and functional interpretation. Ann. Pure Appl. Logic, 169(5):392-412, 2018. URL: https://doi.org/10.1016/j.apal.2017.12.004.
  10. Bruno Dinis and Imme van den Berg. Neutrices and external numbers: A flexible number system. Monographs and Research Notes in Mathematics. CRC Press, Boca Raton, FL, 2019. With a foreword by Claude Lobry. URL: https://doi.org/10.1201/9780429291456.
  11. Kurt Gödel. Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes. Dialectica, 12(3‐4):280-287, 1958. URL: https://doi.org/10.1111/j.1746-8361.1958.tb01464.x.
  12. Timothy Griffin. A formulae-as-type notion of control. In Proceedings of the 17th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '90, pages 47-58, New York, NY, USA, 1990. ACM. URL: https://doi.org/10.1145/96709.96714.
  13. Amar Hadzihasanovic and Benno van den Berg. Nonstandard functional interpretations and categorical models. ND Journal of Formal Logic, 58(3), 2017. Google Scholar
  14. Arend Heyting. Mathematische Grundlagenforschung. Intuitionismus. Beweistheorie. Springer-Verlag, Berlin, 1934. URL: https://doi.org/10.1007/978-3-642-65617-0.
  15. Mikhail Katz and David Sherry. Leibniz’s infinitesimals: their fictionality, their modern implementations, and their foes from Berkeley to Russell and beyond. Erkenntnis, 78(3):571-625, 2013. URL: https://doi.org/10.1007/s10670-012-9370-y.
  16. Stephen Kleene. On the interpretation of intuitionistic number theory. Journal of Symbolic Logic, 10:109-124, 1945. Google Scholar
  17. Andrey Kolmogorov. Zur Deutung der intuitionistischen Logik. Mathematische Zeitschrift, 35(1):58-65, 1932. URL: https://doi.org/10.1007/BF01186549.
  18. Georg Kreisel. On the interpretation of non-finitist proofs, I. J. Symb. Log., 16:241-267, 1951. Google Scholar
  19. Jean-Louis Krivine. Typed lambda-calculus in classical Zermelo-Fraenkel set theory. Arch. Math. Log., 40(3):189-205, 2001. Google Scholar
  20. Jean-Louis Krivine. Realizability in classical logic. In Interactive models of computation and program behaviour. Panoramas et synthèses, 27, 2009. Google Scholar
  21. Jean-Louis Krivine. Realizability algebras: a program to well order ℝ. Logical Methods in Computer Science, 7(3), 2011. URL: https://doi.org/10.2168/LMCS-7(3:2)2011.
  22. Jean-Louis Krivine. Bar Recursion in Classical Realisability: Dependent Choice and Continuum Hypothesis. In Jean-Marc Talbot and Laurent Regnier, editors, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016), volume 62 of Leibniz International Proceedings in Informatics (LIPIcs), pages 25:1-25:11, Dagstuhl, Germany, 2016. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.CSL.2016.25.
  23. Albert Lightstone and Abraham Robinson. Nonarchimedean Fields and Asymptotic Expansions. North-Holland mathematical library. North-Holland, 1975. Google Scholar
  24. Robert Lutz. Rêveries infinitésimales. Gazette des mathématiciens, 34:79-87, 1987. Google Scholar
  25. Alexandre Miquel. Existential witness extraction in classical realizability and via a negative translation. Logical Methods in Computer Science, 7(2):188-202, 2011. URL: https://doi.org/10.2168/LMCS-7(2:2)2011.
  26. Alexandre Miquel. Forcing as a program transformation. In Proceedings of the 2011 IEEE 26th Annual Symposium on Logic in Computer Science, LICS '11, page 197–206, USA, 2011. IEEE Computer Society. URL: https://doi.org/10.1109/LICS.2011.47.
  27. Alexandre Miquel. Implicative algebras: A new foundation for realizability and forcing. ArXiv e-prints, 2020. URL: http://arxiv.org/abs/1802.00528.
  28. Étienne Miquey and Hugo Herbelin. Realizability interpretation and normalization of typed call-by-need λ-calculus with control. In Foundations of software science and computation structures, volume 10803 of Lecture Notes in Comput. Sci., pages 276-292. Springer, Cham, 2018. URL: https://doi.org/10.1007/978-3-319-89366-2_1.
  29. Ieke Moerdijk. A model for intuitionistic non-standard arithmetic. Ann. Pure Appl. Logic, 73(1):37-51, 1995. A tribute to Dirk van Dalen. URL: https://doi.org/10.1016/0168-0072(93)E0071-U.
  30. Ieke Moerdijk and Erik Palmgren. Minimal models of Heyting arithmetic. J. Symbolic Logic, 62(4):1448-1460, 1997. URL: https://doi.org/10.2307/2275651.
  31. Edward Nelson. Internal set theory: A new approach to nonstandard analysis. Bull. Amer. Math. Soc, 1977. Google Scholar
  32. Edward Nelson. Radically Elementary Probability Theory. Annals of Mathematical Studies, vol. 117. Princeton University Press, Princeton, N. J., 1987. Google Scholar
  33. Jerzy Łoś. Quelques remarques, théorèmes et problèmes sur les classes définissables d'algèbres. Journal of Symbolic Logic, 25(2):168–168, 1960. URL: https://doi.org/10.2307/2964232.
  34. Dag Prawitz. Natural deduction. A proof-theoretical study. Acta Universitatis Stockholmiensis. Stockholm Studies in Philosophy, No. 3. Almqvist & Wiksell, Stockholm, 1965. Google Scholar
  35. Abraham Robinson. Non-standard analysis. Proc. Roy. Acad. Sci., 1961. Google Scholar
  36. Abraham Robinson. Non-standard analysis. North-Holland Publishing Co., Amsterdam, 1966. Google Scholar
  37. Alfred Tarski. Une contribution à la théorie de la mesure. Fundamenta Mathematicae, 15(1):42-50, 1930. URL: http://eudml.org/doc/212372.
  38. Jaap van Oosten. Realizability: an introduction to its categorical side, volume 152 of Studies in Logic and the Foundations of Mathematics. Elsevier B. V., Amsterdam, 2008. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact