実現可能性解釈

ウィキペディア小見出し辞書

実現可能性解釈

出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2021/06/07 20:51 UTC 版)

「カリー＝ハワード同型対応」の記事における「実現可能性解釈」の解説

スティーヴン・コール・クリーネの実現可能性解釈は、直観主義的算術の証明を再帰的関数とその関数が論理式を実現していることを表す論理式の証明とに分離する。これにより、例えば「任意の自然数 a と b に対して、a と b を割り切る最大の自然数 c が存在する」ことを直観主義的に証明できたならば、ここから最大公約数を計算する再帰的関数と、それが最大公約数を計算していることの証明を抽出できる。 ゲオルク・クライゼルにより変更された実現可能性解釈を高階の直観主義論理に適用することで、もとの論理式の証明からそれを実現する単純型付けされたラムダ項を帰納的に抽出できることが示せる。命題論理の場合、これはカリー＝ハワード対応のステートメントと一致する：抽出されたラムダ項はもとの証明（をラムダ項と見做したもの）と一致し、実現可能性のステートメントは抽出されたラムダ項がもとの論理式の意味する型を持つということの言い換えである。 クルト・ゲーデルのディアレクティカ解釈は計算可能汎関数を備えた直観主義的算術（のある拡張）を実現する。これのラムダ計算との繋がりは自然演繹ほど明白ではない。