Agda

出典: フリー百科事典『ウィキペディア(Wikipedia)』
移動: 案内検索
Agda
パラダイム 関数型
最新リリース 2.3.0.1 / 2012年3月12日(2年前) (2012-03-12
影響を受けた言語 Coq, Epigram, Haskell
プラットフォーム Cross-platform
ウェブサイト Agda wiki
拡張子 .agda, .lagda
agda2による証明の抜粋

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に似ている。

参照[編集]

  • 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.

外部リンク[編集]