.

型推論器 f : プログラム X -> 型 T

ゲーデルの不完全性定理とは、fが全射でないということ。

つまり、全てのプログラムxに対して$ f(x) \neq t $であるような、型tが存在するということ。

でいいんかな？