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?
Asked By : Bakuriu
Answered By : Bakuriu
Yes, I was right. People in the field use the term undecidable to mean semidecidable. In fact, it seems like this is done in most fields.
Best Answer from StackOverflow
Question Source : http://cs.stackexchange.com/questions/30330
0 comments:
Post a Comment
Let us know your responses and feedback