Agda（プログラミング言語）

アグダ
パラダイム	総機能
デザイン：	ウルフ・ノレル。カタリナ・コカンド (1.0)
開発者	チャルマース工科大学
初登場	1.0 – 1999 2.0 – 2007 （1999年） （2007年）
安定版リリース	2.8.0 / 2025年7月5日 （2025年7月5日）
タイピングの規律	強い、静的、依存的、名目上の、明白な、推論された
実装言語	ハスケル
OS	クロスプラットフォーム
ライセンス	BSDライク[ 1 ]
ファイル名拡張子	.agda、、、、、.lagda​.lagda.md​.lagda.rst​.lagda.tex
Webサイト	wiki .portal .chalmers .se /agda
影響を受けた
ロク、エピグラム、ハスケル
影響を受けた
イドリス

Agdaは依存型関数型プログラミング言語であり、元々はチャルマース工科大学のウルフ・ノレルによって開発され、その実装は彼の博士論文に記載されています。^{[ 2 ]}オリジナルのAgdaシステムは1999年にチャルマース大学のカタリナ・コクアンドによって開発されました。^{[ 3 ]}現在のバージョンは元々Agda 2と名付けられていましたが、完全に書き直されたもので、名前と伝統を共有する新しい言語と考えるべきです。

Agdaも命題型パラダイム（カリー・ハワード対応）に基づく証明支援システムですが、 Rocqとは異なり、独立したタクティクス言語を持たず、証明は関数型プログラミングスタイルで記述されます。この言語は、データ型、パターンマッチング、レコード、let式、モジュールといった一般的なプログラミング構造と、Haskell風の構文を備えています。このシステムはEmacs、Atom、VS Codeとのインターフェースを備えています^{[ 4 ] [ 5 ] [ 6 ]}が、コマンドラインインターフェースからバッチ処理モードで実行することもできます。

^{Agdaは、Zhaohui Luoの依存型の統一理論（UTT） [ 7 ]}に基づいています。これはMartin-Löf型理論に似た型理論です。

Agdaは、 Cornelis Vreeswijk [ ^{8 ]}作詞のスウェーデンの歌「Hönan Agda」にちなんで名付けられました。この歌^はAgdaという名の雌鶏について歌われています。これは定理証明器Rocqの名前に由来しており、Rocqは元々Thierry CoquandにちなんでCoqと名付けられていました。

特徴

帰納的型

Agda でデータ型を定義する主な方法は、非依存型プログラミング言語の 代数データ型に似た帰納的データ型を使用することです。

Agda における ペアノ数の定義は次のとおりです。

データℕ :ゼロを設定: ℕ suc : ℕ → ℕ 

基本的に、自然数を表す 型の値を構築するには2つの方法があることを意味します。まず、は自然数であり、が自然数である場合、の次の数を表すも自然数です。 ${\displaystyle \mathbb {N} }$ zeronsuc nn

2 つの自然数間の「以下」関係の定義は次のとおりです。

データ_≤_ : ℕ → ℕ →セットここでz≤n : { n : ℕ } →ゼロ≤ n s≤s : { n m : ℕ } → n ≤ m → suc n ≤ suc m 

最初の構成子 はz≤n、0は任意の自然数以下であるという公理に対応します。2番目の構成子 は推論規則に対応し、 の証明をの証明にs≤s変換します。^{[ 9 ]}したがって、値は1（0の次の数）が2（1の次の数）以下であるという証明です。中括弧で囲まれたパラメータは、推論可能な場合は省略できます。 n ≤ msuc n ≤ suc ms≤s {zero} {suc zero} (z≤n {suc zero})

依存型パターンマッチング

コア型理論では、帰納法と再帰原理を用いて帰納的型に関する定理を証明します。Agdaでは、代わりに依存型パターンマッチングが使用されます。例えば、自然数の加算は次のように定義できます。

ゼロを加えるn = n 加算( suc m ) n = suc (加算m n )

再帰関数／帰納的証明をこのように記述する方が、生の帰納原理を適用するよりも自然です。Agdaでは、依存型パターンマッチングは言語の基本機能であり、コア言語にはパターンマッチングが変換する帰納法／再帰原理が欠けています。

メタ変数

Agdaの特徴の一つは、Rocqなどの他の類似システムと比較して、プログラム構築においてメタ変数に大きく依存していることです。例えば、Agdaでは次のような関数を記述できます。

追加： ℕ → ℕ → ℕx y = ? を加算します。

?ここにメタ変数があります。Emacsモードでシステムを操作すると、期待される型が表示され、メタ変数を改良（つまり、より詳細なコードに置き換える）することができます。この機能により、Rocqなどのタクティクスベースの証明支援システムと同様に、段階的なプログラム構築が可能になります。

証明自動化

純粋型理論によるプログラミングには、多くの退屈で反復的な証明が伴います。Agdaには独立したタクティック言語はありませんが、Agda内で有用なタクティックをプログラムすることは可能です。通常、これは、オプションで関心のあるプロパティの証明を返すAgda関数を記述することで実現されます。そして、型チェック時にこの関数を実行することでタクティックを構築します。例えば、以下の補助定義を使用します。

データMaybe ( A : Set ) : Set where Just : A → Maybe A Nothing : Maybe AデータisJust { A : Set } : Maybe A → Set 、auto : ک { x } → isJust ( Just x )戦術: ∀ { A : Set } ( x : Maybe A ) → isJust x → A 戦術何もしない() 戦術( xだけ) auto = x 

( absurd()と呼ばれるパターンは、型チェッカーがその型に値が存在しないことを検出した場合、つまりそれが偽の命題を表していることが証明された場合に一致します。これは通常、すべての可能なコンストラクタに利用できない引数があるため、つまりそれらが満たせない前提があるためです。ここでは、そのコンテキストではコンストラクタ を適用できる type の値が存在しないため、 type の値を構築できません。absurd パターンを含む方程式では右側の辺は省略されます。)数値を入力し、オプションでその偶数性の証明を返す関数を考えると、次のようにタクティックを構築できます。 isJust AAJustcheck-even : (n : ${\displaystyle \mathbb {N} }$ ) → Maybe (Even n)

チェックイーブン戦術: { n : ℕ } → isJust (チェックイーブンn ) →イーブンn チェックイーブンタクティック{ n } =戦術(チェックイーブンn )補題0 :ゼロでも 補題0 =チェックイーブン戦術自動補題2 :偶数( suc ( sucゼロ)) 補題2 =チェック偶数戦術自動 

各補題の実際の証明は型チェック時に自動的に構築されます。この戦術が失敗した場合、型チェックも失敗します。

さらに、より複雑なタクティクスを記述するために、Agdaはリフレクションプログラミング（リフレクション）による自動化をサポートしています。リフレクション機構により、プログラムフラグメントを抽象構文木に引用したり、抽象構文木から引用を解除したりすることができます。リフレクションの使用方法は、Template Haskellの動作に似ています。^{[ 10 ]}

証明自動化のためのもう一つのメカニズムは、 Emacsモードにおける証明検索アクションです。これは、可能な証明項（5秒に制限されています）を列挙し、そのうちの1つが仕様に適合する場合、アクションが呼び出されるメタ変数に格納されます。このアクションは、例えば、どの定理とどのモジュールから使用できるか、アクションがパターンマッチングを使用できるかどうかなどのヒントを受け付けます。^{[ 11 ]}

終了チェック

Agdaは完全な関数型プログラミング言語です。つまり、Agda内の各プログラムは必ず終了し、すべての可能なパターンが一致する必要があります。この機能がなければ、言語の背後にあるロジックに矛盾が生じ、任意の文を証明できるようになります。Agdaは終了性チェックのために、Foetus終了性チェッカーのアプローチを採用しています。^{[ 12 ]}

標準ライブラリ

Agdaには、自然数、リスト、ベクトルといった基本的なデータ構造に関する多くの有用な定義と定理を含む、広範なデファクトスタンダードライブラリがあります。このライブラリは現在ベータ版であり、活発に開発が進められています。

ユニコード

Agdaの注目すべき特徴の一つは、プログラムのソースコードがUnicodeに大きく依存していることです。Emacsの標準モードでは、\SigmaΣなどの入力にショートカットが使用されます。

バックエンド

コンパイラ バックエンドには、Haskell 用の MAlonzo とJavaScript用の MAlonzo の 2 つがあります。

参照

• 証明補助ツールのリスト

参考文献

1. Agdaライセンスファイル
2. ウルフ・ノレル. 依存型理論に基づく実用的なプログラミング言語に向けて. 博士論文. チャルマース工科大学, 2007. [1]
3. 「Agda: インタラクティブな証明エディタ」 。 2011年10月8日時点のオリジナルよりアーカイブ。2014年10月20日閲覧。
4. Coquand, Catarina; Synek, Dan; Takeyama, Makoto (2005).証明とプログラムの構築における型指向サポートのためのEmacsインターフェース(PDF) . European Joint Conferences on Theory and Practice of Software 2005. 2011年7月22日時点のオリジナル(PDF)からアーカイブ。
5. 「Atom上のagda-mode」 。 2017年4月7日閲覧。
6. "agda-mode - Visual Studio Marketplace" . marketplace.visualstudio.com . 2023年6月6日閲覧。
7. Luo, Zhaohui.計算と推論：コンピュータサイエンスのための型理論. Oxford University Press, Inc., 1994.
8. “[Agda] 「Agda」の由来? (Agda メーリングリスト)” . 2020 年10 月 24 日に取得。
9. 「Agda標準ライブラリのNat」 . GitHub . 2014年7月20日閲覧。
10. Van Der Walt, Paul, Wouter Swierstra. 「Agdaにおけるリフレクションによるエンジニアリング証明」『関数型言語の実装と応用』pp. 157-173. Springer Berlin Heidelberg, 2013. [2]
11. コッケ、ペピン、ワウター・スヴィアストラ。 「アグダの自動車。」
12. Abel, Andreas (1998年7月16日). 「foetus -- 単純な関数型プログラムの終了チェッカー」. arXiv : 2407.06924 [ cs.PL ].

さらに読む

• Bove, Ana; Dybjer, Peter; Norell, Ulf (nd). 「Agdaの概要 - 依存型を持つ関数型言語」(PDF) .
• Norell, Ulf; Chapman, James (nd). 「Agdaにおける依存型プログラミング」(PDF) .

外部リンク

• 公式サイト
• ダニエル・ピーブルズによる5部構成のYouTubeプレイリスト「Agda入門」
• Agdaにおける依存型の残酷な[メタ]入門
• Agda チュートリアル:「理論的な背景なしで Agda プログラミングを探索する」
• HoTTESTサマースクール2022、ホモトピー型理論に関する66の講義（Agdaに関する多くの入門講義と演習を含む）