2001-06-17
λ. Gimp-Ruby
Apollo IRBからパクらせてもらったので、コンソールが一応使えるようになりました。なんとなく嬉しいので、今日中に新しいバージョンを公開します。ただ、なんか色々挙動がおかしい気がしますが。
ちゅうわけで、リリース。registry.gimp.orgにも登録。さて、湘南の文化祭に行ってこよ。
2002-06-17
λ. うぅ。時間がねぇ。
λ. 『夢使い (1)』 植芝 理一
久しぶりに絵に惚れた
λ. 論文読み会 "Clarifying the Fundamentals of HTTP" by Jeffrey C.Mogul, Compaq Research, IETF HTTP WG
以前にRFC2068を読んだときはEntityの概念がイマイチ理解できなかったのだけど、この発表を聞いてその辺りがすっきりしたので、気持ち良い。
2003-06-17
λ. ドイツ語
藁谷先生は面白いなぁ。
λ. 萩野服部研
SICP 5.1 「レジスタ計算機の設計」
λ. [a1; a2...; an] と[b1; b2...; bn] を受け取って, [(a1, bn); (a2, bn - 1); ...; (an, b1)] を返す関数
水凪さんの日記の4/17に載っていた問題。帰りの電車とバスの中で結構真剣に考えてしまった。気づけば簡単。
長さの等しい二つのリスト[a1; a2...; an]と [b1; b2...; bn]を 受け取って, [(a1, bn); (a2, bn - 1); ...; (an, b1)] を返す関数を書きなさい。 ただし、
- nをあらかじめ知ることはできない
- 与えられた二つのリスト以外のリストを使ってはならない
- 再帰呼び出しは高々(n + 1)回しか行ってはならない
- 全体の計算量はO(n)でなければならない
ψ nobsun [hoge :: [a] -> [b] -> [(a,b)] hoge as bs = zip as (reverse..]
ψ あおき [これでいいんですかね… xzip xs ys = f where (f,s) = xzip' xs ys xzi..]
ψ さかい [確かに問題が結構曖昧ですよね。 nobsunさんのは、zipとreverseはそれぞれn回の再帰で実行できるので、..]
ψ ささだ [Haskell ワカリマセーン．ruby か scheme で書いてー．]
ψ nobsun [あっ。なるほど。mapAccumR だ。 xzip as bs = snd $ xzip' as bs xzip' ..]
2006-06-17
λ. 発表練習
とても勉強になりました。 本当にありがとうございます。
λ. 『ふつうのHaskellプログラミング』読書会
第一部を読んだ。 p.26でIOアクションについて「アクションもHaskellの値ですが、不思議なことに、その値を評価すると入出力などが実行されます」と書かれているのが気持ち悪かった。それ以外はとても良く書けていた。
λ. reallyUnsafePtrEquality# :: a -> a -> GHC.Prim.Int#
GHC.Extsに reallyUnsafePtrEquality# :: a -> a -> GHC.Prim.Int# という素敵な関数を発見した。ただ、これは同じサンクであるかを比較するもので、例えばaとid aは同じとみなされない。さらに、id aをwhnfに簡約した後も同じとは見なされないようだ。実装を考えれば当然か。サンクのupdateにindirectionを使う場合なら、GCでindirectionが除去されることで同じになることもありそうな気がするが、どうだろう。
2007-06-17
λ. 『チェーザレ・ボルジアあるいは優雅なる冷酷』 by 塩野七生
先日『チェーザレ — 破壊の創造者』を読んで、チェーザレ・ボルジア(Cesare Borgia)についてもっと知ってみたくなって読んだ。時代を駆け抜けた英雄という感じだな。活躍が華々しい分だけ、その後の没落していく様には泣けるものがある。
2008-06-17
λ. コメントキーフィルタ＆プラグイン
最近、またコメントスパムがひどくなってきたので、コメントキーフィルタ＆プラグインを導入してみた。 最初は青木さんのパッチ(+ artonさんの携帯向けパッチ)にしようかと思ったのだけど、アップデート時のことを考えて、パッチを当てずに済むこっちにしてみた。
2010-06-17
λ. Whyでバブルソートの正当性を示す
計算機言語で定理証明 (Proof Party.JP)のときには、Jahobというツールを使って色々やってみたが、最近Whyという似たツールを知ったので、こっちでも同じようなことをやってみる。 まずは、Jahobでも試したバブルソートの例*1。
これを gwhy BubbleSort.java としてgwhyを起動すると、Proof Obligation が抽出されて一覧されるので、あとはメニューから「Proof」「Prove all obligations」とかを選べば定理証明器などが走って証明をしてくれる。
定理照明器としては、Alt-Ergoしかインストールしていなかったけれど、この例ではあっさり全 Proof Obligation が証明された。
以下が結果の画面。 gwhyのこのインターフェースはテストツールに似せてあるのだろうけど、良いなぁ。
![[gwhyのスクリーンショット]](./images/20100617_0.png)
参考
【2010-06-24追記】
マニュアルを一応読んで、異なる要素が保存されている事を追加してみた。 同じ要素の数が変化するかどうかは書けていない。 今度は Alto-Ergo では証明に失敗するのがあったので、CVC3も使ってみたら、片方ですべてを証明するのは無理だったけど、どちらかでは全部証明できた。
【2010-07-20追記】
要素の個数の保存についても書いてみたが、これは証明がタイムアウトしてしまい、うまくいっていない。
*1 事後条件としては、要素が保存されていることとかは置いておいて、実行後に配列がソートされていることだけを書いてある。
