Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
MTZ-Fachkongress

Antriebe und Energiesysteme von morgen


Austausch von Automobil- und Energiewirtschaft

Am 14./15. Mai geht es in Chemnitz um die Mobilitätswende durch Elektro- und Wasserstofffahrzeuge.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Searching for Applicable Versions of Computable Structures Kapitel lesen Erstes Kapitel lesen

2021 | OriginalPaper | Buchkapitel

Formally Computing with the Non-computable

verfasst von : Liron Cohen

Erschienen in: Connecting with Computability

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren
Vorheriges Kapitel A Tale of Optimizing the Space Taken by de Bruijn Graphs
Nächstes Kapitel Mapping Monotonic Restrictions in Inductive Inference
Fußnoten
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].
 
Literatur
1.
2.
Allen, S.F., et al.: Innovations in Computational Type Theory using Nuprl. J. Appl. Logic 4(4), 428–469 (2006)MathSciNetCrossRef
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.
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.
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.
van Atten, M., van Dalen, D.: Arguments for the continuity principle. Bull. Symbolic Logic 8(3), 329–347 (2002)MathSciNetCrossRef
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
Metadaten
Titel
Formally Computing with the Non-computable
verfasst von
Liron Cohen
Copyright-Jahr
2021
Buch
Connecting with Computability

Print ISBN: 978-3-030-80048-2

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

Copyright-Jahr: 2021

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

Premium Partner

    Bildnachweise