Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
Searching for Applicable Versions of Computable Structures Read chapter Read first chapter

2021 | OriginalPaper | Chapter

Formally Computing with the Non-computable

Author : Liron Cohen

Published in: Connecting with Computability

Publisher: Springer International Publishing

Log in

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

search-config
loading …

Abstract

Church–Turing computability, which is the standard notion of computation, is based on functions for which there is an effective method for constructing their values. However, intuitionistic mathematics, as conceived by Brouwer, extends the notion of effective algorithmic constructions by also admitting constructions corresponding to human experiences of mathematical truths, which are based on temporal intuitions. In particular, the key notion of infinitely proceeding sequences of freely chosen objects, known as free choice sequences, regards functions as being constructed over time. This paper describes how free choice sequences can be embedded in an implemented formal framework, namely the constructive type theory of the Nuprl proof assistant. Some broader implications of supporting such an extended notion of computability in a formal system are then discussed, focusing on formal verification and constructive mathematics.

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
Footnotes
1
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].
 
2
For simplicity, throughout this paper we focus on choice sequences of natural numbers.
 
3
For a survey of the status of Church Thesis in type-theory-based proof assistants see [20].
 
4
The extended framework described was formalized in Coq’s formalization of Nuprl’s constructive type theory [3, 27].
 
5
This simplified description omits many components of the system which are not relevant to the current paper.
 
6
See, e.g., [35, 37, 38] for discussions on the various types of restrictions.
 
7
Notable exceptions include, e.g., [36, 42].
 
Literature
1.
2.
3.
4.
Avigad, J., Feferman, S.: Gödel’s functional (“Dialectica’’) interpretation. Handb. Proof Theor. 137, 337–405 (1998)CrossRef
5.
Beth, E.W.: Semantic construction of intuitionistic logic. J. Symbolic Logic 22(4), 363–365 (1957)CrossRef
6.
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)
7.
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)
8.
9.
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.
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.
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.
23.
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.
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.
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.
39.
40.
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
Metadata
Title
Formally Computing with the Non-computable
Author
Liron Cohen
Copyright Year
2021
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

Premium Partner

    Image Credits