(特殊情况下)函数重载是 NP-complete 的
前几天在逛 论坛 的时候看到这么一句话:
Overloading in combination with Hindley-Milner is NP-complete.
后面的 Hinley-Milner 我不太懂,只知道是 Haskell 用的东西。但是前面这个 overloading 我还是知道是啥的。于是我就一时兴起,找到了这么一篇 文章,就证明在某种情况下,overloading 是 NP-complete 的。看起来这是 Programming Language (PL)领域的一个基础题:
In the 1986 version of the Dragon book, Exercise 6.25 is to show that overloading is NPcomplete: **6.25 The resolution of overloading becomes more difficult if identifier declarations are optional. More precisely, suppose that declarations can be used to overload identifiers representing function symbols, but that all occurrences of an undeclared identifier have the same type. Show that the problem of determining if an expression in this language has a valid type is NP-complete.
然而,作为一个完全没接触过 PL 的小白,我连里面的 notation 都看不懂,后来在 Understanding typing judgments 这篇文章的帮助下终于理解了之前的那篇文章在干些啥。这里就把它翻译成白话顺便魔改了一下证明,不需要 PL 预备知识也能看懂。