# How good can a halting detector be?

Is there a Turing Machine that can decide whether almost all other Turing Machines halt?

Suppose we have some enumeration $\mathbb{N} \rightarrow \{M_i\}$ of Turing machines, and some notion of "size" of a set of natural numbers $\| \cdot \|$, and we define:

$$f(i) = \|\{n: M_i \text{ can't decide whether }M_n \text{ halts} \}\|.$$

What characterizations of the minimum value of $f$ exist for different $\| \cdot \|$? For instance, suppose $\| S \|$ is the limsup of the proportion of numbers up to $k$ that are in $S$. Is there an $i$ for which $f(i) = 0$?

See David et al's Asymptotically almost all $\lambda$-terms are strongly normalizing, which proves what it says in the title. However, this paper also shows that the opposite holds for SKI-combinators (into which lambda-terms can be compositionally embedded).
In the lambda calculus, a reduction is the equivalent of a step of a Turing machine, and strong normalization is the property that every reduction sequence eventually reaches a normal form -- ie, no further reductions are possible. (Since a given lambda-term may have many valid reductions, strong normalization is a bit like saying a given nondeterministic Turing machine always halts.) So the fact that asymptotically almost all $\lambda$-terms are strongly normalizing means that with probability approaching 1, reducing a large lambda terms will always reach a normal form.