Agdaを触ってみて

Agda

　今回大学の講義で使用したAgdaについての紹介です。
　そもそもAgdaとは？wikiによると

Agdaは定理証明器、すなわち数学的な証明を検証するコンピュータプログラムである
（中略）
他の定理証明支援系ではスクリプトによって「戦略」を指定して証明を操作するのに対して、Agda では証明を項として表し直接操作するというアイデアに基づいている。言語はデータ型や case式、シグネチャやレコードといった一般的なプログラミング構成概念をもつ。Emacsインターフェイスを使って対話的にコードを作成できるほか、直接コードをコンパイルする処理系の開発も進んでいる。

　とのこと。簡単に言うと A -> B とか B -> (A and (B -> A)) などの論理式が成り立っていることを証明するためのものです。

　ではAgdaを使うために手始めにinstallから。

Agdaのinstall

ここでは詳しい話は省いて手順だけ書きます。$はプロンプト。
私の開発環境は

であった。

Homebrewでinstallしていく。Homebrewはinstallする前にupdateしておくといい。

1,GHCのinstall
 $brew install ghc
2,Haskell-platformのinstall

結構時間かかる。インストール開始からしばらくは動いてないっぽいけど我慢する。ちゃんとはいるから。

     $brew install Haskell-platform
3,cabalのupdate

なんかbrewからのhaskell-platformで入れたcabalはすごくふるいっぽいのでcabalのupdate

     $cabal install cabal-install


少し結構時間かかる

4,Agdaのinstall
     $cabal install Agda

時間かかった。一時間ぐらいかかったんじゃないか？

5,Emacsでの設定

で.emacs.dにて下記コマンドでemacsでAgdaを使えるようにする

     $agda-mode setup

これで使えるようになりました。


どう使うの？

例としてHelloWorldでも。

Agdaはemacsでしか使うのが標準的なそうなのでemacsで使う。

emacsでhello.agda　を作成。

以下を書き込む

module hello where

open import IO

main = run (putStrLn "Hello, あぐだworld!")


agdaを使うにはemacs起動中にコマンド
C-c C-l
をすればいいらしい。コンパイルは
C-c C-x C-c


論理式の証明はまた次の記事で。