# The Hindley-Milner type system plus polymorphic recursion is undecidable or semidecidable?

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?

• Polymorphic recursion is semi-decidable, as is, say the halting problem for a program on given input. There exist algorithms which perform excellently on this problem in practice (I think it is allowed in Haskell). The rule of thumb is: every problem that involves proof-search/type-search is semi-decidable. – cody Sep 30 '14 at 22:23

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.

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.

• I post this just to avoid having the answer in a comment. – Bakuriu May 16 '15 at 9:32
• This is incorrect. Undecidable does not mean semidecidable. Indeed, the classes of undecidable languages and semidecidable languages are imcomparable: there are semidecidable langauges that are not undecidable, and there are undecidable languages that are not semidecidable. – David Richerby Mar 27 '16 at 0:38
• @DavidRicherby You failed to read the question & answer probably. I perfectly well known that's the case however in many articles, as the one pointed out in the question, the two terms are indeed interchanged. So if the question is (as is the case) "do people tend to mix up these terms?" The answer is yes, people tend to mix them up and be inaccurate when writing about this, as is the case for the specific article in the question. – Bakuriu Mar 27 '16 at 8:54
• Bakiru: No, the terms should not be mixed, and it is not common practice to confuse them. I don't see the terms mixed in the paper (version downloaded from di.unito.it/~damiani/papers/sas2008.pdf). A claim that a set is undecidable is a lower bound (usually proved via reduction to halting), while a claim that a set is semi-decidable is an upper bound (proved via an algorithm that enumerates). When the authors use "undecidable" in theorem 5, they mean it. – sdcvvc Mar 27 '16 at 9:52
• @Bakuriu No, sorry. I read the question and your answer just fine. Your answer is wrong. The set in question is both undecidable and semidecidable. The paper authors write "undecidable" because that is the relevant point in that context: there is no algorithm that decides the set. Perhaps what you mean is that it's standard in the field to describe sets that are semi-decidable but undecidable as just being undecidable. But that's not the same thing as using the word "undecidable" to mean "semidecidable". – David Richerby Mar 27 '16 at 16:25