nach oben

Tipp

Formalization of the Computational Theory of a Turing Complete Functional Language Model

verfasst von: Thiago Mendonça Ferreira Ramos, Ariane Alves Almeida, Mauricio Ayala-Rincón

Erschienen in: Journal of Automated Reasoning | Ausgabe 4/2022

Einloggen, um Zugang zu erhalten

Abstract

This work presents a formalization in PVS of the computational theory for a computational model given as a class of partial recursive functions called PVS0. The model is built over basic operators, which, when restricted to constants, successor, projections, greater-than, and bijections from tuples of naturals to naturals, results in a proven (formalized) Turing complete model. Complete formalizations of the Recursion theorem and Rice’s theorem are discussed in detail. Other relevant results, such as the undecidability of the Halting problem and the fixed-point theorem, were also fully formalized.

Vorheriger Artikel A Formalization of SQL with Nulls

Nächster Artikel A Formalization of the Smith Normal Form in Higher-Order Logic

Sie möchten Zugang zu diesem Inhalt erhalten? Dann informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

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

über 69.000 Bücher
über 500 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 90 Tage mit der neuen Mini-Lizenz testen!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 58.000 Bücher
über 300 Zeitschriften

aus folgenden Fachgebieten:

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

Jetzt 90 Tage mit der neuen Mini-Lizenz testen!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 50.000 Bücher
über 380 Zeitschriften

aus folgenden Fachgebieten:

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

Jetzt 90 Tage mit der neuen Mini-Lizenz testen!

Jetzt informieren

Alves Almeida, A., Ayala-Rincon, M.: Formalizing the dependency pair criterion for innermost termination. Sci. Comput. Program. 195, 102474 (2020). https://doi.org/10.1016/j.scico.2020.102474

Arts, T.: Termination by absence of infinite chains of dependency pairs. In: 21st International Colloquium on Trees in Algebra and Programming CAAP, LNCS, vol. 1059, pp. 196–210. Springer (1996). https://doi.org/10.1007/3-540-61064-2_38

Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. Theor. Comput. Sci. 236, 133–178 (2000). https://doi.org/10.1016/S0304-3975(99)00207-8 MathSciNetCrossRefMATH

Avelar, A.B.: Formalização da Automação da Terminação Através de Grafos com Matrizes de Medida. Ph.D. thesis, Department of Mathematics, Universidade de Brasília (2014). http://repositorio.unb.br/handle/10482/18069 (in Portuguese)

Boyer, R.S., Moore, J.S.: A Mechanical Proof of the Unsolvability of the Halting Problem. J. Assoc. Comput. Mach. 31(3), 441–458 (1984). https://doi.org/10.1145/828.1882 MathSciNetCrossRefMATH

Carneiro, M.: Formalizing Computability Theory via Partial Recursive Functions. In: 10th International Conference on Interactive Theorem Proving ITP, LIPIcs, vol. 141, pp. 12:1–12:17. Schloss Dagstuhl-Leibniz-Zentrum für Informatik (2019). https://doi.org/10.4230/LIPIcs.ITP.2019.12

Ferreira Ramos, T.M., Muñoz, C.A., Ayala-Rincón, M., Moscato, M.M., Dutle, A., Narkawicz, A.: Formalization of the undecidability of the halting problem for a functional language. In: 25th International Workshop on Logic, Language, Information, and Computation WoLLIC, LNCS, vol. 10944, pp. 196–209. Springer (2018). https://doi.org/10.1007/978-3-662-57669-4_11

Floyd, R.W., Beigel, R.: The Language of Machines: An Introduction to Computability and Formal Languages. W H Freeman & Co (1994). https://doi.org/10.2307/2275690

Forster, Y., Larchey-Wendling, D.: Certified undecidability of intuitionistic linear logic via binary stack machines and Minsky machines. In: 8th ACM SIGPLAN International Conference on Certified Programs and Proofs CPP, pp. 104–117. ACM (2019). https://doi.org/10.1145/3293880.3294096

10.

Forster, Y., Smolka, G.: Weak call-by-value Lambda calculus as a model of computation in Coq. In: 8th International Conference on Interactive Theorem Proving ITP, LNCS, vol. 10499, pp. 189–206. Springer (2017). https://doi.org/10.1007/978-3-319-66107-0_13

11.

Forster, Y., Heiter, E., Smolka, G.: Verification of PCP-related computational reductions in Coq. In: 9th International Conference on Interactive Theorem Proving ITP, LNCS, vol. 10895, pp. 253–269. Springer (2018). https://doi.org/10.1007/978-3-319-94821-8_15

12.

Forster, Y., Kirst, D., Smolka, G.: On Synthetic Undecidability in Coq, with an Application to the Entscheidungsproblem. In: 8th ACM SIGPLAN International Conference on Certified Programs and Proofs CPP, pp. 38–51. ACM (2019). https://doi.org/10.1145/3293880.3294091

13.

Goldfarb, W.D.: The undecidability of the second-order unification problem. Theor. Comput. Sci. 13, 225–230 (1981). https://doi.org/10.1016/0304-3975(81)90040-2 MathSciNetCrossRefMATH

14.

Heiter, E.: Undecidability of the Post Correspondence Problem. Master’s thesis, Faculty of Mathematics and Computer Science, Saarland University (2014). https://www.ps.uni-saarland.de/~heiter/downloads/PCP_Undecidability.pdf

15.

Hopcroft, J.E., Motwani, R., Ullman, J.D.: Introduction to Automata Theory, Languages, and Computation, 3rd edn. Pearson (2008)

16.

Johannisson, K.: Formalizing the Halting Problem in a Constructive type theory. In: International Workshop on Types for Proofs and Programs TYPES, LNCS, vol. 2277, pp. 145–159. Springer (2000). https://doi.org/10.1007/3-540-45842-5_10

17.

Kirst, D., Larchey-Wendling, D.: Trakhtenbrot’s Theorem in Coq, A Constructive Approach to Finite Model Theory. CoRR arXiv:2004.07390 (2020)

18.

Larchey-Wendling, D.: Typing total recursive functions in Coq. In: 8th International Conference on Interactive Theorem Proving ITP, LNCS, vol. 10499, pp. 371–388. Springer (2017). https://doi.org/10.1007/978-3-319-66107-0_24

19.

Larchey-Wendling, D., Forster, Y.: Hilbert’s Tenth Problem in Coq. In: 4th International Conference on Formal Structures for Computation and Deduction FSCD, LIPIcs, vol. 131, pp. 27:1–27:20. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2019). https://doi.org/10.4230/LIPIcs.FSCD.2019.27

20.

Lee, C.S., Jones, N.D., Ben-Amram, A.M.: The size-change principle for program termination. In: Conference Record of POPL 2001: The 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 81–92 (2001). https://doi.org/10.1145/360204.360210

21.

Manolios, P., Vroon, D.: Termination analysis with calling context graphs. In: 18th International Conference on Computer Aided Verification CAV, LNCS, vol. 4144, pp. 401–414. Springer (2006). https://doi.org/10.1007/11817963_36

22.

Muñoz, C.A., Ayala-Rincón, M., Moscato, M.M., Dutle, A.M., Narkawicz, A.J., Almeida, A.A., Avelar, A.B., M. Ferreira Ramos, T.: Formal verification of termination criteria for first-order recursive functions. In: 12th International Conference on Interactive Theorem Proving (ITP 2021), LIPIcs, vol. 193, pp. 27:1–27:17. Schloss Dagstuhl-Leibniz-Zentrum für Informatik (2021). URL https://drops.dagstuhl.de/opus/volltexte/2021/13922

23.

Norrish, M.: Mechanised computability theory. In: Second International Conference on Interactive Theorem Proving ITP, LNCS, vol. 6898, pp. 297–311. Springer (2011). https://doi.org/10.1007/978-3-642-22863-6_22

24.

Post, E.L.: Recursive unsolvability of a problem of Thue. J. Symb. Logic 12(1), 1–11 (1947). https://doi.org/10.2307/2267170 MathSciNetCrossRefMATH

25.

Sipser, M.: Introduction to the Theory of Computation, 3rd edn. Cengage Learning (2012). https://doi.org/10.1145/230514.571645

26.

Spies, S., Forster, Y.: Undecidability of higher-order unification formalised in Coq. In: 9th ACM SIGPLAN International Conference on Certified Programs and Proofs CPP, pp. 143–157. ACM (2020). https://doi.org/10.1145/3372885.3373832

27.

Trakhtenbrot, B.A.: The impossibility of an algorithm for the decidability problem on finite classes. Doklady Akademii Nauk SSSR 70(4), 569–572 (1950) MATH

28.

Turing, A.M.: Computability and \(\lambda \)-definability. J. Symb. Logic 2(4), 153–163 (1937). https://doi.org/10.2307/2268280 CrossRefMATH

29.

Turing, A.M.: Checking a large routine. In: Campbell-Kelly, M. (ed.) The Early British Computer Conferences, pp. 70–72. MIT Press, Cambridge, MA, USA (1989). URL http://dl.acm.org/citation.cfm?id=94938.94952

Titel: Formalization of the Computational Theory of a Turing Complete Functional Language Model
verfasst von: Thiago Mendonça Ferreira Ramos
Ariane Alves Almeida
Mauricio Ayala-Rincón
Publikationsdatum: 30.01.2022
Verlag: Springer Netherlands
Erschienen in: Journal of Automated Reasoning / Ausgabe 4/2022
Print ISSN: 0168-7433
Elektronische ISSN: 1573-0670
DOI: https://doi.org/10.1007/s10817-021-09615-x

Springer Professional

Tipp

Weitere Artikel dieser Ausgabe durch Wischen aufrufen

Formalization of the Computational Theory of a Turing Complete Functional Language Model

Abstract

Sie möchten Zugang zu diesem Inhalt erhalten? Dann informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Premium Partner

Springer Professional

Tipp

Weitere Artikel dieser Ausgabe durch Wischen aufrufen

Abstract

Bitte loggen Sie sich ein, um Zugang zu diesem Inhalt zu erhalten

Sie möchten Zugang zu diesem Inhalt erhalten? Dann informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Weitere Artikel der Ausgabe 4/2022

Larry Wos: Visions of Automated Reasoning

Correction to: Local is Best: Efficient Reductions to Modal Logic K

Six Decades of Automated Reasoning: Papers in Memory of Larry Wos

A Comprehensive Framework for Saturation Theorem Proving

Fast Left Kan Extensions Using the Chase

A Wos Challenge Met

Premium Partner