翻訳と辞書
Words near each other
・ カリーム・ハーン・ザンド
・ カリーム・ヴァレンタイン
・ カリーラとディムナ
・ カリーライス
・ カリール・ジブラン
・ カリール・ジブラーン
・ カリーンの剣
・ カリーヴルスト
・ カリー・ウェッブ
・ カリー・ウェブ
カリー・ハワード同型対応
・ カリー・ハワード対応
・ カリー・ペイトン
・ カリー・ボリー
・ カリー化
・ カリー郡
・ カリー郡 (オレゴン州)
・ カリー郡 (ニューメキシコ州)
・ カリー=ハワード同型
・ カリー=ハワード同型対応


Dictionary Lists
翻訳と辞書 辞書検索 [ 開発暫定版 ]
スポンサード リンク

カリー・ハワード同型対応 : ウィキペディア日本語版
カリー=ハワード同型対応[かりー=はわーどどうけいたいおう]

カリー=ハワード同型対応(カリー=ハワードどうけいたいおう、)とは、プログラミング言語理論証明論において、計算機プログラムと証明との間の直接的な対応関係のことである。「プログラム=証明」(proofs-as-programs)・「型=命題」(formulae-as-types)などとしても知られる。これはアメリカの数学者ハスケル・カリー論理学者ウィリアム・アルヴィン・ハワードにより最初に発見された形式論理の体系とある種の計算の体系との構文論的なアナロジーを一般化した概念である。通常はこの論理と計算の関連性はカリーとハワードに帰属される。しかしながら、このアイデアはブラウワーハイティングコルモゴロフらが定式化した直観主義論理の操作的解釈の一種と関係している。

==一般的な定式化==
もっと一般的な観点からいえば、カリー=ハワード対応は証明計算計算模型型システムとの間の対応である。これは2つの対応に分けられる。ひとつは、論理式のレベルであり、これは特定の証明体系や計算模型の選択に依存しない。いまひとつは、形式的証明とプログラムのレベルであり、これは証明体系や計算模型の選択に依存する。
論理式と型のレベルにおいて、この対応によれば、含意は関数型、論理積は直積型(タプル、構造体、リストなど、言語によって様々に呼ばれる)、論理和は直和型(バリアント、共用体、Eitherなど)、偽は空な型、真はシングルトン型のように振る舞うという。量化子依存直積または直和にそれぞれ対応する。
まとめると、次のような表になる:

証明体系と計算模型のレベルにおいて、この対応は主に構造的な同一性を示す。ひとつはヒルベルト流の推論体系コンビネータ論理、いまひとつはゲンツェン自然演繹ラムダ計算との間の同一性である。

自然演繹とラムダ計算との間には次のような対応関係が存在する:


抄文引用元・出典: フリー百科事典『 ウィキペディア(Wikipedia)
ウィキペディアで「カリー=ハワード同型対応」の詳細全文を読む

英語版ウィキペディアに対照対訳語「 Curry-Howard correspondence 」があります。



スポンサード リンク
翻訳と辞書 : 翻訳のためのインターネットリソース

Copyright(C) kotoba.ne.jp 1997-2016. All Rights Reserved.