<p>This isn't a "nice" property, because whether it's true or false depends upon the encoding.</p>

<p>See David et al's <a href="https://arxiv.org/abs/0903.5505" rel="nofollow noreferrer"><em>Asymptotically almost all $\lambda$-terms are strongly normalizing</em></a>, 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). </p>

<p>In the lambda calculus, a <em>reduction</em> 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. </p>

<p>However, lambda-terms can be translated in a meaning-preserving way into a combinatory calculus such as the <a href="https://en.wikipedia.org/wiki/SKI_combinator_calculus" rel="nofollow noreferrer"><em>SKI combinators</em></a> (and vice-versa), and in combinator calculi asymptotically all terms loop. </p>

CC BY-SA 4.0
2018-05-15T04:55:21.093Z
I observe that a future visitor, not necessarily knowing the relationship between strong normalization and halting detection, may not be able to determine what position (if any) your answer takes.
Eric Towers
CC BY-SA 4.0
2018-05-15T10:36:56.780Z
@EricTowers Done!
Neel Krishnaswami
CC BY-SA 4.0
2018-05-14T16:38:18.263Z
2018-05-15T10:36:42.797Z
2018-05-15T10:36:42.797Z
Neel Krishnaswami
<p>Is there a Turing Machine that can decide whether <em>almost all</em> other Turing Machines halt?</p>

<p>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:</p>

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

<p>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$? </p>

CC BY-SA 4.0
2018-05-14T16:01:51.947Z
https://projecteuclid.org/euclid.ndjfl/1168352664
Emil Jeřábek
<turing-machines><halting-problem>
How good can a halting detector be?
Acccumulation
# How good can a halting detector be?

(Asked by: username_0 on 2018-05-14)

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$?

**Tags:** turing-machines, halting-problem
> **Comments:**
> **username_1**: https://projecteuclid.org/euclid.ndjfl/1168352664  

---

## 1 answers

### Answer by username_2 on 2018-05-14. Score: 10 | Accepted answer

This isn't a "nice" property, because whether it's true or false depends upon the encoding.

See David et al's [*Asymptotically almost all $\lambda$-terms are strongly normalizing*](https://arxiv.org/abs/0903.5505), 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.

However, lambda-terms can be translated in a meaning-preserving way into a combinatory calculus such as the [*SKI combinators*](https://en.wikipedia.org/wiki/SKI_combinator_calculus) (and vice-versa), and in combinator calculi asymptotically all terms loop.

> **Comments:**
> **username_3**: I observe that a future visitor, not necessarily knowing the relationship between strong normalization and halting detection, may not be able to determine what position (if any) your answer takes.  
> **username_2**: @EricTowers Done!  

---

