日々の流転

λ. ようやく近代思想のレポートを書き上げた。しっかし、2日間徹夜してまで書いた内容がこれかと思うと愕然とするよ。しかし、まあ、書くものは書いたんだ。まあ、いいや。いいのだ。

λ. 数学と論理の試験を受けた。100点取るべきような問題だったけど、「A∨¬AをNKまたはLKで証明せよ」という問題がわからなくて悔しかった。あと、不完全性定理の説明の問題で、「対角化定理」の語を使い残してしまったので、これも不味かったな。はぁ。

λ. 今日は、あと「デザイン言語総合講座」の試験を受けて、それから論理プログラミングのミニプロを仕上げて提出しなくちゃいけない。さぁ、頑張るぞ。

λ. 昼食

学食で、「ピラフの牛ソースかけ」と「キャベツとベーコンのコンソメスープ」。

λ. デザイン言語総合講座の試験

「持ち込み可」だと言うのをすっかり見落としてましたよ。さらに鞄に入っていると思ってた資料は入ってないし、絶体絶命のピーンチ!!

…だったんだけど、偶然知合いに会って、彼女の機転で九死に一生を得ました。本当に感謝感謝。

λ. とはいえ、論述問題が散々な出来だった。いつもの事だけど、時間無さ過ぎ。はぁ。

頭の中で考えがまとまってて、書き出すのに手間取ってるので、やはり手先の器用度をアップして、4倍速くらいで書き出せるようにしたい。

λ. 人間と法 テスト

これで評価されるというのもどうかと思うけど、まあ単位はくると思うので気にしないで次の課題に取り掛かろう。

1. 未成年者と疑われる人と取引きをする場合に注意すべき事を書きなさい。
2. 以下の言葉について説明しなさい。
   • 「立証(挙証)責任」
   • 「無効と取消し」
   • 「法人擬制説」

λ. 逃避活動: esecpl.hs

こないだは慣れない言語で慣れないものを書いて失敗してしまった。このprのインターフェースには無駄がある。これを書き直して……とかやっているうちに全然別の方向に行ってしまった。それにしてもHaskellらしくなさ過ぎ。

esecpl.hs

λ. バイト

shiftという所でバイトすることに。

λ. Central-European Functional Programming School

Varmo Vene: Signals and Comonads に興味があったのだけど、この講義の資料は公開されてないっぽいな。残念。……と思ったら、あった。Interp.tgz に含まれてるのか。後で読んでみよう。

Varmo Vene: Signals and Comonads

「fby」は「followed by」の略で、「wvr」は「whenever」の略らしい。 ストリームを利用したプログラミングではよく出てくる演算子らしいけど、知らなくて最初何かと思った。

(2005-09-29 追記) 会場では Tarmo Uustalu1 and Varmo Vene. The Essence of Dataflow Programming (LtU) が資料として配布されていたそうで、そっちにはかなり詳しく書いてあった。面白い。

λ. るびま 0008 号

「おすすめのライブラリ」の話だけど、tsortはopen-uriやppほどじゃないけど何度か使ったことがある。少なくとも、resolve.rbよりは使ってる。

trapの話は知らかった。キャンセレーションポイントといえば Thread#kill や Thread#raise といったメソッドの問題をまず想像した。ちなみに、これは今非常によろしくなくて、例えばensureの中で実行がキャンセルされると悲惨なことに成りえる(e.g. [ruby-dev:23619])。[ruby-dev:23619]の問題に限って言えば、Mutex や ConditionalVariable をCで実装すれば解決できるのだけど、この問題の本質はRubyのスレッド/同期のプリミティブが compositionality を欠いているということなのだと思う。

それと、「だいたい、アプリケーションて 2 種類あると思うんですよ。IO をするスレッドというかプログラムと、計算をして黙り込んでいるプログラムがあると思うのですが、IO のほうは途中で止めるときは、自分でここは止まる可能性があると宣言するか、あるいはブロックするところで止まるのがいいのではないかと思うのですが。(中略) で、計算するほうはぷちっと殺してもいいことがありまして、それはそれでいきなり殺す、つまりキャンセレーションポイントを宣言しなくても殺せる意味で、この二つの使い方を両方サポートするにはどうしたらいいかということですかね」という点は興味深いな。

ちなみに、Haskellでは型によってIOアクションの実行と普通の計算を区別しているので、この問題には自然に対処出来ていると思う。IOアクションの実行に関しては普通にキャンセレーションポイントの概念を持っているのに対して、後者の普通の計算については(処理系的には)いつでもプチっと殺してしまえる。実際、STMモナド(see Composable memory transactions)では型によってIOアクションの実行が含まれないことが保障されているので、トランザクションに失敗した時点でプチっと実行をキャンセルして、後で再実行する。

「興味を持っているテーマ」のSQL(とRDB)のindexの話は面白いな。SQLのこうした発想は Data Structures Considered Harmful といった発想にも繋がっていたはず。(FIXME)

λ. 有限体GF(p)

ふと、有限体を扱うための簡単なライブラリが欲しくなったので、書いてみた(GF.hs)。有限体といっても、素体(prime field)だけで、拡大体(extension field)は扱えないけどね。

書いていて感じたのだけど、型クラスを compile-time prolog として使うと、本物の prolog との違いで結構はまるね。

それと、拡大体をこういうアプローチで扱うにはどうしたらよいのだろうか。原始多項式にどの既約多項式を使おうと結果は全て同型なわけで、既約多項式を明示するのは馬鹿らしい。標準的な既約多項式みたいなのはあるのだろうか?　そして拡大体の元の標準的な表記法はあるのだろうか?

【2008-04-29 追記】 どう書く？orgの「法演算」のお題にnobsunが同様の方法を使って答えていたので、このコードも転載してみた。

λ. 『陰陽ノ京(おんみょうノみやこ)』, 渡瀬 草一郎 (著), 田島 昭宇 (イラスト)

を読んだ。なかなか良く書けていると思った。

λ. 雑談メモ

• ホーン節に限定されない、一般のresolutionは色々難しい
  • ancestor resolution
  • factoring
  • Michael Genesereth
• Prolog based theorem proover
  • Mark E. Stickel
  • 対偶等を使ってPrologで扱える形に変換する前処理
  • 意味論の問題
  • 2008-03-27追記: SATCHMO等のことか?　⇒ SATCHMOで遊ぶ - ヒビルテ (2007-12-19)
  • 2008-05-25追記: いや、PTTP - Prolog Technology Theorem Proverのことか。
• model checking で幾何学の定理を証明?
• magic set
  • Magic sets and other strange ways to implement logic programs.
• magic set と chart parser ?
• Cocke-Younger-Kasami (CYK) algorithm
  • 2008-03-27追記: Haskellで書いてみた
• 『現代数理論理学入門』の強制法の解説はわかりやすいらしい

λ. 統計の本

某K氏に統計の本の紹介を頼んだら、この二冊を紹介された。 後で読みたい。

λ. 知識発見法レポート

先日読んだ Learning Minesweeper with Multirelational Learning に触発されて、数独で数字を埋めるための規則を学習させようとしてみたのだけど、残念ながらうまくいかなかった。

• 知識発見法レポート
• 背景知識 sudoku.b
• 正例 sudoku.f
• 負例 sudoku.n

λ. 君は修悦体を知っているか

スラッシュドット ジャパン | ガムテープによる独特なフォント「修悦体」 より。そういえば、見たことがある気がする。こうして見ると凄いな。

λ. 時をかける少女

テレビでやっていたので観た。 筒井康隆の小説とはぜんぜん違う話なのね(こっちも読んでないけど)。

λ. 日本Ruby会議2009 3日目

後で書く

ソケットライブラリの改善 / 田中 哲

寝坊してakrさんの最初の発表はだいぶ聞き逃してしまったが、あまった時間でやっていた、design decision を中心に説明する発表を聞くことが出来たので満足。 ソケット自体の話はあまりよくわかっていないのだけど、design decision の話はとても面白かった。 「inspect可能 = 意味がオブジェクト内で決まる」で何をオブジェクトにすべきかというのに関係している、という観点や、「Ruby が知らないオプションがあるかもしれないので、オプション毎のサブクラスは作らない」という話、それから「Best name should be best behavior」など。あと、「It is wrong if Ruby is harder than C」とか「知らないところにきいても仕方ない。Rubyのことはまつもとさんに」に笑った。

• 天泣記(2009-07-19)

スクリプト言語Ruby / arton

.

あらためて仕事で使うRuby / 後藤 謙太郎

.

Ruby製アプリケーションを配布するn個の方法 / 原 悠

今Rubyの仕様を書いているそうで。多重代入のカンマとか、よくわかんなかったら隣の人(matz)に聞くとか。Rubyを実行ファイル化する方法は、RubyScript2Exe, Exerb, Ocra, Crate と結構色々あったんだねぇ。Crateのスクリプトをsqliteのデータベースにしてそれも実行ファイルにくっつけるというのは、けっこうきもいと思った。

tDiary の Ruby 1.9 対応の過程と今後のロードマップ / 柴田 博志

.

Haml and Sass: Solution for you who get tired of ugly markup / 浦嶌 啓太

.

Take the Red Pill / 角谷 信太郎

角谷さんは運営委員長。実行委員長は高橋さんで、よくないことがあったら謝る人は高橋さん。青いピルを選べば、何もかも今までどおり。「会社に戻ってXMLエンタープライズ」　赤いピルを選べば「welcome to real world」。Rubyは無名の質を備えたプログラミング言語。

基調講演: Rubyと私、そして日本Rubyの会 / 高橋 征義

.

夕食はアボカフェというところで、アボガド丼などを。 アボガドとSPAMはよく合うなぁ。