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

被引：1

作者：

Ferreira Ramos, Thiago Mendonca ^{[1
]}

Almeida, Ariane Alves ^{[1
]}

Ayala-Rincon, Mauricio ^{[1
,2
]}

机构：

[1] Univ Brasilia, Dept Comp Sci, Brasilia, DF, Brazil

[2] Univ Brasilia, Dept Math, Brasilia, DF, Brazil

来源：

JOURNAL OF AUTOMATED REASONING | 2022年 / 66卷 / 04期

关键词：

Functional programming models; Automating termination; Computability theory; Halting Problem; Rice's Theorem; Theorem proving; PVS; TERMINATION;

D O I：

10.1007/s10817-021-09615-x

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

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.

引用

页码：1031 / 1063

页数：33

共 50 条

[1] Formalization of the Computational Theory of a Turing Complete Functional Language Model
Thiago Mendonça Ferreira Ramos
Ariane Alves Almeida
Mauricio Ayala-Rincón
[J]. Journal of Automated Reasoning, 2022, 66 : 1031 - 1063
[2] The Game Description Language Is Turing Complete
Saffidine, Abdallah
[J]. IEEE TRANSACTIONS ON COMPUTATIONAL INTELLIGENCE AND AI IN GAMES, 2014, 6 (04) : 320 - 324
[3] The Creative Computational Model and Applications Based on Image Thinking Formalization Theory
Zhu, Ping
[J]. 2015 3RD ASIAN PACIFIC CONFERENCE ON MECHATRONICS AND CONTROL EINGINEERING (APCMCE 2015), 2015, : 278 - 282
[4] Language integration for model formalization
Bouabana-Tebibel, Thouraya
[J]. 2011 IEEE INTERNATIONAL CONFERENCE ON INFORMATION REUSE AND INTEGRATION (IRI), 2011, : 372 - 377
[5] FORMALIZATION OF LANGUAGE SYSTEMS FOR BEHAVIOR THEORY
GEORGE, FH
[J]. PSYCHOLOGICAL REVIEW, 1953, 60 (04) : 232 - 240
[6] Supporting a parallel functional language computational model
Keane, JA
Xu, MQ
[J]. EUROSIM '96 - HPCN CHALLENGES IN TELECOMP AND TELECOM: PARALLEL SIMULATION OF COMPLEX SYSTEMS AND LARGE-SCALE APPLICATIONS, 1996, : 135 - 140
[7] Formalization of the Undecidability of the Halting Problem for a Functional Language
Ferreira Ramos, Thiago Mendonca
Munoz, Cesar
Ayala-Rincon, Mauricio
Moscato, Mariano
Dutle, Aaron
Narkawicz, Anthony
[J]. LOGIC, LANGUAGE, INFORMATION, AND COMPUTATION (WOLLIC 2018), 2018, 10944 : 196 - 209
[8] Are Turing Machines Platonists? Inferentialism and the Computational Theory of Mind
Jon Cogburn
Jason Megil
[J]. Minds and Machines, 2010, 20 : 423 - 439
[9] Are Turing Machines Platonists? Inferentialism and the Computational Theory of Mind
Cogburn, Jon
Megil, Jason
[J]. MINDS AND MACHINES, 2010, 20 (03) : 423 - 439
[10] Computational Complexity in Language String Processing and theory of Halting Problem in Deterministic Turing Machine Accepting Context Sensitive Language, Context Free Language or Regular Language
Sharma, Chetan
Rinku
[J]. 2015 2ND INTERNATIONAL CONFERENCE ON COMPUTING FOR SUSTAINABLE GLOBAL DEVELOPMENT (INDIACOM), 2015, : 2091 - 2096

← 1 2 3 4 5 →