トップ 追記

follow ikegami__ at http://twitter.com

イネムリネズミ日記

いけがみを召喚するには、出現予定を参考にしてください。三週間前までにメールをくだされば、日程を追加するなどしてスケジュールに組み込むことができるかもしれません。勉強会や個人的な会合、中途採用面接などに応じます。日記に書かないことはこちら

2003|04|05|06|07|11|12|
2004|01|02|03|04|05|06|07|10|11|
2005|01|02|03|04|05|06|07|08|11|
2006|09|10|11|12|
2007|01|02|03|04|05|06|07|08|09|10|11|12|
2008|01|02|03|04|05|06|07|08|09|10|11|12|
2009|01|02|03|04|05|06|07|08|09|11|12|
2010|03|04|12|
2011|02|03|04|06|08|09|10|

2011-10-28 Tumblr はじめました [長年日記]

まとまった文章書く気力がなかなか出ないのと、ついつい Twitter で言いたいことつぶやいて、何も残らない現象起きています。FaceBook もあるし Google+ もあるし、使い分け難しいね。

そこで、下書きみたいな気持ちで書いた文章を 不思議の国のイネムリネズミ(Tumblr) に書くことにしました。(追記:URLのスペル変えました、ブックマークしたひとは変えてください、すみません)

位置付けは次のように考えています:

ここ、イネムリネズミ日記
わりとまとまった主張を書く場所。アンテナや RSS フィードに捕捉されているし、読者を意識した文章にする。
Tumblr
下書き。あるいは、どこかの引用。
FaceBook
近況報告(英語)。友人限定。
Google+
近況報告(日本語)。友人限定。
Twitter
たれながし。しょうもない。

文章ではないですが、なにか作ったものは GitHub に置くようにします。


2011-09-11 続く残暑 [長年日記]

_ Agda(リリース版) のインストール

現在の 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 (開発版)のインストール

バグを踏むのを恐れずに先端のソフトウエアを使いたい人向けに、開発版のインストールの方法も説明する。

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 については、MacPortsFinkGentoo 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 オプション付きで起動する)

  • M-x describe-variable して変数 exec-path, load-path, agda2-include-dirs などを確かめる
  • exec-path 上に ghci があるか
  • load-path 上に haskell-mode があるか
  • load-path 上に agda2.el や agda2-mode.el など works/Agda/src/data/emacs-mode にある Emacs ライブラリがあるか
  • agda2-mode で C-c C-l したあと、C-x b で *ghci* バッファに移動しメッセージを見る

ここまでのことを試した (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 コマンドがインストールされないという指摘をメーリングリストで頂いたので更新しました。


2011-09-09 秋よ来い [長年日記]

_ 旧 Agda で書かれた Hoare 論理のライブラリを Agda2 に翻訳した

旧 Agda で書かれた Hoare 論理のライブラリAgda2 に翻訳した件について。

Separation 論理が Hoare triple で書かれているので、それを Agda にもちこむにはどうしたらよいのだろうかという妄想から、移植プロジェクトが始まった。Separation 論理は巨大なサイズの Coq ライブラリとして実現されている。それを Agda でどうこうするのは大変だろうなという想像はつくが、どれだけ大変なのかを身をもって知りたかった。

移植の方針は、1) 実直に翻訳 2) Agda 標準ライブラリをできるだけ使う 3) 足したり引いたりしない、の以上3点で行った。ファイル名や関数名は元のファイルからそのまま書き写したので、Agda2 の convention に合わないものもある。

Hoare.agda

Hoare 論理モジュール。コマンドの意味論を与える関数などをパラメータとしてとる。健全性(Soundness)の証明が入っている。

Prim.agda

上述の Hoare 論理モジュールにわたすパラメータの構築子が入っている。

RelOp.agda/SET.agda

RelOp.agda は二項関係の補題など。SET.agda はよく使う補題をまとめている。

Integer.agda

Prim.agda の付随物。

Eg2.agda/Eg2Sub.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 のライブラリはどこまでやっているのだろうか。


出現予定(召喚方法 ikegami@madscientist.jp):

RSS feed を再開しました。RSS の思想を尊重するために全文配信はしません、あしからず。