完全性
completeness
意味論的に真である命題は形式的に証明できる
論理式$ \varphi(X_1,\cdots,X_n)がトートロジーならば、証明可能である
逆に
完全な型推論を持つコンパイラは、正しいプログラムであるならば、型が推定できると保証される
と言えるのかmrsekut.icon
型理論の文脈では
型エラーがあれば、バグが絶対にある
不正な動作をしないプログラムは、型検査を通過する
健全性の逆
内容的に正しい判断は全て導出できる
成り立つ命題は証明できる
ゲンツェンの自然演繹(NK)では、完全性定理が成り立つ
参考
型安全性入門
http://web.sfc.keio.ac.jp/~hagino/logic16/05.pdf
健全性と完全性 - 発声練習
型以外の具体例あり