Formalization of the Computational Theory of a Turing Complete Functional Language Model
Journal of automated reasoning(2022)
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.
MoreTranslated text
Key words
Functional programming models,Automating termination,Computability theory,Halting Problem,Rice’s Theorem,Theorem proving,PVS
AI Read Science
Must-Reading Tree
Example
Generate MRT to find the research sequence of this paper
Chat Paper
Summary is being generated by the instructions you defined