# Halting Problem, Typed Version: A Headache

After many years, I have been revisiting the venerable old Halting Problem and the self-referential / diagonalization “party trick” that shows that there is no Turing Machine able to solve it.

I was bothered by the fact that it was, and continues to be, stated in an untyped manner, and thus is a bit sloppy for my tastes.

Let's call HALTP be the (actually, "an") always-halting Turing Machine (TM) which can decide whether a pair [Turing Machine, Input] is a combination that halts (the P is coming from the P convention.)

Once typing is considered when one feeds the representation of HALTP (actualy, the representation of a slightly modified version of HALTP) to the HALTP Turing machine itself, things fall a bit apart.

# Preliminaries

(Actually you can just go directly to "typing" as everything here is rather unsurprising)

• All the TMs that we are talking about are ‘a-machines’, as opposed to the (more interesting) ‘o-machines’ which have access to “Oracle Tapes”. They are implementations of functions taking input, running to completion (or not) and yielding output.
• There is an Universal TM called UTM_L, able to simulate any other TM, if that TM has been expressed as some finite string of symbols chosen from a finite alphabet $$L$$ (which is assumed to be possible).
• A string from $$L^*$$ representing the Turing Machine with the name MYTM is written <MYTM>, and thus the "code" of MYTM.
• Not every string from $$L^*$$ represents an actual TM (some strings have no meaning and cannot be run by UTM_L). We mark the subset of valid TMs as $$L^*_{valid} \subset L^*$$ (I state w/o proof that $$L^*_{valid}$$ this is a decidable language).
• We assume that all the TM are run by UTM_L, which also is a multitape machine with disjoint symbol sets for each tape. The following tapes are assumed to exist:
• ✇I = Input Tape containing elements from a language $$TREE$$ (see below).
• ✇P = Program Tape containing a <TM> from a $$L^*_{valid}$$ to be emulated.
• ✇W = Work Tape (not further examined)
• ✇O = Output Tape containing strings from the 4-element language: { ⊥, ⊤, ⚠, ∅ }. ✇O originally only contains ∅, which is replaced by one of the other three words.
• With loss of generality we only consider TMs which accept / reject elements of a given language. The functions they implement are not "constructive".
• Every TM accepts elements of a language $$TREE$$ on ✇I. $$TREE$$ is informally defined as: "The bracketed expressions build from comma-separated <TM>, strings from a language $$W*$$ built from a finite set of symbols disjoint from $$L$$, the elements of which we denote with <w> and elements from the language $$TREE$$". For example: [<TM1>, [], <w0>, [<w1>, <w2>]].
• Finally, we define:
• DECIDER TM: The TM is presented with <w> on ✇I. It always halts and replaces the ∅ sign on ✇O with:
• ✇O = ⊤ if TM accepts <w>
• ✇O = ⊥ if TM rejects <w>
• ✇O = ⚠ if there is a type error (see below)
• RECOGNIZER TM: The TM is presented with <w> on ✇I. It may or may not halt.
• ✇O = ⊤ if TM halts and accepts <w>
• ✇O = ⊥ if TM halts and rejects <w>
• ✇O = ⚠ if there is a type error 8see below)
• ✇O = ∅ if TM does not halt (a bit of a language abuse as it just means that the original ∅ symbol on ✇O will never be replaced).

# Typing

Now, we implement “typing” in as follows:

We add “type judgements” to our Turing Machine description toolset. Type judgements are not found on tapes, they are part of the specification of TMs.

We need just two type judgements:

• <tm>: TM – The word <tm> on the ✇I represents a TM from $$L^*_{valid}$$
• <x>: TREE – The word <x> on the ✇I is an element from $$TREE$$.

We assume that when a TM is run on input <w>, i.e. when we compute TM(<w>), the TM performs a type check and decides whether <w> passes all type judgements given in its definition. If <w> does not pass, the TM outputs ⚠ on the ✇O and halts.

# Define HALTP

So, we suppose that there is a TM called HALTP with obeys the following specification:

• HALTP( [<tm>: TM, <x>: TREE] ) meaning that UTM_L implementing it shall expect
• On ✇P: <HALTP>
• On ✇I: The finite word from $$TREE$$ represented by [<tm>, <x>] where <tm> and <x> fulfill the type judgements.

If the initial type check on ✇I fails, ✇O = ⚠

Otherwise, we expect flawless performance and halt-in-all cases and:

• ✇O = ⊤ if the TM given by <tm> halts and accepts <x>
• ✇O = ⊥ if the TM does not accept <x> (does not halt or rejects <x>)

# The Problem

In the diagonalization approach, we feed <HALTP> to HALTP (actually <the complement of HALTP> to HALTP, but let’s keep going). So let’s try that here:

Does HALTP halt on input x?

HALTP( [<HALTP>: TM, <x>: TREE] )

But what is <x>?

<x> must evidently be something that can be given to the TM represented by the first argument i.e. HALTP, otherwise this call is entirely meaningless.

HALTP expects and argument matching ( [<tm>: TM, <x>: TREE] )

so we need to actually call HALTP like this, as we want to call HALTP on HALTP:

Does HALTP halt on input itself on input x?

HALTP( [<HALTP>: TM, [ <HALTP>: TM, <x’>: TREE]] )

But what is <x’>?

<x> must evidently be something that can be given to the TM represented by the second argument i.e. HALTP, otherwise this call is entirely meaningless.

so we really need:

Does HALTP halt on input itself on input itself on input x?

HALTP( [<HALTP>: TM, [ <HALTP>: TM, [ <HALTP>: TM, <x’’>: TREE]]] )

The effort to build a meaningful argument to HALTP seems to fail due to an infinite regress and the question "what happens if we give HALTP to HALTP" does not make sense because giving HALTP to HALTP is nonsensical.

The textbook proof seems to absolutely ignore this problem, it assumes that calling

HALTP( <HALTP>, <HALTP> )

makes sense.

For example, the extract below is from Michael Sipser’s “Introduction to the Theory of Computation, 2nd Edition”, 2006, p. 179. In particular, it compares "running HALTP on itself" with a compiler in Pascal compiling the compiler for Pascal – but that is not the same thing at all because the argument to the compiler is meaningful without an additional argument to the compiler-to-be-compiled.

How to to fix that?

• Perhaps you'll like this proof more: cs.stackexchange.com/a/35683/683. – Yuval Filmus Feb 23 at 18:55
• I'm wondering why do you associate "being stated in an untyped manner" with "sloppy"? Many mathematical proofs are stated in an untyped manner. Perhaps understanding that better might help me understand your sense of unease/discomfort with this proof? – D.W. Feb 24 at 16:43
• The halting problem for the typed Turing machines is undecidable. It is not hard to give it a new proof or adapt the previous proof. – Apass.Jack Feb 26 at 5:13

A crucial aspect of Turing machines is that you can build a universal Turing machine. Another way to think of that is that Turing machines are expressive enough that you can construct a Turing machine that acts as an interpreter for Turing machines: if you provide it a description of a Turing machine (as bits), then it will simulate execution of that Turing machine. Another way to describe this is that Turing machines basically can implement eval. Moreover, once you can implement eval, then the halting problem becomes undecidable.
However, eval is incompatible with some static type systems: it takes as input a bit-string, and outputs a value whose type is not statically known. Many static type systems can't handle that. So, if you introduce a static type system without being sufficiently careful, then you might have (without realizing it) restricted expressivity enough that eval can no longer be implemented, an interpreter cannot be implemented, etc.