プログラミング言語と論理学の両立
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2021/09/29 03:08 UTC 版)
「依存型」の記事における「プログラミング言語と論理学の両立」の解説
カリー＝ハワード同型対応により、どんなに複雑な数学的な性質も型によって表現できる。もしユーザーが、型が非空である (つまり、その型を持つ値が存在する) ことの構成的な証明を与えることができれば、コンパイラは証明の正当性を検査し、証明の構成を追うことにより、実際にその値を計算できる実行可能なプログラムコードを出力することができる。このように証明を検査できるという性質により、依存型を持つプログラミング言語は定理証明支援系と近い関係にある。コードを生成できるという視点からは、機械的に検証された数学の証明からプログラムコードを直接導出することができるため、形式手法によるプログラム検証や証明つきコード（英語版）へのアプローチが考えられる。
※この「プログラミング言語と論理学の両立」の解説は、「依存型」の解説の一部です。
「プログラミング言語と論理学の両立」を含む「依存型」の記事については、「依存型」の概要を参照ください。
ウィキペディア小見出し辞書の「プログラミング言語と論理学の両立」の項目はプログラムで機械的に意味や本文を生成しているため、不適切な項目が含まれていることもあります。ご了承くださいませ。
お問い合わせ。
- プログラミング言語と論理学の両立のページへのリンク
