AgdaというHaskellとは違うプログラミング言語を触り始めました。実は以前から少し触っていたのですが、PDFリーダーの試作を始めてからすっかり勉強を怠っていました。
どういうことができる言語かと言いますと、「数学の定理」が「証明」できます。
例えば、
(3 × 4) + (2 × 4)
という数式は、素直にやれば
①
(3 × 4) + (2 × 4) =
12 + (2 × 4) = 12 + 8 = 20
という計算になりますが、
因数分解を知っていれば、3と2がまとめられて、
②
(3 × 4) + (2 × 4) =
(3 + 2) × 4 = 5 × 4 = 20
といった具合に別の計算もできます。
ここで重要なのは「同じ結果を返す」一方で、「計算の回数（コスト）」が異なっていることです。
①：掛け算が2回、足し算が1回
②：足し算が1回、掛け算が1回
②のほうが効率的に計算できるとわかります。
これは簡単な計算でしたが、大掛かりなプログラムについても同様のことが言えます。少しの変更が大きな速度向上につながることは往々にして見受けられます。
ただし、「同じ結果を返す」ことをどう保証するか、というのが問題になります。
この辺は人間が数学的に証明するというのが現状ですが、それを楽にする（支援する）プログラミング言語が存在します。
そのうちの一つがAgda(CoqとかIdrisというのも有名です)になります（※１）。
支援というのはある程度ルールに従って、これは機械がやれるよ、という箇所を端折るということのようです。
発見的に色々なルートみつける、それを戦略をもって証明する、ということが機械学習(流行りのいわゆるA.I.)の技術を応用して、やれるんじゃないかと思っています（※２）。
他にもとっておきのネタがありますが、Agda（及び型理論）をマスターしないと本当にやれるかは不明なのでここでは触れません。
このAgdaという言語（およびその開発環境のemacs）は、普通のプログラミング言語と毛色が違ってゲーム感覚で証明を楽しめます（※３）。
①戦略をユーザーが考えて証明していく（パズルゲーム）
②ユーザーがゲーム世界の構造物を配置する、その構造物について成り立つ定理を証明していく（箱庭ゲーム）
上のように、結構重要な技術でもっと普及したほうが良いと勝手に思っています。有志の方達の紹介もありますが、結構上級者向けで難しいと見ています。上級者でない自分が、他人に説明する資料を作る、それを通して自分の理解を深める、ということができる良いタイミングっぽいので、動画を撮りながらプログラムして面白いのが出てきたら紹介してみようと思います。
次回は、Agdaの開発環境の導入方法と、具体的に何かを証明している様子（動画）を紹介する予定です。よろしくお願いします。
導入方法：https://polymony.net/2019/05/16/07-installationofagda/
証明の様子：https://polymony.net/2019/05/26/post-536/
（※１）最初は人口が多く、チュートリアルもたくさんあるCoqにしようとしましたが、AgdaはHaskellと近い文法なので最後はAgdaを選択しました。CoqというのはOCamlというこれも関数型プログラミング系言語ですが、そちらをベースに作られているようです。
（※２）実は”Type Theory and Formal Proof: An Introduction”の受け売りですが。。。こういう型理論+証明論と機械学習の両方に通じている人間はなかなかおらず、今後誰かがやるといい感じ、みたいなことが最後に書かれています。
（※３）そのあたりは次回の動画を見てもらえればと思います。また、型理論という学問の観点からするとAgdaはHaskellの上位互換っぽいです（例えば、長さがnの配列、という型をAgdaだと扱えます）。実用面はまだまだっぽいですが、Haskellを深く知るためにもAgdaをやったほうが良いという感があります。