patternMinor
The Hindley-Milner type system plus polymorphic recursion is undecidable or semidecidable?
Viewed 0 times
thepolymorphicundecidablerecursionhindleysystemsemidecidabletypeplusmilner
Problem
I have often read that Hindley-Milner extended to allow polymorphic recursion is undecidable. However is the term used what is actually meant? Or do people actually mean semidecidable when they mention that?
I ask this before I've recently found a paper where such a type system is presented and an algorithm based on the search of a fixed-point allows type inference for the type system. The trick is that you can fix a number $k$ of iterations for the search to maintain decidability of such a type system. If you cannot find a fixed point you can use the usual ML rules to try to type the program disallowing polymorphic recursion.
The authors proved that, given a well-typed expression $s$ there exist $k \in \mathbb{N}$ such that you can type the expression with the correct type limiting the number of iterations to $k$.
Now, I think this implies semidecidability of type inference with polymorphic recursion in such a case. If we allow $k = +\infty$ what would happen is that the algorithm would always terminate for well-typed expression, but could not terminate for non-well typed expressions.
Am I correct in this conclusion or is there some hidden issue I didn't understand?
I ask this before I've recently found a paper where such a type system is presented and an algorithm based on the search of a fixed-point allows type inference for the type system. The trick is that you can fix a number $k$ of iterations for the search to maintain decidability of such a type system. If you cannot find a fixed point you can use the usual ML rules to try to type the program disallowing polymorphic recursion.
The authors proved that, given a well-typed expression $s$ there exist $k \in \mathbb{N}$ such that you can type the expression with the correct type limiting the number of iterations to $k$.
Now, I think this implies semidecidability of type inference with polymorphic recursion in such a case. If we allow $k = +\infty$ what would happen is that the algorithm would always terminate for well-typed expression, but could not terminate for non-well typed expressions.
Am I correct in this conclusion or is there some hidden issue I didn't understand?
Solution
The answer you gave is right, but I'd like to stress the relationship between the two terms.
A formal language is decidable if and only if there exists an algorithm which correctly accepts or rejects every input in finite time. We also say it's computable.
A formal language is undecidable if and only if it is not decidable.
A formal language is semidecidable if and only if an algorithm exists that recognizing an input that is in the language. In particular, all decidable languages are semidecidable! However the halting problem is an example of a semidecidable language that is also undecidable. The complement of the halting problem is not even semidecidable.
We say type inference is undecidable rather than semidecidable (even though both characterizations are true) because the former is usually more relevant.
A formal language is decidable if and only if there exists an algorithm which correctly accepts or rejects every input in finite time. We also say it's computable.
A formal language is undecidable if and only if it is not decidable.
A formal language is semidecidable if and only if an algorithm exists that recognizing an input that is in the language. In particular, all decidable languages are semidecidable! However the halting problem is an example of a semidecidable language that is also undecidable. The complement of the halting problem is not even semidecidable.
We say type inference is undecidable rather than semidecidable (even though both characterizations are true) because the former is usually more relevant.
Context
StackExchange Computer Science Q#30330, answer score: 5
Revisions (0)
No revisions yet.