日々の流転

λ. Agda2

ずっとAgda2を試そう試そうと思っていたけど、ようやく試した。

まずはインストール。alexとhappyはwindows用のバイナリをダウンロードしてきてPATHの通っている場所に置く。binaryとzlibはまだGHC 6.8対応していないようだったから自分で対応して……とかやってるうちに対応版が出ていた。しょぼーん。Agda2自体も簡単なパッチ(Agda-2.1.2-ghc68-win32.patch)をあててビルドできた。

で、動かしてみる。 Agda1はemacs-agdaというプログラムとelispが通信していたけど、Agda2ではhaskell-modeで動かしたghciにライブラリを読み込ませて、こいつとやり取りをして実現している。これは面白い。よく考えたなぁ。ただ、実行環境を配布したりするのにはちょっと面倒になってしまっているけど。

とりあえず、かなり色々変わっているようなので、色々試してみる。

文法

まずは文法。型宣言に使う記号が「::」から「:」になっていて*1、暗黙の引数は「{A : Set} ->」等として渡すようになっている。 恒等関数はこんな感じになる。

id : {A : Set} -> A -> A
id x = x

嵌ったのがcase。以下の状態でゴール0で C-c C-c で agda2-make-case を呼び出すと「Panic: passAVar: got x」というエラーになる。 サンプルを見てもcaseを使ったのはないみたいだし、caseはなくなったのだろうか。

data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat

f : Nat -> Nat
f x = { x }0

また、この例のようにデータ型定義はGADTスタイルになり、dataとidataの区別も無くなったようだ。 (2007-12-08追記: というか、The Agda Wiki - Inductive Families を見ると、Inductive Families は無くなっているのね。これはAgda1からの乗り換えはまだ難しいか)

それから、演算子の定義でアンダースコアをプレースホルダーとして使うことが出来るようになっていて、中置演算子だけでなく、distfix な演算子も簡単に定義可能。OBJみたいでかっこいい。けど、アンダースコアを含む名前が使えなくなっているので注意。

_+_ : Nat -> Nat -> Nat
zero  + m = m
suc n + m = suc (n + m)

if_then_else_ : {A : Set} -> Bool -> A -> A -> A
if true  then x else y = x
if false then x else y = y

しかし、こうしてみてみると、Haskellに囚われずに文法を拡張していってるんだなぁ、と思う。

停止性検査

それから、停止性検査のagda-check-terminationコマンドはなくなっているので、その辺りはどうなっているのかと思い、以下の例を試す。 そしたら、一行目のbottomと二行目の右辺のbottomが赤くハイライトされた。なるほど、自動的に検査されるようになったのね。

bottom : {A : Set} -> A
bottom = bottom

次はアッカーマン関数を試す。今度は赤くハイライトされない。 Agda1よりは強力なアルゴリズムを使っているようだ。 Size Change Termination (SCT)?　 (2008-03-24 追記: アッカーマン関数のAgdaでの定義 - あいまいな本日の私(2008-03-11)によると、アルゴリズム自体はfoetusの停止判定で変わらず、単にAgda1で実装がまだ追いついていなかったということらしい)

ack : Nat -> Nat -> Nat
ack (zero) n            = suc n
ack (suc m') (zero  )   = ack m' (suc zero) 
ack m@(suc m') (suc n') = ack m' (ack m n')

次に、20050508にAgda1を触ったときにも試した、再帰的なデータ型を試す。結果は「Datatype T is not strictly positive, because it occurs negatively」というエラーになった。正しい対処だとは思うが、HOASを使いたい人とかには残念かもね。

data T (P : Set) : Set where
  psiInv : (T P -> P) -> T P

型クラス

Agda1にあった型クラスは無くなった? examples/Monad.agda にモナドを定義する例があるが、これに関しては以前に比べると非直観的なような。

Prop≠Set

以前に池上さんに教えてもらったように、Setとは別にPropというソートが用意されていて、型の階層は以下のようになっている。 ただ、PropとSetをどう使い分ければ良いかはまだ良くわからない。

• Prop ⊂ Set1
• Set ⊂ Set1
• Set1 ⊂ Set2 ⊂ …

相互再帰

Agda1では定義の中では既に定義済みの定義と自分自身しか参照できなかったため、相互再帰を行いたいときは自分で組化(tupling)を行う必要があった。 それに対して、Agda2ではmutualキーワードを使って相互再帰的な定義を自然に行えるようになっている。

mutual

  even : Nat -> Bool
  even zero    = true
  even (suc n) = odd n

  odd : Nat -> Bool
  odd zero    = false
  odd (suc n) = even n

【2007-12-08追記】 これは勘違い。私が知らなかっただけで、Agda1のころからmutualはあった。

λ. 計画停電

今日(12/2)はSFCで計画停電があるため、この日記も止まる予定。それから、それにあわせてこのサーバーのリプレースも行うそうなので、環境が変わって動かなったりとかもあるかも。

• SFC 慶應義塾大学 湘南藤沢キャンパス - 【再掲】: SFC構内停電に関するお知らせ（注意）
• 2007-10-31 構内停電に伴うネットワークの停止について

【2007-12-08追記】 今回の移行で、Linux/x86からLinux/x86_64になったのだけど、GDBMのフォーマットはアーキテクチャ依存なのを忘れていて、w3mlとRuBBSが動かなくなっていた。 以前、WebサーバがSolaris/sparcからLinux/x86になったときにも嵌ったのに、同じ事で二度失敗するとは……

λ. シャガール展

生誕120年記念　色彩のファンタジー　シャガール展　−写真家イジスの撮ったシャガール− というのをやっていたので、見に行ってみた。 「受付にて『シャガール〜大柴！』とくっきりはっきりいった方は100円割り引きます」とのことなので、ちょっと恥ずかしかったけど言ってみた。もっともルー大柴という人のことは良く知らないのだけど。

λ. 石焼ホットックと黒蜜きな粉アイス

土古里(도고리)というところでお昼を食べて、デザートに「石焼ホットックと黒蜜きな粉アイス」というのを食べた。 「ホットック」って何かと思ったら、お米から作ったお菓子らしい。英語では「Korean Ricecake and Brown Sugar Soybean Flour Icecream in Hot Pebbles」という説明で、韓国語では「돌솥　호떡　콩가루　아이스크림」と説明されていた。韓国語でもアイスクリームは「アイスクリーム」なのね。

λ. “A simple propositional S5 tableau system” by Melvin Fitting

• <URL:http://comet.lehman.cuny.edu/fitting/bookspapers/pdf/papers/SimpleSfive.pdf>
• <URL:http://www.ingentaconnect.com/content/els/01680072/1999/00000096/00000001/art00034>

を読んだ。

S5のシーケント計算はcut-admissibleではない(cf. 様相論理のシーケント計算)から、タブローもややこしいのではないかと思い込んでいたが、想像していたよりもずっと簡単なんだな。しかも、TやS4の決定問題がPSPACEなのに対して、S5の決定問題は高々NP完全で済むそうだ。これは、TやS4では(様相を剥がす時の)ブランチの破壊的な変更の順序に意味があったが、S5ではどの順序で行っても結果が同じため。

それから、健全性を示すための議論で、全ての世界の間に到達可能性関係が成り立つような構造だけを考えているのが、ちょっと目から鱗だった。S5の通常の構造では到達可能性関係は任意の同値関係なのだけど、ここでの扱いはこの通常の構造における同値類を取り出してきて一つの構造として扱っていると考えられる。妥当性を考える場合には、任意の構造を考えるので、こうしても実は結果は同じ。

ちなみに、何故これを読んだかというと、例によって知識論理を使って論理パズルを解くため。 先日のSPASSで知識の論理を使って論理パズルを解く?では定理証明機SPASSを使ってみたが、S5は決定可能なはずなのに、正しくない結論を与えたときに止まらなくなってしまうようで、どうもよろしくない。 それならば、S5の決定手続きを調べてみよう、という事で読んだのだった。 実際に論理パズルを解くために使うのはまた今度挑戦してみる予定。

【2007-12-04追記】 あれれ!?　この場合のタブローってシーケント計算とほぼ同じで、しかもカットに対応するようなものは入っていないように見えるんだよな。シーケント計算がcut-admissibleでないのに対して、これが完全なのは、一体何が原因?

【2007-12-06追記】 Deep Inference and the Calculus of Structures - Modal Logic 見つけた A Deep Inference System for the Modal Logic S5 という論文には以下のように書いてあったのだが、具体的に何が問題なのか良くわからない……

The failure of the sequent calculus to accommodate cut-admissible systems for the important modal logic S5 (e.g. in Ohnishi and Matsumoto [21]) has led to the development of a variety of new systems and calculi. A partial solution to this problem has been presented in Shvarts [25] and Fitting [5], where theorems of S5 are embedded into theorems of cut-free systems for K45. These systems provide proof search procedures for S5, they are, however, systems of a weaker logic.

λ. 無限オブ無限

稲葉さんの「無限オブ無限」より。

まずは非常に単純な回答。 斜めに列挙するのに比べると、最初の方のリストの要素が出てきやすく、後の方のリストの要素が出てきにくいのが若干問題かも知れないけど。

iflatten :: [[a]] -> [a]
iflatten = foldr interleave []

interleave :: [a] -> [a] -> [a]
interleave (x:xs) ys = x : interleave ys xs
interleave [] ys     = ys

実行結果はこんな感じ。

Main> take 10 $ iflatten [[(i,j)|j<-[1..]] | i<-[1..]]
[(1,1),(2,1),(1,2),(3,1),(1,3),(2,2),(1,4),(4,1),(1,5),(2,3)]

ちなみに、要素が必ず現れるというのは一種の公平性(fairness)なのだけど、こういった方法をより一般化すると Backtracking, Interleaving, and Terminating Monad Transformers (cf. 20050702#p04) でされているような話になるはず。

また、上記のものにあった後の方のリストの要素が出てきにくいという問題も、20050702#p04で書いた bindz のような関数を用いることで解決することが出来るはず。 もちろんこの場合にはもっと単純になると思うけど。

λ. 整礎性は一階述語論理では表現できないのね

先日、ヘンキン文 - ヒビルテ (2007-09-16) で、「Xが証明可能であることを□Xと書くと、証明可能性を様相論理で扱える」ということに触れた。これが Löb Logic と呼ばれる論理で、□(□φ→φ)→□φ という公理図式(axiom schema)を持っていて、PAでの証明可能性をある意味で忠実に反映した体系になっている。 それで、この論理をSPASSで扱って遊べないかと思ったのだけど、ちょっといじっているうちに、出来ないということに気付いた。しょぼーん。以下にその理由を簡単に書く。

SPASSはあくまで一階述語論理の定理証明機なので、□(□φ→φ)→□φ のような様相論理の公理図式は、クリプキ構造に関する一階述語論理の公理で表現してやる必要がある。 そして、□(□φ→φ)→□φ はクリプキ構造の到達可能性関係が推移的かつ整礎(well-founded)であることに対応することが知られている。 で、推移性は何の問題もないのだけど、問題は整礎性。

関係Rの整礎性は「空でない部分集合にはRに関する極小元が存在する」こと、もしくは「x0 R x1 R x2 R … という無限列が存在しない」ことによって定義される*1。 前者の定義では集合を量化する必要があるけど、一階述語論理では個体しか量化できず、集合を量化出来ないのだった。二階論理なら ∀P. (∃x. P(x)) → (∃x. P(x) ∧ ∀y. P(y)→¬R(x,y)) と書けるんだけどね。後者の定義も同様に一階述語論理では書けない。

λ. Coqで“無限オブ無限”

稲葉さんの「無限オブ無限」は余再帰的な関数(corecursive function)の良い例題なのではないかと思い、Coqでも書いてみることにした。 何故いつものAgdaではなくCoqかというと、Agdaはまだcodataに対応しておらず無限リストやストリームを直接扱うことが出来ないため。

まず、Coqでは余再帰的な関数は、全域関数であることを保証するために guarded corecursion の形で書かないといけない。ので、guarded corecursion の形で書こうとしたのだけど、色々試してもどうも書けない。 何故かと思って落ち着いて考えてみたら、そもそも iflatten (repeat []) が実効的(effective)に定義出来ないから、この関数 iflattern は全域的な計算可能関数ではないのだった。

色々細かい条件を色々加えればCoqでも定義できるだろうけど、Coq初心者の私にはそれは面倒なので、とりあえず無限リストの無限リストの場合のみで定義してみた。Coqでマトモに何かを書くのは初めてなので、変な書き方をしてるかも知れないけど、そこは識者のツッコミに期待しておきます(^^;

(* IFlatten.v *)
Section IFlatten.

Require Import List.
Require Import Streams.

(* anamorphisms (co-iteration) *)
CoFixpoint unfold (A X : Set) (phi : X -> A*X) (x : X) : Stream A
:= match phi x with
     | (a, x) => Cons a (unfold A X phi x)
   end.
Implicit Arguments unfold [A X].

Inductive CV (A X : Set) : Set :=
  | CVLast : X -> CV A X
  | CVCons : A * CV A X -> CV A X.
Implicit Arguments CVLast [A X].
Implicit Arguments CVCons [A X].

(* futumorphisms (course-of-values co-iteration) *)
Definition futu (A X : Set) (phi : X -> A * CV A X) (x : X) : Stream A
:= let psi cv :=
         match cv with
           | CVLast x => phi x
           | CVCons p => p
         end
   in unfold psi (CVLast x) .
Implicit Arguments futu [A X].

Definition add_prefix (A : Set) (xs : list A) (X : Set) (cv : CV A X) : CV A X
:= fold_right (fun a cv => CVCons (a, cv)) cv xs.
Implicit Arguments add_prefix [A X].

Definition iflatten (A : Set) (ss : Stream (Stream A)) : Stream A
:= let phi x :=
          match x with
          | (ss, ls) =>
             let s := hd ss in
             let ss2 := tl ss in
             let ls2 := tl s :: List.map (fun x => tl x) ls in
               ( hd s
               , add_prefix
                 (List.map (fun x => hd x) ls)
                 (CVLast (ss2, ls2))
               )
          end
   in futu phi (ss, nil).
Implicit Arguments iflatten [A].

End IFlatten.

(* Haskell のコードを出力する *)
Extraction Language Haskell.
Extraction "IFlatten" iflatten.

これをCoqIDEに読み込ませたら、ちゃんと通った。 Coqで定義が通ったので、少なくともちゃんと全域関数になっていることは分かる。そして、ExtractionでHaskellのソースコードを生成したので、正しく定義できているか簡単に確認してみることに。 このままだと試しにくいのでまずは簡単なラッパを定義する。

import IFlatten

l2s :: [a] -> Stream a
l2s (x:xs) = Cons0 x (l2s xs)

s2l :: Stream a -> [a]
s2l (Cons0 x xs) = x : s2l xs

iflatten' :: [[a]] -> [a]
iflatten' xss = s2l $ iflatten $ l2s [l2s xs | xs <- xss]

で、試す。

Main> take 10 $ iflatten' [[(i,j) | j<- [1..]] | i<-[1..]]
[(1,1),(2,1),(1,2),(3,1),(2,2),(1,3),(4,1),(3,2),(2,3),(1,4)]

うん、ちゃんと定義できてるみたい。 折角Coqで定義したので、題意を満たしていることをちゃんと形式的に証明したいところだけど、それはまだやっていない。

【2007-12-10追記】 にわとり小屋でのプログラミング日記のyoshihiro503さんが、形式的な証明をしてくれたようです。わーい。 ⇒ Coqで”無限オブ無限” - にわとり小屋でのプログラミング日記

λ. A brainf*ck interpreter in Prolog

ふと、現実逃避にPrologでBrainf*ckの簡単なインタプリタを書いてみた。

brainfuck(Src) :- bf(Prog, Src, []), !, seq(Prog, []*[0], _).

bf([]) --> [].
bf([X|Y]) --> bf1(X), {!}, bf(Y).
bf(X) --> [_], bf(X).

bf1('>') --> ">".
bf1('<') --> "<".
bf1('+') --> "+".
bf1('-') --> "-".
bf1('.') --> ".".
bf1(',') --> ",".
bf1(w(X)) --> "[", bf(X), "]".

seq([], T, T).
seq([X|K], T1, T2) :- step(X, T1, T), seq(K, T, T2).

step('>', L*[X|R], [X|L]*R1) :- R=[_|_] -> R1=R ; R1=[0].  
step('<', [X|L]*R, L*[X|R]).
step('+', L*[X|R], L*[Y|R]) :- X=255 -> Y=0 ; Y is X+1.
step('-', L*[X|R], L*[Y|R]) :- X=0 -> Y=255 ; Y is X-1.
step('.', L*[X|R], L*[X|R]) :- put_byte(X).
step(',', L*[_|R], L*[X|R]) :- get_byte(X).
step(w(W), T1, T2) :- while(W, T1, T2).

while(W, T1, T2) :-
    T1=_*[0|_] -> T1=T2 ; seq(W, T1, T), while(W, T, T2).

多分一番メジャーなProlog処理系である SWI Prolog で実行してみる。

% pl 
?- consult(brainfuck).
% brainfuck compiled 0.00 sec, 9,300 bytes

Yes
?- brainfuck("
>+++++++++[<++++++++>-]<.>+++++++[<++++>-]<+.+++++++..+++.[-]>++++++++[<++
++>-]<.>+++++++++++[<+++++>-]<.>++++++++[<+++>-]<.+++.------.--------.[-]>
++++++++[<++++>-]<+.[-]++++++++++.").
Hello World!

Yes
?-

どうせなので、ファイルから読み込んで実行することも出来るようにしてみる。

brainfuck_file(FileName) :- readfile(FileName, X), !, brainfuck(X).

readfile(FileName, Str) :-
    see(FileName), get_byte(B), readfile_loop(B, Str), seen.

readfile_loop(-1, []) :- !. 
readfile_loop(H, [H|T]) :- get_byte(B), !, readfile_loop(B, T).

それはそうと、Brainf*ckって日本語訳するとやっぱり「脳姦」になるのだろうか?　なんというか、氏賀Y太あたりの描くグロ絵を連想してしまって非常にアレでございます。(今回のエントリは実はこれを書きたかっただけ。← 最低です)

【2008-03-27】 WAMのindexing最適化によって不要になるカットを取り除いた。

λ. 第三十五回圏論勉強会

今日は圏論勉強会だった。 写真

今日は“Categories, Types and Structures” の 2.4 Examples of CCC’s からだったのだけど、しょっぱなが 2.4.1 Scott Domains 。 CCCの例としていきなり Scott Domain を持ってくる辺り、この本はかなりぶっ飛んでると思うのだった。どう見ても著者の趣味丸出しです。本当にありがとうございました。しかし、これは Topology via Logic (Cambridge Tracts in Theoretical Computer Science)(Steven Vickers) を持ってきておけばよかったなぁ。

帰ってきてから、Topology via Logic を少し読み返して確認。 順序集合でのコンパクトな要素と、位相空間のコンパクトな集合にはちゃんと関係があって、開集合系を包含関係に関する順序集合と考えたときに、コンパクト開集合はこの順序集合のコンパクトな要素になっている。 また、xがコンパクトな要素の場合にも「x≦⋁S ならばSの有限部分集合S'が存在して x≦⋁S'」は言える。

練習問題の「ii. if x₀ is compact and y ≦ x₀ then y is compact.」の反例は、どこかで見た記憶があると思ったら、イデアル完備化の落とし穴 でほぼ同じ例を書いていた。

λ. Polaroid Gallery を試してみた

いつも圏論勉強会の板書の写真のページはzphotoを使って作っていたのだけど、zphotoは64bit環境には対応していないらしく、エラーになってしまった。 丁度良い機会なので、某サイトで使われていたPolaroid Gallery v.1.01 を、好きな画像を机の上に散らばったポラロイド写真風にする「Polaroid Gallery」 - GIGAZINEを参考にして、使ってみた。⇒ 圏論勉強会の写真(Polaroid Gallery)

面白いけど、写真全体が見えるように縮小してくれたりとかはしないようなので、こういう目的には使えなさそうだ。

λ. 推移閉包は一階述語論理では表現できないのね

先日の「SPASSで知識の論理を使って論理パズルを解く?」についてちと考えていて、共通認識を扱う知識論理を一階述語論理に翻訳するには推移閉包(transitive closure)を表現する必要があることに気付いた。 それ自体はここではどうでも良いのだけど、どうにも推移閉包をうまく表現できなくて困った。

例えば、TがRの推移閉包であることを表すには「∀x,y. (T(x,y) ⇔ (R(x,y) ∨ (∃z. R(x,z)∧T(z,y))))」のような公理では不十分で、これだと最小不動点以外の解を排除できないため、「有限回のRで到達可能」ということをちゃんと表せていない。うーむ。

検索してみると、一階述語論理で推移閉包を表現できないというのは随分有名な話だったようだ。知らなかった……orz　しかし、こないだの「整礎性は一階述語論理では表現できないのね」といい、一階述語論理の表現力って僕が漠然と思っていたよりも、ずいぶんと限定されたものなのだな。

λ. Wellfounded induction in Agda2

Coqの整礎帰納法(Wellfounded induction)はどうやって実現されているのか見てみたら、accessibility predicate を定義して、それに対する通常の帰納法になっているようだった。 なるほど、整礎帰納法は accessibility predicate に関する通常の帰納法になってしまうのね。面白い。 Coqはまだ良くわからないので、とりあえずAgda2で似たようなもの(?)を書いてみる。

Rel : Set -> Set1
Rel X = X -> X -> Set

-- The accessibility predicate
data Acc {X : Set} (_<_ : Rel X) (x : X) : Set where 
  AccIntro : ((y : X) -> y < x -> Acc _<_ y) -> Acc _<_ x

-- A relation is wellfounded if every element is accessible
Wellfounded : {X : Set} -> (R : Rel X) -> Set
Wellfounded {X} R = (x : X) -> Acc R x

-- Wellfounded induction
wInd : {X : Set} -> {_<_ : Rel X} -> (wf : Wellfounded _<_) ->
       {P : X -> Set} ->
       ((x : X) -> ((y : X) -> y < x -> P y) -> P x) ->
       (x : X) -> P x
wInd {X} {_<_} wf {P} F x = f x (wf x)
  where
    f : (x : X) -> (Acc _<_ x) -> P x
    f x (AccIntro ch) = F x (\y r -> f y (ch y r))

これを length (filter p xs) ≦ length xs の証明 と組み合わせると、ようやく停止性の証明されたクイックソートが書けそうw

あと、一階述語論理と違ってCoqやAgdaで整礎性を表現できるのは、単なる不動点ではなく最小不動点を定義できるからか。一階述語論理の「Acc(x) ⇔ ∀y. y < x → Acc(y)」だと最小不動点であることを表現できないのが問題になる。

関連

• 整礎性は一階述語論理では表現できないのね - ヒビルテ(2007-12-05)

λ. 「Coqで“無限オブ無限”」のyoshihiroさんによる証明

先日のCoqで“無限オブ無限”で書いたCoqのコードが題意を満たすことを、にわとり小屋でのプログラミング日記のyoshihiro503さんが証明してくれました。ありがとうございます。
⇒ Coqで”無限オブ無限”(証明部分)

これは圧巻。面倒そうだとは思っていたものの、なんと500行もの証明に。 ……自分でやらなくて正解だったかも(苦笑

Coqを知らない人はこれを見て何が何だか分からないと思うけど、CoqIDEに読み込ませてステップ実行*1させていくと、ゴールがどう変形されていくかが分かって、何をやってるかが分るはず。といっても、僕もまだ全部はとても理解できていないけど。

λ. malloc-free な C 言語はチューリング完全

ku-ma-meさんが「malloc-free な C 言語はチューリング完全か」と書いていた。そこでku-ma-meさんも「再帰をうまく使えばできるのかな」と書いているけど、再帰を使って全部スタック上に確保してしまえば良さそうだ。 ヒープがないならスタックを使えばいいじゃない

Brainf*ck

とりあえず、メモリが有界でないBrainf*ckが実装できればチューリング完全だと思うので、実装してみた。

#include <stdio.h>

struct cell {
    struct cell *prev, *next;
    unsigned char value;
};

static void
f(const char *pc, struct cell *p)
{
    struct cell c = { .prev=p, .next=NULL, .value=0 };
    if (p) p->next = &c;
    p = &c;

    while (1)
        switch (*pc++) {
        case '\0': return;
        case '>':
            if (p->next)
                p = p->next;
            else
                return f(pc, p);
            break;
        case '<': p = p->prev; break;
        case '+': p->value++; break;
        case '-': p->value--; break;
        case '.': putchar(p->value); break;
        case ',': p->value = getchar(); break;
        case '[':
            if (!p->value) {
                int lv=1;
                while (lv)
                    switch (*pc++) {
                    case '[': lv++; break;
                    case ']': lv--; break;
                    }
            }
            break;
        case ']':
            {
                int lv=1;
                pc-=2;
                while (lv)
                    switch (*pc--) {
                    case '[': lv--; break;
                    case ']': lv++; break;
                    }
                pc++;
            }
            break;
        }
}

void brainfuck(const char *prog){ f(prog, NULL); }

実行用のコード。

#include <glib.h>
#include <stdio.h>
#include <locale.h>

int main(int argc, char **argv)
{
    GError *err = NULL;
    gchar *prog;
    setlocale(LC_ALL, "");
    g_file_get_contents(argv[1], &prog, NULL, &err);
    if (err) {
        puts(g_locale_from_utf8(err->message, -1, NULL, NULL, NULL));
        return 1;
    } else {
        brainfuck(prog);
        return 0;
    }
}

プログラムを読み込む処理は本質的ではないため、今回はプログラムの読み込み自体はmalloc-freeにはしなかった。というのも、読み込み処理をわざわざCで書かなくても、プログラムを既存の「brainf*ck自身で書かれたbrainf*ck処理系」に固定してしまえば済む話なので。

一般化?

ってか、つきつめて考えると、今のCならプログラムをCPS変換wして、以下のような関数を使えば良いか。しょーもないオチだけど。

void malloc_cps(size_t n, void (*k)(void*, void*), void *user_data)
{
    unsigned char a[n];
    k(a, user_data);
}

λ. RHG読書会::東京 Practical Common Lisp

.

λ. Thinkpad X61 を注文

元々、次のラップトップはレッツノートプレミアムエディションが欲しかったのだけど、Lenovo がクリスマスセールとして Thinkpad X61 を¥119,910円からの値段で売っていて、レッツノートプレミアムエディションの¥268,000からと比べて圧倒的に安かったので、こっちを注文してしまった。3年拡張クーリエサービスとあわせて¥130,410。 メモリは1GBのモデルにしておいて、自分で2GB増設する予定。

これまでずっとレッツノートを使っていたので色々と不安もあるが、Thinkpadは評判も良いし、まあ何とかなるだろう。

λ. 福岡伸一『生物と無生物のあいだ』

生物と無生物のあいだ (講談社現代新書)(福岡 伸一) を読んだ。 ogijunさんの紹介<URL:http://d.hatena.ne.jp/ogijun/20070714/p1>を見て読みたくなったのだけど、図書館で予約したら今頃になってしまった。

λ. ガルベスアドベンチャー

小太郎ゲーム オンライン:赤ちゃんガルベスが冒険するガルベスアドベンチャー 【日本語版】 を遊ぶ。 デビルエンドが難しかった。

λ. 円定期1年もの　金利1.2%キャンペーン

住信SBIネット銀行が円定期1年もの金利1.2%キャンペーンというキャンペーンをやっている。今募集している利付国債(5年)*1が年1.1%(税引後 年0.88%)しかないのに、年1.2%(税引後 年0.96%)の定期預金というのは素晴らしいね。 E*TRADEの口座を持っていれば、ネット上だけで口座を作れるようなので、ちょっと預けてみようと思う。

【追記】 新生銀行も冬の特別円定期として年1.1%(税引き後0.88%)というのをやっているな。また、500万以上預けるとプラチナ円定期となり、年1.2%(税引き後0.96%)になるようだ。 結構、こういうキャンペーンをやっているところはあるのね。

λ. S5のS4への埋め込み

[Coq-Club] Theorem Prover for Modal Logic S5 に「Formula A is a theorem of S5 iff formula <>[]A is a theorem of S4」と書いてあった。どうやって証明するのかしばらく悩んでしまったのだけど、ヒルベルト流の証明を考えて、証明の構造に関する帰納法で証明出来ることを確認した。ヒルベルト流は色々と面倒なので、証明できることを確認しただけで実際に証明はしていないけど。

λ. “Mechanizing common knowledge logic using COQ” by Pierre Lescanne

Coqの上で共通認識論理を形式化して色々する話。こういうのはとっくにやりつくされている話だと思っていたが、案外そうでもないらしい。

ヒルベルト流の共通認識論理を深い符号化法(deep embedding)でCoqに埋め込む。作る体系は普通のものではなくてCoqのパワーを生かしたもので、高階述語論理になってるし、論理結合子も→と∀を使ったチャーチエンコーディングで表現するようになっている。

共通認識論理の紹介としても分かりやすい。 ただ、最大不動点に関する話は、A→BのときAがBよりも大きいとしていて変な気がする。 共通認識様相を特徴付ける推論規則として、⊢ φ→ψ∧E_G(φ) から ⊢ φ→C_G(ψ) を導く推論規則があって、これは一種の余帰納法(coinduction)なのだから、A→BのときAよりもBが大きいとすべきだと思うが。

The muddy children という問題について、これを使って実際に証明をしている。ただ、専用のTacticsはまだ用意していない。

また、三賢者と帽子のパズルを例に、共通認識様相が実際には必要ない場合についての説明があった。「⊢ 仮定→結果」の形で示す場合には仮定に共通認識の様相が必要になるが、「事実 ⊢ 結果」の形で示す場合には事実には共通認識様相は不要*1。先日、SPASSで知識の論理を使って論理パズルを解く?で書いた話がまさにこれに当てはまっていて、うわっと思った。

あと、「Epistemic logic is usually mechanized by model checking」と書かれていて、Needham-Schroeder Public-Key Protocol の話が参照されていた。この話はモデル検査では有名な話だけど、知識論理と関係があるとは知らなかった。

それから、この論文とは直接の関係はないけど、ytbさんが知識様相論理をAgda2上に実装しているそうなので、どんな感じになるのか少し気になるのだった。

λ. ddとダブルバッファリング(?)

ふと、「ddは読み込みと書き込みを別スレッドに分けて、ダブルバッファリングのようなことをしているのだろうか」というのが気になり、GNU　coreutils のソースを確認してみたが、特にそんなことは無いようだ。

λ. かも鍋

λ. SATCHMOで遊ぶ

先日の渕一博記念コロキウム『論理と推論技術：四半世紀の展開』での長谷川隆三氏の発表『モデル生成型定理証明系MGTPの要素技術』(スライド)で紹介されていたSATCHMOで少し遊んでみる。 これは節集合のモデルを作ることで、充足可能性を証明するのだとか。なので、当然、証明したい論理式の否定を与えてモデルが存在しないことを確認すれば、その論理式が恒真であることがわかるので、定理証明機として使うことが出来ると。

スライドで紹介されていたソースコードそのままだと SWI Prolog に怒られてしまったので、演算子の優先順位とあと動的に変化する述語をdynamicディレクティブで指示するようにしておく。

% satchmo.pl
:- op(1200, xfy, '--->').
:- dynamic false/0.

satisfiable :- is_violated(C), !, satisfy(C), satisfiable.
satisfiable.

is_violated(C) :- (A--->C), call(A), not(C).

satisfy(C) :- component(X,C), asserta(X),
              on_backtracking(retract(X)),
              not(false).

component(X,(Y;Z)) :- !, (X=Y; component(X,Z)).
component(X,X).

on_backtracking(_).
on_backtracking(X) :- call(X), !, fail.

しかし、トリッキーだなぁ。 Prologはこういうのが書けるのが楽しい。

問題S1

まずはスライドにあった問題S1。 Prologと同じで「,」がandで「;」がorを表している。

% s1.pl
:- dynamic p/1, q/1, r/1, s/1.

true ---> p(a); q(b).
q(X) ---> s(f(X)).
r(X) ---> s(X).
p(X) ---> q(X); r(X).
p(X), s(X) ---> false.
q(X), s(Y) ---> false.

で、satchmoを呼び出して充足可能性をチェック。

?- consult(satchmo).
Yes
?- consult(s1).
Yes
?- satisfiable.
No
?- 

うん、ちゃんと充足不可能なことを示してくれた。

モデルが存在する例

次はちゃんとモデルが存在する例を試してみる。

% hoge.pl
:- dynamic p/1, q/1.

true ---> p(x); q(x).
p(X) ---> false.
q(X) ---> q(X).

実行。

?- consult(satchmo).
Yes
?- consult(hoge).  
Yes
?- satisfiable.  
Yes

というわけで、充足可能なことが分かったので、今度はlistingを使ってPrologのデータベース中の述語を表示してモデルを調べてみる。

?- listing.
(略)
:- dynamic q/1.
q(x).
(略)

値域限定

色々と試していたら、satisfiableはNoになって欲しい節集合で、試したらYesになってしまったものがあって、どうしてなのか少し悩んでしまった。 原因は、SATCHMOの仮定している値域限定「節の結論部に現れる変数は仮定部にも現れなくてはならない」という制約に違反してしまっていたからだった。 なるほど、なるほど。

λ. お菓子を少し買い込んでみた

λ. OCaml-Nagoya の人たちと飲み会

OCaml-Nagoya の人たちとの飲み会に参加。

関連

• OCaml-Nagoya の人たちと飲み会 - まめめも

λ. 岩明均 『ヒストリエ (1)』

p.24でアリストテレスが「大地の大きさについてある数学者は周囲40万スタディア(約7万2千キロメートル)と算出したのだが……私はもっと小さいのではないかと考えている」と言っててちょっと気になったのだけど、この「ある数学者」というのは誰のことだろう?

Big Bang: The Origin of the Universe (P.S.)(Simon Singh) の p.13 には「The feat of measureing the size of the Earth was first accomplished by Eratosthenes, born in about 276 BC in Cyrene, in modern-day Libya.」とあったが、ヒストリエでアリストテレスが喋っているのは紀元前343年なので、エラトステネスはまだ生まれてもいなかったし、それにエラトステネスの概算は40万スタディアではなく25万スタディアだった。

λ. MyMiniCity

なんか、みんなやってるみたいなので、私も始めてみた。 まだ人口が一人しかいない(笑

<URL:http://adjunction.myminicity.com/>

追記

24人まで増えた。

λ. クリスマスケーキ

λ. FF6懐かしいなぁ

たまたま、ニコニコ動画(RC2)‐ＦＦ６　妖星乱舞をみて感動する。 エレクトーンでここまで再現できるのね。 すごいなぁ。

これを観てたらFF6が懐かしくて仕方なくなって、検索してて見つかった FINAL FANTASY VI - Vain Dream, Hazy Memory という小説を読みふける。

λ. ローソンで Edy! キャンペーン

「今ならローソンでのEdy2,000円分の利用またはチャージで、ソニー“ウォークマン”を抽選でプレゼント！」とのことなので、今Edyへのチャージでポイントの付くクレジットカードを持っていないこともあり、一応¥2000だけチャージしてみた。

【追記】 まあ、当選しなかったけどさ。

λ. HaskellでCYK法

文脈自由文法のパーサーの最も効率の良いアルゴリズムの一つとしてCYK法(CYK algorithm)があるのだけど、これまでどういうアルゴリズムか知らなかったので、ちょっと調べてHaskellで素朴に書いてみた。 手続き型言語で書くとテーブルをボトムアップに作る手順が肝になるが、Haskellだと順序を気にせず再帰的にテーブルを定義するだけで良い。

import Data.Array

type S = N
type N = Int
data Prod t = T t | !N :++ !N
type Rules t = Array N [Prod t]
type Table = Array Int (Array Int (Array N Bool))

parse :: Eq t => Rules t -> S -> [t] -> Bool
parse rules s xs = table ! 0 ! (n-1) ! s
  where
    n = length xs
    table = mkTable rules (listArray (0, n-1) xs)

mkTable :: Eq t => Rules t -> Array Int t -> Table
mkTable rules ary = seq rules $ table
  where
    table =
      mkA lb ub $ \i ->
      mkA i  ub $ \j ->
      flip fmap rules $ \ps -> or $ do
        p <- ps
        case p of
          T t ->
              [i==j && t==ary!i]
          n1 :++ n2 ->
              [lookup i k n1 && lookup (k+1) j n2 | k <- [i..j-1]]
    (lb, ub) = bounds ary
    lookup i j n = table ! i ! j ! n
    mkA i j f = listArray (i,j) [f x | x <- range (i,j)]

で、適当な例で試す。

plus = 0
mult = 1
lpar = 2
rpar = 3
expr = 4
factor = 5
plus_expr = 6
mult_factor = 7
expr_rpar = 8

rules :: Rules String
rules = array (0, 8) 
    [ (expr,   num ++ [lpar :++ expr_rpar, factor :++ mult_factor, expr :++ plus_expr])
    , (factor, num ++ [lpar :++ expr_rpar, factor :++ mult_factor])
    , (plus_expr, [plus :++ expr])
    , (mult_factor, [mult :++ factor])
    , (expr_rpar, [expr :++ rpar])
    , (plus, [T "+"])
    , (mult, [T "*"])
    , (lpar, [T "("])
    , (rpar, [T ")"])
    ]
    where
      num = [T (show i) | i <- [0..10]]

test = parse rules expr ["1", "*", "(", "2", "+", "3", ")"]

λ. コミケ

何やら不思議なパーティでコミケへ。

• 入手したもの
  • 「くろいブラウスのあのこ」 (平均律)
  • 「東方文鳥録　〜Return Reanimateness〜」 (文鳥オンライン)
  • 「珍しい物を食べる会　珍味ミシュラン(山手線西側編)」「珍しい物を食べる会　珍味ミシュラン(山手線東側編)」 (mixi:「珍しい物を食べる会」)
  • 「青少年言説 WORKS - 後藤和智の仕事 2006〜2007」
  • 「暗黒団　計算機まとめノート　Linux上でのアセンブラ」「複素代数幾何初級検定・問題3とその解答」「最短距離のC言語」 (暗黒通信団)
  • 「Spファイル vol.5」 (Spファイル友の会)
  • 「THROW LINE」 (PASTA'S ESTAB)
• 入手できなかったもの
  • 全方位スクロール物量系アブストラクト系シューティング「exception」 (i-saintさん)
  • 「風 - KAZE -」 (SOUND HOILC)
  • 「コープスパーティブラッドカバー1」
  • 「うみねこのなく頃に episode 2」 (07th expansion)
  • 幺樂団の歴史4「東方夢時空　〜 Pantasmagria of Dim.Dream」, 幺樂団の歴史5「東方靈異伝　〜 Highly Responsive to Prayers」 (上海アリス幻樂団)
  • …

λ. 忘年会