（特殊情况下）函数重载是 NP-complete 的

Posted on In Disqus: Word count in article: 681 Reading time ≈ 2 mins.

前几天在逛 论坛 的时候看到这么一句话：

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 预备知识也能看懂。

简单来说，如果我们允许一个变量的类型在声明时不确定的话（但是后续用到的类型均为同一个），那么函数重载就是 NP-complete 的。我们就用 C++ 的语法举个例子吧：（以下并不是一段合法的 C++ 代码）

1
2
3
4
int f();
float f();

auto x = f();  // what's the type of x?

这里的 f 有两个 signature，返回值可以是 int 也可以是 float。C++ 不允许这样的返回值重载。接下来我们要构造一个函数，并且证明判断其是否有合法的类型这件事是 NPC 的。

我们声明两个类型 F 和 T，以及两个辅助函数 Or 和 Not。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
struct T {};
struct F {};

T Or(T, T, T);
T Or(T, T, F);
T Or(T, F, T);
T Or(T, F, F);
T Or(F, F, T);
T Or(F, T, F);
T Or(F, F, T);
F Or(F, F, F);

F Not(T x);
T Not(F x);

我们考虑把 3-SAT 归约成 overloading。举个例子，对于一个 3-SAT 实例：想要判断是否存在一组 \((x_1, \dots, x_4) \in \{true, false\}^4\) 满足 \[ (x_1, x_2, \neg x_3) \wedge (\neg x_2, x_3, x_4) \wedge (x_1, x_3, \neg x_4), \] 我们就可以写出如下代码：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
T init();
F init();

auto x1 = init(); auto y1 = Not(x1);
auto x2 = init(); auto y2 = Not(x2); 
auto x3 = init(); auto y3 = Not(x3); 
auto x4 = init(); auto y4 = Not(x4);

int g(T, T, T);

int ret = g(
    Or(x1, x2, y3),
    Or(y2, x3, x4),
    Or(x1, x3, y4),
);

如果我们能通过为 \(x\) 决定类型来重载 \(g\)，那么就意味着我们找到了原 3-SAT 问题的一组解。于是就规约过去了……

所以这个证明的难点在于如何看懂 notation 吧……