計算可能性論理とは、計算可能性のある側面を基本概念として捉えた論理の定式化です。これは通常、特殊な論理接続詞と、論理が計算的にどのように解釈されるかを説明する意味論の組み合わせを伴います。
計算可能性論理の最初の形式的解釈は、おそらく1945年にスティーブン・クリーネが行った実現可能性解釈であろう。彼は直観主義的数論をチューリングマシン計算の観点から解釈した。彼の動機は、数学的命題の証明を構成的手続きとみなすという直観主義のハイティング＝ブラウワー＝コルモゴロフ（BHK）解釈を明確にすることであった。
様相論理や線形論理といった他の多くの種類の論理、そしてゲーム意味論といった新しい意味モデルの台頭に伴い、計算可能性に関する論理は様々な文脈で定式化されてきました。ここではそのうちの2つについて述べます。
計算可能性のための様相論理
クリーネの元々の実現可能性解釈は、計算可能性と論理の関係を研究する研究者の間で大きな注目を集めてきました。 1982年、マーティン・ハイランドはこれを完全高階 直観主義論理へと拡張し、実効トポスを構築しました。2002年には、スティーブ・アウォディ、ラース・ビルケダル、ダナ・スコットが計算可能性のための様相論理を定式化しました。これは、通常の実現可能性解釈を拡張し、「計算可能真」という概念を表現する2つの様相演算子を導入したものです。
ジャパリゼの計算可能性論理
計算可能性論理とは、2003年にギオルギ・ジャパリゼが開始した研究プログラムを指す。その目的は、ゲーム理論的意味論から論理を再発展させることである。このような意味論では、ゲームを対話型計算問題の形式的等価物とみなし、その「真理」をアルゴリズム的な勝利戦略の存在とみなす。
参照
参考文献
- SCクリーネ「直観主義的数論の解釈について」『記号論理学ジャーナル』 10:109-124, 1945年。
- JMEハイランド著『効果的なトポス』ASトロエルストラ、D.ファン・ダーレン編『LEJブラウワー生誕100周年記念シンポジウム』165-216ページ。ノースホランド出版社、1982年。
- S. Awodey, L. Birkedal, D.S. Scott.局所実現可能性トポスと計算可能性のための様相論理. コンピュータサイエンスにおける数学的構造, 12(3):319-334, 2002.
- G. Japaridze,計算可能性論理入門. Annals of Pure and Applied Logic 123 (2003), 1-99ページ.
外部リンク
- CMU における型と計算の論理
- 計算可能性論理ホームページ
- ギオルギ・ジャパリゼ
- ゲームセマンティクスか線形ロジックか?
