正确性

Correctness: Soundness, Completeness, Undecidability.

设我们想要避免的错误为 X，我们定义一个 static checker 的正确性 (correctness) 为：

• A type system is sound if it never accepts a program that, when run with some input, does X, i.e., soundness prevents false negatives.
• A type system is complete if it never rejects a program that, no matter what input it is run with, will not do X, i.e., completeness prevents false positives.

实际上，soundness 与 completeness 这两个术语来自逻辑学，其被广泛的应用在编程语言的理论设计中。

• A sound logic proves only true things.
• A complete logic proves all true things.

如果一个 type system 能够兼具 soundness 与 completeness，那么它所接受的程序集合与所有不执行 X 的程序集合是完全等价的。可惜，理论是美好的，现实是残酷的：

以 ML 的 static checker 为例，若我们想避免的问题 X 为 “string 类型的值作为除法运算的运算数”：

1
2
3

fun f1 x = 4 div "hi"                         (* f1 never get called *)
fun f2 x = if true then 0 else 4 div "hi"
fun f3 = if x <= abs x then 0 else 4 div "hi"

注意，上述的三个函数均不会执行 4 div "hi" 这一语句，但 ML 的 static checker 却会检出类型错误并拒绝程序运行。这也就是说，ML 并不能很好的处理假阳性程序，它的 static checker 并不是 complete 的。

为了确保 X 不出现，现代语言的设计者选择了 soundness 与 always terminates 而牺牲了 completeness。接受假阴性程序的后果要远大于拒绝假阳性程序的后果。

与停机问题 (halting problem) 类似，一个总能停机的 static checker 不能兼具 soundness 与 completeness 的原因也是由图灵机的不可决定性 (undecidability) 决定的。

非正式的设想一下，若我们想避免的问题 X 为程序进入死循环，那么一个既 sound 又 complete 的 static checker 本身就是对停机问题的通用解法。这样，我们把该问题的不可能性归约到了停机问题的不可能性上。