Abstracting the Undecidability of the Halting Problem

Question

Let us work in some constructive metalogic (where we have at least the following: Natural numbers, Booleans, Lists, Disjoint Union, and Sets).

To reason about Turing machines, we could (probably) define the following (metalogical) functions and sets:

TMData : Set == Seq(Bool) 
// TMData is the set of all finite boolean sequences

TMEval(alg: TMData, input: TMData) : TMData + "null" 
// TMEval is the 'big step operational semantics' of Turing machines.
// It 'executes' `alg` with `input`, and returns "null" on divergence or the answer.

Now, we can prove the following metalogical theorem:

SolvesHalting(halt_solver: TMData) == 
               ∀inp_alg: TMData, TMEval(halt_solver, inp_alg) = (TMEval(inp_alg,[]) = "null" ? [0] : [1])
// SolvesHalting is a metalogical predicate which says whether `halt_solver` can solve the halting problem.

THEOREM HaltingUnsolvable == ∀ alg: TMData : ¬ SolvesHalting(alg)
// It is possible to prove this theorem in our metalogic. We would have to unfold the definitions of TMEval and TMData.

Now, I could define a "new" programming language / notion of computation. For instance, we could define:

* PythonData, PythonEval //PythonData is all python programs, which are ASTs
* GodelData, GodelEval //GodelData is just Nat. These are the traditional partial recursive functions
* TaggedTMData, TaggedTMEval //This is simply 'a copy' of TMData, where each finite boolean sequence has a tag '*', which makes the set different from TMData.

Now, I think that we could prove a version of the Halting problem undecidability for each of these (and more), which are different statements in the metalogic. My question is whether there is a way we can abstract the essence of this problem? The idea is to 'not repeat ourselves' with the proof, and have a single proof.

• Maybe we can define something like a HaltUndecidable to be a set (the data - eg. TMData, TaggedTMData, etc.) and an evaluation function subject to various conditions which are required for the halting problem?
  • Then <TMData, TMEval>, <PythonData, PythonEval>, etc. are instances of HaltUndeciable, and we don't have to prove anything else..
  • I'm curious whether one of the well-formedness conditions requires the set to be countably infinite? Could it be possible to prove a version of the halting problem where the set is uncountably infinite?
• Another approach might be to define the notion of a simulation between our different notions of computation, and prove a theorem that says that one version of the Halting problem "lifts" to another version if there is a simulation. Is this the way one typically goes about this?
• Does anything change significantly when our metalogic is classical, instead of constructive?

Answer 1

It's possible to abstract the structure of the argument. However, it's not really possible to do so correctly without knowing the details of arguments for specific systems. I've formalized two versions of the argument here, in Agda, but I'll explain roughly how they work below.

As with realizability, I'll use partial applicative systems and partial combinatory algebras as abstract computational systems.

• A PAS is a set $\cal A$ with a partial binary operation $\cdot : \cal A → A \rightharpoonup A$, where the operation is an abstraction of applying a computation (the left argument) to some input (the right argument). In my formalization, I use an alternate definition where we iterate the binary operation to have a partial interpretation of formal terms in $0$ variables, $\mathsf{Tm}_{\mathcal{A}} \rightharpoonup \cal A$. (Also note that I write $f \cdot x \cdot y$ to mean $(f \cdot x) \cdot y$)
• A PCA is a PAS that has representations of every formal applicative term over $\cal A$ with $n+1$ variables. This means that given an equation of the form: $$\mathsf{C}\ x\ y\ \ldots = E$$ where $E$ is an expression built out of the variables $x, y, \ldots$, elements of $\cal A$, and application, there is an element $\sf c : \cal A$ such that $\mathsf{c} \cdot a \cdot b \cdot \ldots$ is equivalent to interpreting $E[x := a, y := b, \ldots]$ in the PAS. This is equivalent to assuming that representatives of the $\sf s$ and $\sf k$ combinators exist in $\cal A$, but much more convenient.

Lambda calculi naturally have this structure, but pretty much all computational systems (that I'm aware of) can fit into it. From combinatory completeness, we can define representations that will be needed later:

• $\newcommand{\true}{\mathsf{true}} \true\ x\ y = x$
• $\newcommand{\false}{\mathsf{false}} \false\ x\ y = y$
• $\newcommand{\id}{\mathsf{id}} \id\ x = x$

You can also look at this as allowing representatives of lambda expressions $λx\ y\ \ldots . E$ where the $λ$ binder occurs only once at the outermost level of the expression. Any other lambda expression must be turned into a sequence of combinator definitions.

It's also necessary for there to be $\newcommand{\Tm}{\mathsf{Tm}} ω : \Tm_{\cal A}$ such that evaluating $ω$ is undefined. From this we can get an element $Ω : \cal A$ such that $Ω \cdot a$ is always undefined (it is the representative of $λx. ω$, essentially). Being undefined in the PAS is the abstract equivalent of not halting, and there is nothing in the definition that actually forces any term to be undefined.

Given this setup, it's possible to copy the logic used to show that the halting problem for Turing machines is undecidable.

• Define a halting decider to be $\newcommand{\h}{\mathsf{h}} \h \in \cal A$ such that
  1. $\h \cdot a \cdot b$ is always defined and either $\true$ or $\false$
  2. if $\h \cdot a \cdot b$ is $\true$, then $a \cdot b$ is well-defined
  3. if $\h \cdot a \cdot b$ is $\false$ then $a \cdot b$ is undefined
• Define $δ \in \cal A$ to be the representative of $λ x. \h \cdot x \cdot x \cdot Ω \cdot \id \cdot \id$, and consider $δ \cdot δ$
• $δ \cdot δ$ is equivalent to $\h \cdot δ \cdot δ \cdot Ω \cdot \id \cdot \id$
  1. If $\h \cdot δ \cdot δ$ is $\true$, then the above expression is $\true \cdot Ω \cdot \id \cdot \id$ which is equivalent to $Ω \cdot \id$, which is undefined. This contradicts the second part of the halting decider specification.
  2. If $\h \cdot δ \cdot δ$ is $\false$, then the expression is instead well-defined with result $\id$. This contradicts the third part of the halting decider specification.
• Since the first part of the halting decider says that one of these cases must hold, it just cannot be the case that any $\h$ is a halting decider.

However, there's a problem with formulating the argument this way. If you instantiate to the lambda calculus, what it proves is:

• There is no total term $\h$ such that if $\h\ x\ y = \true$ then $x\ y$ normalizes, and if $\h\ x\ y = \false$ then $x\ y$ doesn't normalize.

But this is a weak result. In the lambda calculus, all that $\h$ can do is apply $x$ and $y$ to things, and by considering $\h\ Ω\ Ω$, we can tell that it actually must not apply its arguments at all if it successfully yields $\true$ or $\false$. So, the first part of the halting decider specification ensures that $\h$ is effectively a constant function.

So, for a version of the argument appropriate to the lambda calculus, we need more structure:

• Suppose we have a quotation $\newcommand{\Q}{\mathsf{Q}} \Q : \Tm_{\cal A} → \cal A$ that represents terms over $\cal A$ as elements of $\cal A$. This can be any function subject to the requirements below. So $\Q\ a$ could give structural information about $a : \cal A$, not just structure about the term
• Suppose there is an evaluation element $\newcommand{\ev}{\mathsf{ev}} \ev : \cal A$, such that $\ev \cdot \Q(e)$ is equivalent to the interpretation of $e$. So if $e$ is well-defined with result $a$, then $\ev \cdot \Q(e) = a$, and if $e$ diverges, then $\ev \cdot \Q(e)$ diverges. How $\ev$ behaves on values not in the image of $\Q$ is unspecified and doesn't matter.
• Suppose there is an element $\newcommand{\q}{\mathsf{q}} \q : \cal A$ that implements quotation internally, in the sense that $\q \cdot \Q(e) = \Q(\Q(e))$. How $\q$ behaves on values not in the image of $\Q$ is again unspecified.

Now we can copy the logic of the halting argument for lambda calculi as the following:

• Define a halting decider $\h : \cal A$ to be such that:
  1. $\h \cdot \Q(a) \cdot \Q(b)$ is always $\true$ or $\false$ (behavior on other values is unspecified)
  2. if $\h \cdot \Q(a) \cdot \Q(b)$ is $\true$, then $a \cdot b$ is well-defined
  3. if $\h \cdot \Q(a) \cdot \Q(b)$ is $\false$ then $a \cdot b$ is undefined
• Define $δ : \cal A$ to be the representative of $λx. \ev \cdot (\h \cdot x \cdot (\q \cdot x) \cdot \Q(ω) \cdot \Q(\id))$, and consider $δ \cdot \Q(δ)$
• $δ \cdot \Q(δ)$ is equivalent to $\ev \cdot (\h \cdot \Q(δ) \cdot (\q \cdot \Q(δ)) \cdot \Q(ω) \cdot \Q(\id))$
  1. If $\h \cdot \Q(δ) \cdot \Q(\Q(δ))$ is $\true$, then the above expression is equivalent to $\ev \cdot \Q(ω)$ which is undefined (remember, $\q \cdot \Q(δ) = \Q(\Q(δ))$). This contradicts the second portion of the halting decider specification.
  2. If $\h \cdot \Q(δ) \cdot \Q(\Q(δ))$ is $\false$, then the expression is instead equivalent to $\ev \cdot \Q(\id)$ which is defined with value $\id$. This contradicts the third portion of the halting decider specification.
• Again, the first portion of the halting decider specification requires that one of these two cases holds. So, it just cannot be the case that $\h$ is a halting decider.

When instantiated appropriately, this is the interesting version of the halting problem for lambda terms. It's possible to encode the lambda term data structure in the lambda calculus so that the terms can be decomposed and analyzed (I've written an Agda formalization of this here), and it meets the specification for quotation above. Then the abstract argument above instantiates to a refutation of a non-trivial notion of halting deciders in lambda calculi.

The Turing machine PCA is based on encoding already. So it can easily meet the quotation specification above by something like representing every machine (code) by itself, and evaluation being the identity (or possibly something a little more complicated, but not much). Real programming languages can use strings or data structures and an interpreter for representing themselves and evaluation. General recursive functions in arithmetic should be similar to Turing machines.

I'm not certain what you get by choosing something like a domain model or similar. In general there are examples that do not satisfy the premises above. For instance, there are PCAs where application is always well defined, so there is no notion of 'not-halting' in the first place (at least, within the above specifications). There might also be PCAs where the quotation specification doesn't make sense, and I'm uncertain if there is a more general argument for those. I don't think it's the case that every abstract 'computational system' has a well-defined self-undecidable halting problem. But, the above should cover a lot of the foundational ones typically considered.

Answer 2

Dan Doel's answer seems a lot more complicated than I would expect one to need, since very little "unfolding" is actually required. You just need to understand the structure of the proof of the Halting Problem!

Implicitly in your set-up you have an encoding procedure that presents programs as data that can be handled by programs in the same language, which is the crucial ingredient in the Halting Problem (and yet the precise details are unimportant!). I'll denote that encoding by $\#$ (and I'll leave the decoding function, aka compiler, implicit). The proof of the failure of the Halting Problem proceeds as follows:

• Suppose that program $P$ solves the halting problem, so $P(\#T) == 1$ if program $T$ halts on no inputs and $P(\#T) == 0$ otherwise.
• Construct a program $Q$ on Data as "$Q(\#T)$ := {if $P(\#(T(\#T)))$ then [loop forever] else return 1}". Note that $T(\#T)$ is the program obtained from $T$ by taking $\#T$ as an input, and we are putting the encoding of that program into $P$. This could very well be a nonsense program if $T$ doesn't accept a first argument of type Data, but that's fine: $P(\#(T(\#T))$ must evaluate to $0$ in that case.
• By construction, $P(\#(Q(\#Q)))$ cannot take the correct value, since if $P(\#(Q(\#Q))) == 1$ (halts) then $Q(\#Q)$ loops forever, and otherwise $Q(\#Q)$ halts. That's a contradiction.

Note that this is (perhaps surprisingly, since I phrased it in terms of a "contradiction") a constructive proof: if we instead take $Q$ to have two arguments, $\#P$ and $\#T$, then $Q$ is a witness of the failure of every program to solve the halting problem. So classical vs constructive logic makes no difference here.

---

To parametrize this proof with respect to the choice of data, we need to include the encoding function and the compiler in the parametrization in addition to the set of data and the evaluation operation. The compiler assigns semantics to formal syntax; the encoding function specifies how the data is interpreted as data by the chosen semantics. For your Python example, the compiler depends on the choice of version of Python. For your Gödel example, the choice of compiler and encoding function is determined by your Gödel numbering. For your Tagged Data example, the compiler will simply ignore the tag (although it's up to you whether the tag gets ignored by the encoding function). Beware that you also need a function on programs formalizing the pseudocode in the construction of $Q$ (most complicated in the Gödel example). That's all: with those ingredients, you can run the above proof.

Regarding your other questions: you could constrain the compiler to compile into a particular language if you wanted (for the "lifting" strategy) but that's not really necessary. The proof doesn't depend on the data set being countably infinite; this works for hypothetical models of computation which can interpret uncountably many programs (such as models allowing infinite programs).