計算機科学との関係

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

計算機科学との関係

出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2022/08/08 05:41 UTC 版)

「数理論理学」の記事における「計算機科学との関係」の解説

計算機科学における計算可能性理論の研究は数理論理学における計算可能性の研究と密接に関係している。ただしその重視されている点に違いがある。計算機科学者はしばしば具体的なプログラミング言語と実際的計算可能性に焦点を当てるが、数理論理学における研究者達は理論的な概念としての計算可能性と計算不可能性に焦点を当てる。 プログラミング言語の意味論の理論はプログラム検証（とくにモデル検査）などモデル理論に関係する。証明とプログラムの間のカリー・ハワード対応は証明論のとくに直観主義論理に関係する。ラムダ計算やコンビネータ論理のような形式計算は理想化されたプログラミング言語として研究される。 計算機科学はまた自動定理証明や論理プログラミングのような自動検証や証明探索の技術の開発によって数学に寄与している。 記述計算量理論は論理と計算量を関係づける。この領域での最初の重要な結果であるフェイギンの定理（1974）はNPがexistencialな二階述語論理の論理式で表現可能な言語の成す集合とちょうど一致することを示す。