A non-expert view on Turing machines, Proof Verifiers, and Mental reasoning

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.


Similar Publications

An $(r, \ell)$-partition of a graph $G$ is a partition of its vertex set into $r$ independent sets and $\ell$ cliques. A graph is $(r, \ell)$ if it admits an $(r, \ell)$-partition. A graph is well-covered if every maximal independent set is also maximum. Read More


Quantum walks have received a great deal of attention recently because they can be used to develop new quantum algorithms and to simulate interesting quantum systems. In this work, we focus on a model called staggered quantum walk, which employs advanced ideas of graph theory and has the advantage of including the most important instances of other discrete-time models. The evolution operator of the staggered model is obtained from a tessellation cover, which is defined in terms of a set of partitions of the graph into cliques. Read More


In a vertex-colored graph, an edge is happy if its endpoints have the same color. Similarly, a vertex is happy if all its incident edges are happy. Motivated by the computation of homophily in social networks, we consider the algorithmic aspects of the following Maximum Happy Edges (k-MHE) problem: given a partially k-colored graph G, find an extended full k-coloring of G maximizing the number of happy edges. Read More


We study the computational complexity of the infinite-horizon discounted-reward Markov Decision Problem (MDP) with a finite state space $|\mathcal{S}|$ and a finite action space $|\mathcal{A}|$. We show that any randomized algorithm needs a running time at least $\Omega(|\mathcal{S}|^2|\mathcal{A}|)$ to compute an $\epsilon$-optimal policy with high probability. We consider two variants of the MDP where the input is given in specific data structures, including arrays of cumulative probabilities and binary trees of transition probabilities. Read More


We present a bipartite partial function, whose communication complexity is $O((\log n)^2)$ in the model of quantum simultaneous message passing and $\tilde\Omega(\sqrt n)$ in the model of randomised simultaneous message passing. In fact, our function has a poly-logarithmic protocol even in the (restricted) model of quantum simultaneous message passing without shared randomness, thus witnessing the possibility of qualitative advantage of this model over randomised simultaneous message passing with shared randomness. This can be interpreted as the strongest known $-$ as of today $-$ example of "super-classical" capabilities of the weakest studied model of quantum communication. Read More


The positive semidefinite rank of a convex body $C$ is the size of its smallest positive semidefinite formulation. We show that the positive semidefinite rank of any convex body $C$ is at least $\sqrt{\log d}$ where $d$ is the smallest degree of a polynomial that vanishes on the boundary of the polar of $C$. This improves on the existing bound which relies on results from quantifier elimination. Read More


We study the computational complexity of identifying dense substructures, namely $r/2$-shallow topological minors and $r$-subdivisions. Of particular interest is the case when $r=1$, when these substructures correspond to very localized relaxations of subgraphs. Since Densest Subgraph can be solved in polynomial time, we ask whether these slight relaxations also admit efficient algorithms. Read More


Let $\Omega\subset\mathbb{R}^{n+1}$ have minimal Gaussian surface area among all sets satisfying $\Omega=-\Omega$ with fixed Gaussian volume. Let $A=A_{x}$ be the second fundamental form of $\partial\Omega$ at $x$, i.e. Read More


The resolution of linear system with positive integer variables is a basic yet difficult computational problem with many applications. We consider sparse uncorrelated random systems parametrised by the density $c$ and the ratio $\alpha=N/M$ between number of variables $N$ and number of constraints $M$. By means of ensemble calculations we show that the space of feasible solutions endows a Van-Der-Waals phase diagram in the plane ($c$, $\alpha$). Read More


We revisit the undecidability result of rank 3 intersection type inhabitation (Urzyczyn 2009) in pursuit of two goals. First, we strengthen the previous result by showing that intersection type inhabitation is undecidable for types of rank 3 and order 3, i.e. Read More