4 ms·

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

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 8y ago
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 8y ago
  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 8y ago
    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 8y ago
      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.
      - yters 8y ago
        In that case you are relying on generics or the equivalent of dynamic typing. My point is that if the language is just static typing without these extra facilities, you cannot translate without knowing the outcome at runtime.

yters 8y ago

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 8y ago
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 8y ago
  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 8y ago
    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.
    - yters 8y ago
      In that case you are relying on generics or the equivalent of dynamic typing. My point is that if the language is just static typing without these extra facilities, you cannot translate without knowing the outcome at runtime.