|
Agda（アグダ）は定理証明器、すなわち数学的な証明を検証するコンピュータプログラムである。ペール・マルティン＝レーフの型理論の一種における構成的証明構築のための対話的システムであり、一方で依存型をもつ関数型プログラミング言語であるともみなすことができる。1990年代よりチャルマース工科大学で主に開発されている。 他の定理証明支援系ではスクリプトによって「戦略」を指定して証明を操作するのに対して、Agda では証明を項として表し直接操作するというアイデアに基づいている。言語はデータ型や case式、シグネチャやレコードといった一般的なプログラミング構成概念をもつ。Emacsインターフェイスを使って対話的にコードを作成できるほか、直接コードをコンパイルする処理系の開発も進んでいる。 == Agda == Agda は当時チャルマース工科大学で開発されていた、依存型理論を基にした証明支援系(ALF, Alfa)やプログラミング言語(Cayenne)に続いて開発された。2000年代の半ばに大幅な改良が計画され、 Agda2 として実装された(以前のバージョンを Agda1 と表記して区別する場合も多い)。Agda2は、Ulf Norellによってチャルマースで開発が続いている。インスタンス導出、文脈から推論できるときは省略できる暗黙の変数など、構文は Agda 1 から変更されている(ただし、変換ツールが開発されている)。Agda 2 はより可読性の高い証明を得るための方法として、Unicodeが広く使われている。 Agda 2 は Makoto Takeyama と Nils Anders Danielsson によって開発されたコマンドラインツールおよび強力なEmacsモードの両方を提供する。 Agda 実装者会議(AIM: Agda Implementers' Meeting)が定期的に開催されている。会議期間中は Code Sprint と呼ばれる共同作業に多くの時間が割り当てられ、参加者は小グループに分かれて Agda の機能拡張、ドキュメント整備、ライブラリ作成などを進める。 Agda 2 はEpigramに似ている。 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「Agda」の詳細全文を読む スポンサード リンク
|