いけがみを召喚するには、出現予定を参考にしてください。三週間前までにメールをくだされば、日程を追加するなどしてスケジュールに組み込むことができるかもしれません。勉強会や個人的な会合、中途採用面接などに応じます。日記に書かないことはこちら。
まとまった文章書く気力がなかなか出ないのと、ついつい Twitter で言いたいことつぶやいて、何も残らない現象起きています。FaceBook もあるし Google+ もあるし、使い分け難しいね。
そこで、下書きみたいな気持ちで書いた文章を 不思議の国のイネムリネズミ(Tumblr) に書くことにしました。(追記:URLのスペル変えました、ブックマークしたひとは変えてください、すみません)
位置付けは次のように考えています:
文章ではないですが、なにか作ったものは GitHub に置くようにします。
現在の Agda のインストールの方法を解説する。今後の開発状況によって、やり方は大きく変わる可能性があるので注意すること。Agda Wiki に最新の方法が記述されるはずである。
Linux/*BSD については、いくつかのプラットフォーム Agda on Debian/Ubuntu/Arch : FreeBSD でパッケージされているものもある。あるいは、Haskell Platform を導入したうえで、cabal update; cabal install Agda-executable をおこなう。これで ghc の Agda ライブラリおよびコマンド agda と agda-mode がインストールされる。このままだと、まだ .emacs が設定されていないので、コマンド
% agda-mode setup
により .emacs を編集する。コマンド agda-mode は cabal でインストールしたならば ~/.cabal/bin に置かれるはずである。
MacOSX では Wiki の記述 Agda for MacOSX に従えばよい。
Windows では、 all-in-one package of Agda for Windows があるので、それをインストールすればいいだろう。ただし、Agda は Unicode を頻繁に用いるので綺麗に表示するフォントが必要になる。
つぎに Agda 標準ライブラリをダウンロードし .emacs を設定する(Wiki に記述あり)。Agda 標準ライブラリは、Ubuntu や Debian では agda-stdlib というパッケージになっているのでそれをインストールしてもよい。
バグを踏むのを恐れずに先端のソフトウエアを使いたい人向けに、開発版のインストールの方法も説明する。
Agda は ghc (Glasgow Haskell Compiler) と haskell-mode と Agda それ自身(ghc の Agda ライブラリと Emacs の agda2-mode.el など)、および Agda 標準ライブラリに依存するソフトウエアである。したがって、この 4 種類をインストールする必要がある。開発版をインストールするために、分散バージョン管理ツール darcs をインストールする。
ghc のインストールは、Haskell Platform を導入するのが楽である。
haskell-mode は Linux ならばディストリビューションに応じてパッケージが存在するはずである。なければ、haskell-mode for Emacs サイトからダウンロードし、Emacs の load-path のどこかにおく。
Emacs は、Linux なら必ずパッケージが存在するはずである。MacOSX については、MacPortsや Fink、Gentoo Portage のパッケージで導入してもよいし、Aquamacs をインストールするのもよい。
Agda と Agda 標準ライブラリの開発版を導入するために darcs をインストールする。 Linux ならばディストリビューションに応じてパッケージが存在するはずである。なければ、cabal install darcs とする。MacOSX でも同様にすればよい。なお、cabal は Haskell Platform に付随する。
Agda の開発版を取得し、インストールするために、作業ディレクトリをつくり(ここでは works とする)、つぎのコマンドを実行する:
% cd works % darcs get --lazy http://code.haskell.org/Agda % cd Agda % runghc Setup.hs configure % runghc Setup.hs build % sudo runghc Setup.hs install % cd src/main % runghc Setup.hs configure % runghc Setup.hs build % sudo runghc Setup.hs install
上記の手順で agda のみならず、Emacs の agda2-mode を設定するコマンド agda-mode がインストールされる。agda-mode コマンドは agda-mode setup で、.emacs を編集する。が、その実体は、つぎの snippet を .emacs に追加するだけである:
(load-file (let ((coding-system-for-read 'utf-8))
(shell-command-to-string "agda-mode locate")))
.emacs が汚染されるのを嫌うぼくのような人間は、works/Agda/src/data/emacs-mode/ を load-path に置けばよい。開発版レポジトリからのシンボリックリンクにしておけば、アップデートの手間を省くことができる。
つぎに、Agda 標準ライブラリを開発レポジトリから入手する:
% cd works % darcs get --lazy http://www.cse.chalmers.se/~nad/repos/lib/
最後に、.emacs を設定する:
;; agda2.el などを load-path 上に置くこと
(load-library "agda2")
(add-hook 'agda2-mode-hook
(lambda ()
(add-to-list 'agda2-include-dirs
(expand-file-name ("どこか/works/lib/src"))) ; Agda 標準ライブラリ
))
次のファイル Foo.agda を読み込んだとき agda2-mode になり、さらに C-c C-l でエラーが起きなければインストールに成功したといってよい(ロードが終わると toolbar に Agda:Checked と表示される、これは Agda の型検査が終了したことを示す):
module Foo where import Data.Nat
トラブルシューティング:うまくいかない場合は次のことを確認してみるとよいだろう(emacs を --debug-init オプション付きで起動する)
ここまでのことを試した (darcs get した) うえで、レポジトリを最新に保つには、つぎのコマンドを行う:
% cd works/Agda % darcs pull % cd works/lib % darcs pull
Agda 標準ライブラリの場合は、これで最新にアップデートされる。Agda については、ふたたび runghc を走らせて更新する必要がある。
% cd works/Agda % runghc Setup.hs configure % runghc Setup.hs build % sudo runghc Setup.hs install % cd src/main % runghc Setup.hs configure % runghc Setup.hs build % sudo runghc Setup.hs install
[2011-09-22 追記] src/main ディレクトリでもふたたび runghc Setup.hs install しないと agda コマンドがインストールされないという指摘をメーリングリストで頂いたので更新しました。
旧 Agda で書かれた Hoare 論理のライブラリを Agda2 に翻訳した件について。
Separation 論理が Hoare triple で書かれているので、それを Agda にもちこむにはどうしたらよいのだろうかという妄想から、移植プロジェクトが始まった。Separation 論理は巨大なサイズの Coq ライブラリとして実現されている。それを Agda でどうこうするのは大変だろうなという想像はつくが、どれだけ大変なのかを身をもって知りたかった。
移植の方針は、1) 実直に翻訳 2) Agda 標準ライブラリをできるだけ使う 3) 足したり引いたりしない、の以上3点で行った。ファイル名や関数名は元のファイルからそのまま書き写したので、Agda2 の convention に合わないものもある。
Hoare 論理モジュール。コマンドの意味論を与える関数などをパラメータとしてとる。健全性(Soundness)の証明が入っている。
上述の Hoare 論理モジュールにわたすパラメータの構築子が入っている。
RelOp.agda は二項関係の補題など。SET.agda はよく使う補題をまとめている。
Prim.agda の付随物。
具体例 { x = 2 } if (x = 1) then y:=3 else z:=3 fi { x < z }
実直に翻訳したので、わかりやすさが多少犠牲になっている。すべてを説明しようとすると長くなってしまうので、勘所を。
Hoare.agda のなかにある代数的データ型 data HTProof : Cond -> Comm -> Cond -> Set が、Hoare 論理の論理式を構成する。論理式の意味するところは、ITPro の記事に詳しい。
Hoare 論理でプログラムの性質の証明をするとき、論理式を組み上げるだけなら HTProof を使った項の型検査を Agda でやればよい。実際、 Eg2.agda はそれをやっている。
しかし、このライブラリは少し欲張っていて、プログラムの意味論を与えている。さらに Hoare 論理で証明された論理式から、意味のうえで「正しい」ことも示している。それが、Hoare.agda のなかの関数 SemComm と証明 Soundness である。
関数 SemComm の中身は二項関係である。中身を理解するには RelOp.agda と SET.agda を行き来する必要がある。
SemComm Skip = ... SemComm Abort = ... SemComm (PComm pc) = ... SemComm (Seq c1 c2) = ... SemComm (If b c1 c2) = ... SemComm (While b c) = ...
Agda2 での二項関係の定義がなにかを RelOp.agda と Agda 標準ライブラリで理解したなら、 SemComm の定義の右辺を追うことができる。While b c の意味だけが、少しトリッキーで、自然数 n があって n 回 b が成り立ち c が行われ n+1 回目で b が不成立という関係を n についてわたった和を取っている。
Satisfies : Cond -> Comm -> Cond -> Set
Satisfies bPre cm bPost
= (s1 : State) -> (s2 : State) ->
SemCond bPre s1 -> SemComm cm s1 s2 -> SemCond bPost s2
Soundness : {bPre : Cond} -> {cm : Comm} -> {bPost : Cond} ->
HTProof bPre cm bPost -> Satisfies bPre cm bPost
Soundness の証明は 100 行にわたり、その実は補題つかいまくりの証明なので説明できません。Agda は tactics 使わないので証明が読めるとかいう話を聞いたけどそれは嘘だね。翻訳するときに型検査通しているときは証明追えましたが、数日経つと忘れてしまった。コメントとして、ドキュメントを残しておけばよかった。
そして、本来の目的の Separation 論理を Agda でやる上での困難ですが、証明図を書いてそれを検査するだけなら、今回の Hoare 論理ライブラリ同様に代数的データ型で定義してやればよいだけに思われる。だけど、意味論を与えてその上での正しさまで証明しようとすると、Hoare 論理で 100 行(しかも大変だった)かかっていたものをやることになるので、そこが大変だろう。Coq のライブラリはどこまでやっているのだろうか。
RSS feed を再開しました。RSS の思想を尊重するために全文配信はしません、あしからず。
