Agda 入門証明支援系の言語である Agda の入門を目的としています 具体的には Agda による証明の方法を知る 実際に自然数に対する演算の証明を追う ことをしていきます 証明支援系と呼ばれる分野の言語です 他には Coq などがあります Haskell で実装されています 型が非常に強力で表現力が高いです 命題や仕様を表す論理式を型として定義することができます 例えば 1 + 1 = 2 とか Agda における証明は 証明したい命題 == 関数の型 命題の証明 == 関数の定義 として定義します 関数と命題の対応を Curry-Howard Isomorphism と言います どうしてプログラムで証明できるかというと (命題 と 定義) は (仕様 と 実装) のように対応します int chars_to_int(char * chars) つまり char * から int は作れる、という
