logic - 系统的健全性和完整性

Question

首先介绍一些术语(取自here，第14页):
正程序是有错误的程序。
否定程序是没有错误的程序。
因此，程序有四种类型:
积极计划，分析为积极->真正积极(TP)。
积极计划，分析为否定->假否定(FN)。
否定程序，分析为肯定->假肯定(FP)。
否定程序，分析为否定->真否定(TN)。
如果系统从不接受肯定的程序，则它为声音。
如果系统从不拒绝否定程序，则它是完整。

因此，从我上面写的内容来看:

A complete system accepts FN and TN programs.
A sound system also accepts FN and TN programs.

一位同事告诉我，声音系统也接受FP程序。有人可以确认这一点并解释为什么这样做吗？

Answer 1

这本书是这样解释的:

Soundness prevents false negatives and completeness prevents false positives.

因此，为了使系统健全，它不需要防止误报，而只需防止误报。为防止误报，它必须完整。

该书以类型系统为例进一步解释了它:

In modern languages, type systems are sound (they prevent what they claim to) but not complete (they reject programs they need not reject). Soundness is important because it lets language users and language implementers rely on X never happening. Completeness would be nice, but hopefully it is rare in practice that a program is rejected unnecessarily and in those cases, hopefully it is easy for the programmer to modify the program such that it type-checks.

Type systems are not complete because for almost anything you might like to check statically, it is impossible to implement a static checker that given any program in your language (a) always terminates, (b) is sound, and (c) is complete. Since we have to give up one, (c) seems like the best option (programmers do not like compilers that may not terminate).