Top

Published in:

2021 | OriginalPaper | Chapter

Formally Computing with the Non-computable

Author : Liron Cohen

Published in: Connecting with Computability

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

The chapter delves into the formalization of intuitionistic mathematics, specifically Brouwer’s choice sequences, within a proof assistant. It extends the traditional Church–Turing computability by integrating these sequences, which are considered non-computable, into a mechanized system. This integration not only broadens the theoretical notion of computation but also enables practical applications in formal verification and constructive mathematics. The paper discusses the technical modifications made to the Nuprl proof assistant to support the new computational theory, including changes to the library, computation system, type system, and semantics. It also highlights the implications of this formalization for the verification of complex systems and the practice of constructive mathematics. The work aims to bridge the gap between intuitionistic principles and computational theories, providing a robust framework for exploring the wider implications of this novel computational theory.

AI Generated

This summary of the content was generated with the help of AI.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter A Tale of Optimizing the Space Taken by de Bruijn Graphs

next chapter Mapping Monotonic Restrictions in Inductive Inference

Variants of bar induction were shown to be compatible with constructive type theory, and used to enhance the logical functionality implemented by proof assistants [29, 32].

For simplicity, throughout this paper we focus on choice sequences of natural numbers.

For a survey of the status of Church Thesis in type-theory-based proof assistants see [20].

The extended framework described was formalized in Coq’s formalization of Nuprl’s constructive type theory [3, 27].

This simplified description omits many components of the system which are not relevant to the current paper.

See, e.g., [35, 37, 38] for discussions on the various types of restrictions.

Notable exceptions include, e.g., [36, 42].

Agda wiki. http://wiki.portal.chalmers.se/agda/pmwiki.php

Allen, S.F., et al.: Innovations in Computational Type Theory using Nuprl. J. Appl. Logic 4(4), 428–469 (2006)MathSciNetCrossRef

Anand, A., Rahli, V.: Towards a formally verified proof assistant. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 27–44. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08970-6_3CrossRef

Avigad, J., Feferman, S.: Gödel’s functional (“Dialectica’’) interpretation. Handb. Proof Theor. 137, 337–405 (1998)CrossRef

Beth, E.W.: Semantic construction of intuitionistic logic. J. Symbolic Logic 22(4), 363–365 (1957)CrossRef

Bickford, M., Cohen, L., Constable, R.L., Rahli, V.: Computability beyond church-turing via choice sequences. In: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, pp. 245–254 (2018)

Bickford, M., Cohen, L., Constable, R.L., Rahli, V.: Open Bar - a Brouwerian intuitionistic logic with a pinch of excluded middle. In: Baier, C., Goubault-Larrecq, J., (eds.), 29th EACSL Annual Conference on Computer Science Logic (CSL), vol. 183, LIPIcs, pp. 11:1–11:23 (2021)

Bishop, E., Bridges, D.: Constructive Analysis. GW, vol. 279. Springer, Heidelberg (1985). https://doi.org/10.1007/978-3-642-61667-9CrossRefMATH

Bridges, D., Richman, F.: Varieties of Constructive Mathematics. London Mathematical Society Lecture Notes Series, Cambridge University Press (1987)

10.

Bridges, D., Richman, F.: Varieties of Constructive Mathematics. Cambridge University Press, Cambridge (1988)MATH

11.

Brouwer, L.E.J.: Begründung der mengenlehre unabhängig vom logischen satz vom ausgeschlossen dritten. zweiter teil: Theorie der punkmengen. Koninklijke Nederlandse Akademie van Wetenschappen te Amsterdam 12(7), (1919). Reprinted in Brouwer, L.E.J., Collected Works, Volume I: Philosophy and Foundations of Mathematics, edited by Heyting, A., North-Holland Publishing Co., Amsterdam, pp. 191–221 (1975)

12.

Brouwer, L.E.J.: From frege to Gödel: A Source Book in Mathematical Logic, 1879–1931, chapter On the Domains of Definition of Functions (1927)

13.

Church, A.: An unsolvable problem of elementary number theory. Am. J. Math. 58(2), 345–363 (1936)MathSciNetCrossRef

14.

Constable, R.L. et al.: Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall Inc, Hoboken (1986)

15.

Coquand, T., Mannaa, B.: The independence of markov’s principle in type theory. In: Kesner, D., Pientka, B., (eds.) FSCD 2016, vol. 52 of LIPIcs, pp. 17:1–17:18. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2016)

16.

Coquand, T., Mannaa, B., Ruch, F.: Stack semantics of type theory. In: 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pp. 1–11 (2017)

17.

The Coq Proof Assistant. http://coq.inria.fr/

18.

Dyson, V.H., Kreisel, G.: Analysis of Beth’s Semantic Construction of Intuitionistic Logic. Stanford University (1961)

19.

Escardó, M.H., Xu, C.: The inconsistency of a Brouwerian continuity principle with the curry-howard interpretation. In: 13th International Conference on Typed Lambda Calculi and Applications (TLCA), pp. 153–164 (2015)

20.

Forster, Y.: Church’s thesis and related axioms in Coq’s type theory. In: Baier, C., Goubault-Larrecq, J., (eds.) 29th EACSL Annual Conference on Computer Science Logic (CSL 2021), vol. 183 of Leibniz International Proceedings in Informatics (LIPIcs), pp. 21:1–21:19, Dagstuhl, Germany (2021). Schloss Dagstuhl-Leibniz-Zentrum für Informatik

21.

Kleene, S.C., Vesley, R.E.: The Foundations of Intuitionistic Mathematics, Especially in Relation to Recursive Functions. North-Holland Publishing Company, Amsterdam (1965)

22.

Kreisel, G.: On weak completeness of intuitionistic predicate logic. J. Symb. Log. 27(2), 139–158 (1962)MathSciNetCrossRef

23.

Kreisel, G.: Lawless sequences of natural numbers. Compositio Mathematica 20, 222–248 (1968)MathSciNetMATH

24.

Kripke, S.A.: Semantical considerations on modal logic. Acta Philosophica Fennica 16(1963), 83–94 (1963)MathSciNetMATH

25.

Martin-Löf, P.: Constructive mathematics and computer programming. In: Proceedings of the Sixth International Congress for Logic, Methodology, and Philosophy of Science, pp. 153–175. Amsterdam, North Holland (1982)

26.

Moschovakis, J.R.: An intuitionistic theory of lawlike, choice and lawless sequences. In: Logic Colloquium’90: ASL Summer Meeting in Helsinki, pp. 191–209. Association for Symbolic Logic (1993)

27.

Rahli, V., Bickford, M.: A nominal exploration of intuitionism. In: Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP, pp. 130–141, p. 2016. New York (2016)

28.

Rahli, V., Bickford, M.: Validating Brouwer’s continuity principle for numbers using named exceptions. Math. Struct. Comput. Sci. 28(6), 942–990 (2018)MathSciNetCrossRef

29.

Rahli, V., Bickford, M., Cohen, L., Constable, R.L.: Bar induction is compatible with constructive type theory. J. ACM 66(2), 13:1–13:35 (2019)

30.

Rahli, V., Bickford, M., Constable, R. L.: Bar induction: The Good, the Bad, and the Ugly. In: 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pp. 1–12 (2017)

31.

Rahli, V., Cohen, L., Bickford, M.: A verified theorem prover backend supported by a monotonic library. In: Barthe, G., Sutcliffe, G., Veanes, M., (eds.) LPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, vol. 57 of EPiC Series in Computing, pp. 564–582 (2018)

32.

Rathjen, M.: A note on bar induction in constructive set theory. Math. Logic Q. 52(3), 253–258 (2006)MathSciNetCrossRef

33.

Troelstra, A.S.: A note on non-extensional operations in connection with continuity and Recursiveness. Indagationes Mathematicae 39(5), 455–462 (1977)MathSciNetCrossRef

34.

Troelstra, A.S.: Choice Sequences: a Chapter of Intuitionistic Mathematics. Clarendon Press, Oxford (1977)MATH

35.

Troelstra, A.S.: Choice sequences and informal rigour. Synthese 62(2), 217–227 (1985)MathSciNetCrossRef

36.

Troelstra, A.S., van Dalen, D.: Constructivism in Mathematics, An Introduction, vol. I. II. North-Holland, Amsterdam (1988)

37.

van Atten, M.: On Brouwer. Cengage Learning, Wadsworth Philosophers (2004)MATH

38.

van Atten, M., van Dalen, D.: Arguments for the continuity principle. Bull. Symbolic Logic 8(3), 329–347 (2002)MathSciNetCrossRef

39.

van Dalen, D.: An interpretation of intuitionistic analysis. Ann. Math. Logic 13(1), 1–43 (1978)MathSciNetCrossRef

40.

van Dalen, D.: L.E.J. Brouwer: Topologist, Intuitionist, Philosopher: How Mathematics is Rooted in Life. Springer, New York (2013) https://doi.org/10.1007/978-1-4471-4616-2

41.

Veldman, W.: Understanding and using brouwer’s continuity principle. In: Schuster, P., Berger, U., Osswald, H. (eds.) Reuniting the Antipodes - Constructive and Nonstandard Views of the Continuum. Synthese Library (Studies in Epistemology, Logic, Methodology, and Philosophy of Science), vol. 306, pp. 285–302. Springer, Dordrecht (2001). https://doi.org/10.1007/978-94-015-9757-9_24

42.

Veldman, W.: Some applications of brouwer’s thesis on bars. In: Atten, M., Boldini, P., Bourdeau, M., Heinzmann, G. (eds.) One Hundred Years of Intuitionism (1907–2007). Publications of the Henri Poincaré Archives, pp. 326–340. Berkhäuser, Berlin (2008) https://doi.org/10.1007/978-3-7643-8653-5_20

Title: Formally Computing with the Non-computable
Author: Liron Cohen
Publisher: Springer International Publishing
Book: Connecting with Computability
Print ISBN: 978-3-030-80048-2

Electronic ISBN: 978-3-030-80049-9

Copyright Year: 2021
DOI: https://doi.org/10.1007/978-3-030-80049-9_12

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"