Agda
対話的システム、関数型プログラミング言語
From Wikipedia, the free encyclopedia
Agda（アグダ）は、定理証明器、すなわち数学的な証明を検証するコンピュータプログラムであり、ペール・マルティン＝レーフの型理論の一種における構成的証明構築のための対話的システムである。機能的には、依存型をもつ関数型プログラミング言語であるともみなすこともできる。1990年代よりチャルマース工科大学で主に開発されている。
| パラダイム | (証明支援システム) |
|---|---|
| 登場時期 |
|
| 開発者 |
チャルマース工科大学  |
| 最新リリース | 2.8.0 / 2025年7月5日[1] |
| 影響を受けた言語 | Coq, (Epigram, ML, Haskell) |
| プラットフォーム | Cross-platform |
| ライセンス |
BSDライセンス |
| ウェブサイト | |
| 拡張子 | .agda, .lagda |
他の定理証明支援系ではスクリプトによって「タクティク」(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に似ている。