Abstract
The paper explores known results related to the problem of identifying if a given program terminates on all inputs -- this is a simple generalization of the halting problem. We will see how this problem is related and the notion of proof verifiers. We also see how verifying if a program is terminating involves reasoning through a tower of axiomatic theories -- such a tower of theories is known as Turing progressions and was first studied by Alan Turing in the 1930's. We will see that this process has a natural connection to ordinal numbers. The paper is presented from the perspective of a non-expert in the field of logic and proof theory.
Connections
Explore this paper’s authors, topics and related work.
Building this map preview
BZPEER is loading the nearby papers, people, topics and institutions for this page.
Reviews 0
Write a review
No reviews yet.
Discussion 0
Add a comment
No comments yet.