3 ms·

what's the connection between being undecidable and turing complete?

guerrilla 6y ago
Type checking is undecidable for type theories that are Turing-complete. Type theories are Turing complete if they can simulate a turing machine. Roughly, type chicking for a type theory is undecidable if its not decidable whether every term has the type assigned to it by the programmer. The halting problem is the connection, which the website states but the author is inviting bug reports, so maybe its a good idea to ask them to clarify it.
pcstl 6y ago
tl;dr: Every Turing Complete system is undecidable - i.e. for every Turing Complete system which answers "yes" or "no", you can't determine in finite time whether, for any given input, the program will accept it or not. Long version: Being Turing Complete means that a system can compute everything that a Turing Machine can compute. For a long time, it was an open question whether there was a way to determine whether, for a given statement, one could determine whether it was universally valid. Alan Turing's creation of the Turing Machine was originally in order to try to answer this question. The idea was that to determine if a statement was universally valid, one would need to be able to mechanically derive the statement from the axioms of logic - i.e., there would be an algorithm (which Turing formalized as a "Turing Machine") that would be able to take the input and decide whether it was universally valid. Turing then proved - likely his greatest claim to fame - that such an algorithm could not exist - as one can always build an input for which it will be forced to give the wrong answer. Hence, Turing showed that for any Turing Machine - or any system equivalent to a Turing Machine - which answers "yes" or "no" to some input, it is impossible to decide whether it accepts its input in finite time.
gpm 6y ago
If your type system is turing complete, then it's undecidable. This is easily seen through rices theorem [0] which states that all non-trivial (not always true or always false) semantic properties (i.e. about what inputs it maps to what outputs) of turing complete programs are undecidable. In particular what type something is going to be is undecidable. Intuitively you should probably think of this as a slight extension of the halting problem, you can't always tell whether or not something (your type checking) halts. It's not that much of a leap to say that you can't tell whether it will halt after an even number or odd number of steps if it does halt (this doesn't immediately follow from the halting problem, but it is true). Imagine if you had a type that said "if it takes an even number of steps for some given computation to halt, I'm 'type A', if it takes an odd number I'm 'type B'". That's something a turing complete type system can do, and since you can't tell whether it will take an even or odd number of steps you can't tell whether or not the variable is 'type A' or 'type B'. If it's undecidable it's not necessarily turing complete, but it's very easy to be accidentally turing complete, so it probably is. [0] https://en.wikipedia.org/wiki/Rice%27s_theorem https://en.wikipedia.org/wiki/Rice%27s_theorem

Type checking is undecidable for type theories that are Turing-complete. Type theories are Turing complete if they can simulate a turing machine. Roughly, type chicking for a type theory is undecidable if its not decidable whether every term has the type assigned to it by the programmer. The halting problem is the connection, which the website states but the author is inviting bug reports, so maybe its a good idea to ask them to clarify it.

pcstl 6y ago

tl;dr: Every Turing Complete system is undecidable - i.e. for every Turing Complete system which answers "yes" or "no", you can't determine in finite time whether, for any given input, the program will accept it or not. Long version: Being Turing Complete means that a system can compute everything that a Turing Machine can compute. For a long time, it was an open question whether there was a way to determine whether, for a given statement, one could determine whether it was universally valid. Alan Turing's creation of the Turing Machine was originally in order to try to answer this question. The idea was that to determine if a statement was universally valid, one would need to be able to mechanically derive the statement from the axioms of logic - i.e., there would be an algorithm (which Turing formalized as a "Turing Machine") that would be able to take the input and decide whether it was universally valid. Turing then proved - likely his greatest claim to fame - that such an algorithm could not exist - as one can always build an input for which it will be forced to give the wrong answer. Hence, Turing showed that for any Turing Machine - or any system equivalent to a Turing Machine - which answers "yes" or "no" to some input, it is impossible to decide whether it accepts its input in finite time.

gpm 6y ago

If your type system is turing complete, then it's undecidable. This is easily seen through rices theorem [0] which states that all non-trivial (not always true or always false) semantic properties (i.e. about what inputs it maps to what outputs) of turing complete programs are undecidable. In particular what type something is going to be is undecidable. Intuitively you should probably think of this as a slight extension of the halting problem, you can't always tell whether or not something (your type checking) halts. It's not that much of a leap to say that you can't tell whether it will halt after an even number or odd number of steps if it does halt (this doesn't immediately follow from the halting problem, but it is true). Imagine if you had a type that said "if it takes an even number of steps for some given computation to halt, I'm 'type A', if it takes an odd number I'm 'type B'". That's something a turing complete type system can do, and since you can't tell whether it will take an even or odd number of steps you can't tell whether or not the variable is 'type A' or 'type B'. If it's undecidable it's not necessarily turing complete, but it's very easy to be accidentally turing complete, so it probably is. [0] https://en.wikipedia.org/wiki/Rice%27s_theorem https://en.wikipedia.org/wiki/Rice%27s_theorem