[mistercow]

>You assume the human mind is only as powerful as a Turing machine, which is just conjecture.

Given the lack of any proposals for how, even in theory, hypercomputation might be achieved in a physical system, and the lack of any empirical indication that humans are capable of hypercomputation, I would say it's much more than a conjecture. At the very least, it's an incredibly likely conjecture.

> For example, what does this program do when given input another_program?

It prints "program halts." if another_program halts, and prints "program does not halt." otherwise. I understand exactly what this program does, even though I can't tell you its output for an arbitrary input. And if I want to translate the above sentence into Spanish, I don't have to come anywhere near solving the halting problem to do so.

Consider the following program which does not involve the halting problem:

    function (targetDigest)
      i = new BigInt(0);
      while(true) {
        if (sha1(i.toBytes()) == targetDigest) {
          print(i.toBinary());
        }
        i = i.plus(1);
      }
    }

What does this program do when given targetDigest? It prints out the shortest bit string whose SHA-1 is that targetDigest. I obviously can't tell you what specific answer it will output for a given input, but it would be absurd to say that I don't understand the program.

But even if you can come up with sentences that require one to solve the halting problem to translate (and I'm still not convinced such sentences exist), it's another thing entirely to claim that those sentences come up in practice. This is a red herring when it comes to the feasibility of machine translation, because a good translator doesn't need to be able to cope with every valid sentence. It merely needs to cope with the set of sentences that humans actually care about.

[yters]

My point was given a specific another_program you cannot say exactly what the program will do. On the other hand, every program is some kind of Turing computation, so you could argue by knowing of a Turing machine you understand every program. However, that is not so useful.

If we knew everything that comes up in practice, translation and natural language processing would be a solved problem. Without this knowledge, then we need to look at the general picture, which is not solvable. So there is no automated way to understand all language, we have to always rely on a human in the loop to provide domain knowledge.

[mistercow]

No, again, you’re conflating comprehension and execution. It is very clear that you don’t have to execute a set of instructions in order to translate them into another language.

So unless you can give a specific example of a sentence that requires one to solve the halting problem to translate, I don’t think you’re saying anything hint meaningful. And if you can come up with such an example which people would actually use in practice, I’ll eat my hat.

[yters]

Yes, strict translation requires solving the halting problem in the general case. E.g. translate this dynamically typed program into a statically typed one:

  if halts(input): return 1
  else: return "Nope"

However, you can always write an interpreter in your desired language and avoid the halting problem. But, that's not really translation.

[mistercow]

Can you explain to me what you think “translate this dynamically typed program into a statically typed one” means as concerns your fragment of pseudocode? And are you assuming that the “halts” function is a halting oracle?

[yters]

It'd be better expressed as:

  def a_func(input):
      if eval(input) == 0: 
          return 1
      else: 
          return "Nope"

To convert this to a statically typed program, the compiler has to determine what eval(input) returns at compile time, so it knows whether the function has a type signature of int or String.

In general, this is impossible, since eval(input) may not halt.

[mistercow]

The way to type this would be: String -> Int | String (or, if the bottom type is part of your type system, String -> Int | String | Bottom)

And assuming that "eval" is typed as String -> Any, there should be no problem automatically inferring the type signature of this function. I certainly didn't have to solve the halting problem to generate that signature.