On: Show HN: ScrapScript – A tiny functional language ...

[amelius]

As far as I know, nobody ever proved that some programs for which halting cannot be determined are smaller in size than the number of atoms in the universe. Or in other words, that the theorem applies to practical programs. It's purely theoretical.

[xigoi → amelius]

Here is a Python program which is definitely smaller than the number of atoms in the universe. Can you tell me whether it halts?

  n = 1
  while sum(d for d in range(1,n) if n % d == 0) != n:
      n += 2

[scythmic_waves → xigoi]

Oh this is a good one. It halts if there’s an odd perfect number, right?

[xigoi → scythmic_waves]

Yup.

[amelius → xigoi]

If I can't then that's no proof that the halting theorem is true for practical programs.

[xigoi → amelius]

If it's so hard even for such a simple program to determine whether it halts, why do you expect it to not be a problem for much more complex programs?

[amelius → xigoi]

It absolutely is a problem. But don't say that there is no solution to it unless you have a proof.

I'd be impressed if you gave me a program for which it provably cannot be proved that (edit: if) it halts. Or a bound on its size.

[xigoi → amelius]

> I'd be impressed if you gave me a program for which it provably cannot be proved that it halts. Or a bound on its size.

For every program that halts, it's obviously possible to prove that it halts. The point is that there is no algorithm for deciding if an arbitrary given program halts.

[amelius → xigoi]

> there is no algorithm for deciding if an arbitrary given program halts.

But can you prove that statement if I change it into:

there is no algorithm for deciding if an arbitrary given program with size less than N halts; for some suitable definition of size.

[xigoi → amelius]

Since we're considering practicality, let's change the statement to: “There is no algorithm for deciding if an arbitrary given program with size less than 1000 bytes halts which can be implemented without solving several famous open mathematical problems”. I think my program pretty clearly shows that this is true.

[dragonwriter → xigoi]

[never mind, misread the conditiom]

[xigoi → dragonwriter]

Why? This gives sum([]) != 1, which is true. Have you actually tried running the program?