Agda（アグダ）は、定理証明器、すなわち数学的な証明を検証するコンピュータプログラムであり、ペール・マルティン＝レーフの型理論の一種における構成的証明構築のための対話的システムである。機能的には、依存型をもつ関数型プログラミング言語であるともみなすこともできる。1990年代よりチャルマース工科大学で主に開発されている。
他の定理証明支援系ではスクリプトによって「タクティク」(tactic)を指定して証明を操作するのに対して、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に似ている。
脚注
参照
C. Coquand et al. An Emacs interface for type directed support constructing proofs and programs. ENTCS 2006. A. Abel, et al. Verifying Haskell Programs Using Constructive Type Theory, ACM SIGPLAN Workshop Haskell'05, Tallinn, Estonia, 30 September 2005 http://www.tcs.informatik.uni-muenchen.de/~abel/haskell05.pdf M. Benke et al. Universes for generic programs and proofs in dependent type theory. Nordic Journal of Computing, 10(4):265-289, 2003. http://www.cs.chalmers.se/~marcin/Papers/universes.pdf T. Coquand et al. Connecting a Logical Framework to a First-Order Logic Prover. FroCos 2005, pp. 285-301.
外部リンク The Agda 2 homepage (wiki) ドキュメントとバグ報告ツールへのリンク Agda version 1 home page