Agdaに入門した

Agdaのインストールは、ドキュメントの指示に従い、brew install agdaでやりました。Agdaのバージョンは2.6.2.1で、standard libraryのバージョンは1.7.1でした。環境はM1 Mac (Big Sur)です。agda-mode setupが上手く動かなかったので、手動で~/.emacs.d/init.elを編集しました。

(load-file (let ((coding-system-for-read 'utf-8))
                (shell-command-to-string "agda-mode locate")))

exec-path-from-shellも念のためemacsにインストールし、(exec-path-from-shell-initialize)~/.emacs.d/init.elに追記しています。

standard libraryの設定もする必要があります。ドキュメントには/usr/local/lib/agda/にstandard libraryがあると書いてありますが、私の環境では/opt/homebrew/lib/agda/にありました。$(brew --prefix)/lib/agda/の内容を見るのが確実です。作業としては、~/.agda/libraries~/.agda/defaultsに適切な内容を記入するだけです。

Terminal.app内のemacsのagda-modeの表示が崩れていたので、試行錯誤の結果、

で解決しました。

入門

公式のチュートリアル(‘Hello world’ in AgdaA Taste of Agda)と、Programming Language Foundations in AgdaのPart 1をやりました。Programming Language Foundations in Agdaは、Part 1だけでも数日はかかります。これだけやれば、自力である程度は書けるようになります。

ライブラリのドキュメント

standard libraryのドキュメントは、ここから見ることが可能ですが、リリースされたバージョンではなくmasterのドキュメントなので、インストールされているバージョンと内容が異なる場合があります。たとえば、standard library 1.7.1にはData.Fin.raiseしかありませんが、masterにはData.Fin._↑ˡ_Data.Fin._↑ʳ_があります。したがって、HTMLで見るかわりに、emacsで$(brew --prefix)/lib/agda/src/以下を開けば、インストールされているバージョンのドキュメントを見ることができます。emacsで開くことで、C-c C-lでシンタックスハイライトが付き、M-.で定義にジャンプすることができるので、これで十分だと気付きました。(Unicode文字を使った検索も、webブラウザよりemacsの方がやりやすいという利点があります。)

Heterogeneous Equality

Vecについて、[]_++_の右単位元であることを証明したいとき、そのような命題はsubstを用いて

prop : Set₁
prop = forall {A : Set} {n : ℕ} (xs : Vec A n) ->
       subst (Vec A) (+-identityʳ n) (xs ++ []) ≡ xs

と表現することができます。substを使う理由は、xs ++ []の型はVec A (n + zero)であってVec A nではないからです。このような状況では、Relation.Binary.HeterogeneousEquality._≅_を使うと、

prop : Set₁
prop = forall {A : Set} {n : ℕ} (xs : Vec A n) -> xs ++ [] ≅ xs

と表現することができます。subst P eq pは第2引数がreflであると分かったときにしかpにならないので、その点でheterogeneous equalityの方が便利なときもある気がします。

Uniqueness of Identity Proofs (UIP)

Agdaには、--with-K--without-Kというオプションがあり、これらによってKと呼ばれる規則が成り立つかどうかが決まります。デフォルトでは--with-Kが有効になっているので、

K : {A : Set} {x : A} (P : x ≡ x → Set) →
    P refl → (x≡x : x ≡ x) → P x≡x
K P p refl = p

を証明することができます。これは、述語Prefl : x ≡ xについて成り立つならば、任意のx≡x : x ≡ xについてPが成り立つことを意味します。

--without-Kを有効にすると、このKは型検査に通らなくなります。そのかわり、

J : {A : Set} (P : (x y : A) → x ≡ y → Set) →
    ((x : A) → P x x refl) → (x y : A) (x≡y : x ≡ y) → P x y x≡y
J P p x .x refl = p x

は証明することができます。(このJは、--with-Kでも証明できます。)これは、任意のx : AについてP x x (refl : x ≡ x)が成り立つならば、任意のx : A, y : A, x≡y : x ≡ yについてP x y x≡yが成り立つことを意味します。

詳しくはWithout K — Agda 2.6.2.1 documentationを見てください。

--with-Kが有効であるときは、Uniqueness of Identity Proofs (UIP)が任意の型について成り立ちます。UIPは、equality ()の証明が、(存在するならば)一意であるという主張です。

Cubical Agda

Homotopy type theory (HoTT)について聞いたことのある人も多いと思いますが、Cubical type theoryは、より良い計算的性質(canonicityやnormalization)を持つHoTTと言えると思います。特徴的な点は、univalenceが公理ではなく定理であることでしょう。Cubical type theoryには色々な種類がありますが、特にDe Morgan Cubical type theoryと呼ばれる型理論が、Cubical Agdaとして実装されています。Cubical Agdaとしての最低限の機能は--cubicalオプションを使うことで利用できますが、実用上はcubical libraryを使うことが多いでしょう。

cubical libraryのインストールは、git clone https://github.com/agda/cubical && cd cubical && makeを実行した後、cubical.agda-libへのパスを~/.agda/librariesに追記し、cubicalという文字列を~/.agda/defaultsに追記すればよかった気がします。

Cubical Agdaはinterval typeと呼ばれる型Iを導入します。interval typeには2つの定数i0 : Ii1 : Iがあります。注意すべき点は、interval typeを持つ項はi0, i1だけでなく、その2つの「間」に無数の「点」が存在すると考えられることです。interval typeの項はDe Morgan代数を成します。De Morgan代数は、Boole代数(古典論理のモデル)から排中律と無矛盾律を除いたものです。

Cubical Agdaにおいて、equalityは、Relation.Binary.PropositionalEquality._≡_ではなく、path typeと呼ばれるものを使います。型Ax : A, y : Aについて、path typex ≡ yは、関数I -> Aのように扱われます。

path typex ≡ yはdependent path type PathP (λ _ -> A) x yの特別な場合です。PathPを使うと、heterogeneous equalityをより上手く扱えるようになります。

Cubical Agdaでは--without-Kと同じように、UIPが一般には成り立ちません。UIPが成り立つ型に関しては、isPropisSetが役立ちます。たとえば、m : ℕ, n : ℕについて、m ≡ nの証明が2つある場合、Cubical.Data.Nat.isSetℕを使うことで、それらが同じ(equal)であることを証明できます。

Cubical Agdaの文献としては、Internalizing representation independence with univalenceなどを読むと良いです。(本稿ではHITについて触れませんでしたが、この論文はHITを上手く利用しています。)

さいごに

この文章について何か誤り等があれば@elpin1alまでご連絡ください。