This paper presents a formalization of the proof of the undecidability of the halting problem for a functional programming language. The computational model consists of a simple first-order functional language called PVS0 whose operational semantics is specified in the Prototype Verification System (PVS). The formalization is part of a termination analysis library in PVS that includes the specification and equivalence proofs of several notions of termination. The proof of the undecidability of the halting problem required classical constructions such as mappings between naturals and PVS0 programs and inputs. These constructs are used to disprove the existence of a PVS0 program that decides termination of other programs, which gives rise to a contradiction.
CITATION STYLE
Ramos, T. M. F., Muñoz, C., Ayala-Rincón, M., Moscato, M., Dutle, A., & Narkawicz, A. (2018). Formalization of the undecidability of the halting problem for a functional language. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10944 LNCS, pp. 196–209). Springer Verlag. https://doi.org/10.1007/978-3-662-57669-4_11
Mendeley helps you to discover research relevant for your work.