2001-11-06
λ. 朝鮮語
中間テスト。敗北。
λ. 情報通信セキュリティ論
ブロック暗号とストリーム暗号について前回よりももうちょっとつっこんだ話。有限体上の演算とか面白い。しっかし、この「第3回講義メモで、アフィン暗号の式が E(M)＝aM＋b mod N、D(C)＝(C−b)/a mod N となっていますが、復号の方がうまくいきません。」ってFAQはレベル低すぎ。あと、「一年生の時にやったはず」とか言っちゃいかんですよ、せんせ。一年生だってこの授業取ってるんだから。
λ. データベース概論
正規化理論について。さっぱり分からなかったので後でメールで質問しよ。こないだの関係代数のときみたいに数学的な定義を書いてくれれば良かったのに。
λ. ruby_m17n vs TIS620&IS13194
TIS 640620 や IS 13194 のような、(文字ではなく)文字を構成する部品が符号化の単位になっているようなエンコーディングはどのように扱われるべきだろうか?
2002-11-06
λ. 夢
ミミック化した日記帳に襲われる夢。最後には食べられてしまった。バリバリ、ムシャムシャ……
λ. gtk+-2.0.7
いっちーさんのツッコミを見て gtk+-2.0.7がリリースされているのを知った。
λ. 過去
やり直したい過去、消し去りたい過去。目を覆いたくなる失態、穴があったら入りたくなるほど恥ずかしいこと、胸が痛くなること……。でも、そういった過去も、そうでない過去と分かちがたく現在の自分を構成しているのだと思う。
仮に人生をリセットして別の選択をすることが出来たとしても、それは自らのアイデンティティを決定的に損なうことなのではないのか?
λ. Plan9
自分のノートPCにインストールしようと思ったら、Plan9からCD-ROMドライブが認識されずインストールできなかった。
2003-11-06
λ. Gunslinger Girl
先週に続いて今週も録画するのを忘れる。欝だ。
λ. Coalgebras and Monads in Semantics of Java
を読んだ。これをRubyに応用するには何が必要だろう。あと、coalgebraって面白いかも、と今頃になって思った。
2004-11-06
λ. 238 盆地の村
ヴァルターとカタリナのペアを疑ってはいたんだけど、結局正解にたどり着くことは出来なかった。参加者じゃないけど、ちょっと悔しい。
λ. RHG読書会::東京 Reloaded
先月は行けなかったので、久しぶり。
2007-11-06
λ. “State of the Union: Type Inference via Craig Interpolation” by Ranjit Jhala, Rupak Majumdar and Ru-Gang Xu
- <URL:http://www.cse.ucsd.edu/~rjhala/papers/state_of_the_union.html>
- <URL:http://www.springerlink.com/content/h601x44p4379h410/>
<URL:http://fixedpoint.jp/2007/02/10/state_of_the_union.html> より。
Cの共用体は、どの型がいま共用体に格納されているかを覚えていないので、通常タグフィールドと組み合わされて利用される。ので、安全なアクセスであることを検証するために、共用体に対するアクセス時にタグフィールドに関する条件が成り立っていることを静的にチェックすることが考えられる。
条件はアノテーションとして与えることが考えられるけど、ここでは自動的に発見していて面白い。 どうやるかというと、共用体へのアクセスをコントロールフローグラフ(CFG)上で支配するような条件文を集めてきて、各型でアクセスするための条件はdisjointであるはずといった制約を仮定し、Craig Interpolation を使って条件を発見している。 実装は、Cのソースコードの操作やコントロールフローグラフの作成に CIL を、Craig Interpolation に FOCI を利用。
Craig Interpolation が何故こういうことに使えるのか、私はまだ理解できていないので、An interpolating theorem prover を読んでみたいところ。
2008-11-06
λ. Agda2での複数引数のパターンマッチと definitional equality の落とし穴
以下のような関数があったとする。
f : Bool -> Bool -> Bool f true true = true f _ _ = false
このとき、f false x と false の間には definitional equality は成り立つが、f x false と false の間には definitional equality は成り立たないのね。 例えば、以下のようなゴールはそのままではrefine出来ない。
test : forall x -> f x false ≡ false
test x = {! ≡-refl !} -- Oops!, can't refine!
パターンマッチは構文的には全ての引数に対して同時にパターンマッチしているかのように見えるが、実際には左の引数から順に1引数毎にしかパターンマッチしていなくて、どの節を用いるかが決定できていないということだろうか。 こうなっていることには何か理由はあるのだろうけど、非常に直観に反する振る舞いだと思った。
また、単に直観に反するだけでなく実際に困ることもあって、上の例のようなものを証明するときには、先行する全ての引数について場合わけして具体化しなくてはならない。 上の例であれば以下のようにすれば良いのだけど、これは引数の個数や構築子の種類が多い場合には非常に面倒だ。
test : forall x -> f x false ≡ false test true = ≡-refl test false = ≡-refl
2009-11-06
λ. 『プログラミングHaskell』 Graham Hutton (著), 山本 和彦 (訳)
翻訳のレビューに参加させて頂いていた、『プログラミングHaskell』を献本していただきました。
また、それに加えて10月に出版された『プログラミングのための確率統計』も献本していただいてしまいました。
この場を借りて御礼申し上げます。
これまで日本語で出版されていたHaskellの入門書の『ふつうのHaskellプログラミング―ふつうのプログラマのための関数型言語入門』や『入門Haskell―はじめて学ぶ関数型言語』といった本は、ちょっとしたツールやゲームやWikiといった日常的な題材を通じてHaskellの使い方を学ぶという感じだったが、この本はそういうアプローチの本ではなく、「Haskellプログラマはどのように考え、どのようなモノの捉え方をするのか」というのを、もっとダイレクトに教えてくれる本。
そういう意味では、最後の章がアプリケーションの実装等ではなく、『プログラムの論証』という章であるのは象徴的だと思う。
というわけで、手っ取り早くHaskellで何が出来るのかを知るには向いていないけど、Haskellの考え方を知るにはオススメ。また、長年授業で使われてきた講義資料が元になっているだけあって内容の構成も洗練されているし、翻訳の質も高いと思う。
λ. 『プログラミングのための確率統計』 平岡 和幸 (著), 堀 玄 (著)
『プログラミングHaskell』と併せて、10月に出版された『プログラミングのための確率統計』も献本して頂いてしまいました。
この本は『プログラミングのための線形代数』と同じ著者らの本で、『プログラミングのための線形代数』で目から鱗の連続だった身としては、読むのが非常に楽しみです。
ありがとうございました。
ψ たかはし [ruby_m17nの話ですが、UTF-8でも基本的に文字ユニット（部品） 単位で処理してるはずですから、TIS640..]
ψ kjana [そのへん内部コードと外部コードとの変換を自由に定義できるっていうのが ruby-m17n の考え方のベースなんで， ..]
ψ さかい [前述のエンコーディングは、部品の不定長の結合を許すので、エンコーディングをそのままにしたままで、文字単位の処理を行う..]
ψ たかはし [はうっ、TIS620でしたっけか。気づかずにすみません。 むむむ、確かに「どんな内部コードでもおーけー」という意味..]
ψ kjana [しまった．そっか，内部コードは stateless であること， っていう制限はありましたね，そう言えば．文字部品単..]
ψ さかい [部品単位から文字単位への変換は確かに面倒ではあるのですが、結合規則をきちんと形式的に定義できるならば、結合文字を含ん..]