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

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

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

データℕ :セット、ゼロ: ℕ 、 suc : ℕ → ℕ 

つまり、型の値を構築するには2つの方法があるということです。${\displaystyle \mathbb {N} }$は自然数を表します。まず、zeroは自然数であり、がn自然数であれば、の後継数suc nであるも自然数です。n

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

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

最初のコンストラクタ は、z≤n0 は任意の自然数以下であるという公理に対応します。 2 番目のコンストラクタ はs≤s推論規則に対応し、 の証明をn ≤ mの証明に変換できますsuc n ≤ suc m。^{[ 9 ]}したがって、 の値は、1 (0 の後継数) が 2 (1 の後継数) 以下であるという証明です。中括弧s≤s {zero} {suc zero} (z≤n {suc zero})で指定されたパラメータは、推論できる場合は省略できます。

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

ゼロを追加n = n add ( suc m ) n = suc ( add m n )

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

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

追加: ℕ → ℕ → ℕx y を加えるとどうなるか？ 

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

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

データMaybe ( A : Set ) : Set where Just : A → Maybe A Nothing : Maybe Adata isJust { A : Set } : Maybe A → Set where auto : ∀ { x } → isJust ( Just x )戦術: ∀ { A : Set } ( x : Maybe A ) → isJust x → A 戦術なし() 戦術(ただx )自動= x 

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

check-even-tactic : { n : ℕ } → isJust ( check-even n ) → Even n check-even-tactic { n } = Tactic ( check-even n )lemma0 :ゼロは偶数 lemma0 =チェックイベント戦術自動lemma2 : Even ( suc ( suc zero )) lemma2 = check-even-tactic auto 

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

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

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

Agdaは完全な関数型プログラミング言語であり、つまり、その中のすべてのプログラムは終了し、考えられるすべてのパターンに一致しなければなりません。この機能がなければ、言語の背後にある論理は矛盾し、任意のステートメントを証明することが可能になります。終了チェックには、AgdaはFoetus終了チェック器のアプローチを使用します。^{[ 12 ]}

Agdaには、自然数、リスト、ベクトルなどの基本的なデータ構造に関する多くの有用な定義や定理を含む、事実上の標準ライブラリが充実しています。このライブラリはベータ版であり、現在も活発に開発が進められています。

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

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