1
$\begingroup$

When downloading a file from the internet to our computer we are usually prompted with an estimate of how long it will take for the file to be downloaded.

From the Halting Problem, we know that $\mathrm{HALT}_{\mathrm{TM}}$ is undecidable, where:

$\mathrm{HALT}_{\mathrm{TM}} =\{⟨M,w⟩\mid M \text{ is a TM and }M\text{ halts on input }w \} $

Assuming that we can neglect the lack of infinite memory, we can model our computer writing on the disk as a Turing Machine $M$ and take the string encoding of the downloaded file as the input $w$. (More precisely, $w$ should be the string obtained composing the packets sent by the network)

From the Halting Problem it follows that it's not only impossible to know when the download will end, it's even impossible to know whether the download will ever end.

So, are files download times actually unknowable due to the halting problem? If not, where the above reasoning fails?

Improve this question
$\endgroup$
3
  • 2
    $\begingroup$ Using this reasoning, you can show that any problem (e.g. $a+b$) is undecidable. $\endgroup$
    – user114966
    Jul 31, 2020 at 21:43
  • $\begingroup$ Yes, the TM can be arbitrary, so it may work on computing a+b, where a and b are in w. Can you point out where the above reasoning fails? $\endgroup$
    – Rexcirus
    Jul 31, 2020 at 22:27
  • $\begingroup$ I think the answers below explain the issue pretty good. The language $HALT_{TM} = \{\langle M, w\rangle| \ldots \}$ is undecidable. However, language $HALT_{Download} = \{ \langle Download_{TM}, w \rangle | \text{$Download_{TM}$ halts on $M$}\}$ is not: it's just a different language. More specifically, it's a subset of $HALT_{TM}$. As an extreme example, $\emptyset \subseteq HALT_{TM}$, but $\emptyset$ is decidable. $\endgroup$
    – user114966
    Jul 31, 2020 at 23:01

3 Answers 3

Reset to default
4
$\begingroup$

Not at all.

The halting problem says it is impossible to decide whether an arbitrary turing machine with arbitrary input will halt. But there are many, many specific turing machines where we can prove that they halt for every input, or where we can look at the input and decide if the turing machine will halt or not.

And since the people writing the download code surely wrote it in such a way that it is guaranteed to finish for every import, there will be a proof that it is guaranteed to finish.

Improve this answer
$\endgroup$
1
  • $\begingroup$ I'm not sure if the last two lines are actually true, but the answer solved my main confusion on the use of the halting problem. $\endgroup$
    – Rexcirus
    Aug 1, 2020 at 0:13
2
$\begingroup$

The main issue, I think, is that you have reduced your unknown problem (file download times) to a hard problem (the Halting Problem), showing that if you had some efficient algorithm for solving the hard problem, then the unknown problem would also be efficiently solvable. To prove hardness of the unknown problem, you need a reduction that goes the other way, by showing that efficiently solving the unknown problem would allow you efficiently solve the hard problem.

(A secondary issue is that I don't really see any way to express the "file download time" problem purely in terms of abstract Turing machines, since the problem itself seems so essentially tied to the physical world.)

Improve this answer
$\endgroup$
2
$\begingroup$

Solving the "download time problem" is just impossible. Nothing says if your machine (or the network, or the origin, or...) will (or won't) crash, or get overloaded (perhaps everybody in India wakes up with the urge to get the same file, and crash the server) or slow to a crawl, or just speed up to a breeze, halfway through.

The problem here is that the actual time depends on a myriard of variables, many of them unknown (and unknowable), due to the immense complexity of the Internet and it millions of users (and lots of other external factors that can impact it's functioning).

The halting problem for Turing machines is quite different, there the pieces and their relationship is clear, simple and well-defined. By design, really: Turing was looking for a transparent model of what it means for a human to "compute" something, and distilled it down to a extremely minimal, simple one.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.