日々の流転

λ. ファイト　テロリズム

小泉内閣メールマガジン(2001/09/27)で、「ファイト　テロリズム」とか書かれててびびった。…たしかにwith/againstを入れない事もあるけど……ねぇ?

λ. 朝鮮語辞典

を買った。¥7,770なり。うぅ…、高い。

λ. 情報数学Ⅰ

参考文献/資料としてあげられているこの本は入手可能なのだろうか。

J.E. Hopcroft and J.D. Ullman. Formal Languages and their Relation to Automata. Addison-Wesley, Reading, Mass, 1969. 野崎他訳で, サイエンス社より「言語理論とオートマトン」として邦訳あり.

λ. 帰納論理プログラミング

院の講座だけあってついて行く自信ないなぁ。古川先生には「まだまだ時間はあるんだから、来年にしたら?」と言われてるし、来年の春学期に「情報数学Ⅱ」と「データマイニング法A」の授業を取れば、確かに秋にはちょうど良さげかも。どうしたものだろう。…やっぱ、来年にするか。

λ. 萩野研

なんか、なりゆきでRubyについて発表するはめになりそう。まだ取るかどうかも決めてないのにぃ。…いいのかなぁ。

λ. 読んだコミックス

サイレント・メビウス SIDE4

サイレント・メビウス SIDE5

サイレント・メビウス SIDE6

麻宮騎亜

λ. 人間の天敵はいつ開発が完了するだろう。

「ルドラの秘宝」みたい……

λ. Symmetric Haskell

今考えてること。

• Symmetric ML のアイディアをHaskellに対して適用してみる。 つまり、co-dataを通常のdataと同様に(対称的に)定義できるように文法を拡張する。
• ここで扱うco-dataはrecordによって表現できるはず。
• 拡張された文法からHakell98へのトランスレータを作成出来るか?
• 特にco-dataに対するパターンマッチングを用いた関数定義は翻訳できるか?
• Symmetric ML ではlazynessが問題になったが、 Haskellは最初からlazyなので、その辺りはシンプルになるはず。

試しに書いてみると、こんな感じか? 対称的なのは美しいかも知れないけど、全然面白くないなぁ……

codata (a,b) = Fst :: a & Snd :: b
 
pair :: a->b->(a,b)
pair a b = merge
             Fst <- a
             Snd <- b
 
codata InfList a = Head :: a & Tail :: InfList a
 
comb :: InfList a -> InfList a -> InfList a
comb l1 l2 = merge
               Head <- Head l1
               Tail <- comb l2 (Tail l1)
 
-- combの別の定義方法
Head (comb l1 l2) = Head l1
Tail (comb l1 l2) = comb l2 (Tail l1)

λ. 傘

また傘を盗られてしまった。少しの間とはいえあんな所に傘を置いてしまった僕の不注意なのだが、やはり腹が立つ。傘を盗むなんて最大級に卑劣な犯罪ですヨ。犯人は、良心の欠片もない卑劣な人間に違いない!

λ. 今日の向井研

新しい人が二人ほど来た。

ふむ「点の無い幾何学」か。

春学期はみんなバラバラの事をやってて、他人の発表にはついていけていなかったので、今期は何か共通のこともやりたいし、Topology via Logic を輪講するというのも悪くないと思うんだけどなぁ……

向井先生に『プログラム意味論』という本が教科書としてバランス良く丁寧に書かれていると聞いた。ラムダ計算や圏論、それにdomain theoryについても扱っているらしい。

λ. 借りた本

Intuitionistic Type Theory

P. Martin-Löf.

λ. 疲れたよ。

λ. 借りた本

『グリーン・マイル(3) - コーフィの手』

スティーヴン キング (Stephen King) [著], 白石 朗 [訳]

『ハンニバル (上)』

トマス ハリス (Thomas Harris) [著], 高見 浩 [訳]

λ. readFile / writeFile

readFileとwriteFileを使ってファイルを書き直すようなコード(ちょー単純化すると以下のような感じ)を書いたら、期待通りに動かなかった。理由は理解できるのだけど、これはちょっと切ないぞ。

main =
    do s <- readFile "test.txt"
       writeFile "test.txt" (s ++ "hogehoge\n")

λ. 踊る大捜査線 The Movie 2

takotセソセイにフジサワ中央の夕方が安いと教えてもらったので、せっかくだから家族で見に行ってきた。これでようやく元ネタがわかったYO。で、面白かったとは思うけど、リピーター続出ってのはちょっと信じられんな。

λ. 今日から授業開始。

λ. 東方永夜抄のスペルカード取得率

スペルプラクティスで取得/挑戦可能/総数が199/207/222。残りは6Aの禁薬「蓬莱の薬」のHardとLunatic、6BのLuntatic全部、Extraの「インペリシャブルシューティング」、それに Last Word が半分くらいか……。いまだに「深弾幕結界　-夢幻泡影-」を見れねぇ。

λ. 本宮ひろしと集英社に抗議を！！

ヤングジャンプで連載中の「国が燃える」での南京事件の過激な誇張に抗議しようって話。フィクションとはいえ、私もこの描写はあまりに酷いと思う。

λ. Epigram

Epigram is a dependently typed programming language and an interactive programming environment. Epigram has got a type system which is strong enough to express the behaviour of programs, the type checker then guarantees that the program is well behaved. However, you don't have to go as far, you can write ordinary programs and refactor them into more trustworthy, formally checked deliverables -- Epigram supports a pay as you go approach to formal methods.

Epigram is a dependently typed functional programming language.って事で少し興味をひかれる。誰か使ったことあるひといない?

【2006-04-22 追記】 xemacsが必要なのと、自然演繹のスタイルでプログラムを書かなくてはいけないのが、ちょっと嫌かも。

関連エントリ

• 型を返す関数
• Why Dependent Types Matter
• Epilogue for Epigram

リンク

• Wikipedia: Epigram programming language

λ. Alloy Analyzer

The Alloy Analyzer is a tool developed by the Software Design Group for analyzing models written in Alloy, a simple structural modeling language based on first-order logic. The tool can generate instances of invariants, simulate the execution of operations (even those defined implicitly), and check user-specified properties of a model. Alloy and its analyzer have been used primarily to explore abstract software designs. Its use in analyzing code for conformance to a specification and as an automatic test case generator are being investigated in ongoing research projects.

MISE EN PAGES | alloy - the model analyzer より。面白そう。

λ. 第 336 回 PTT 「仮想マシンを利用したプログラムの実行の監視とそのデバッガへの応用」

久しぶりにPTTに参加。 そして、初めて矢上に来た(慶應に6年もいて矢上に来るのが初めてというのもどうかと思うが)。

以下、簡単なメモ。

背景

伝統的なデバッガが共通して持つ機能は、ブレークポイント、ステップ実行、変数の値の調査等だが、これだけでは大規模で複雑なプログラムのデバッグには不十分。逆実行や、不具合に関係のある部分を抽出するスライシングの機能が必要。

仮想マシンの概観

• コード変換エンジン
  • 動的な instrumentation を用いながら個々のスレッドを実行する
• スレッドシステム
  • スレッドスケジューリングや Pthread API のエミュレートを行う
  • 実装は GNU Pth を基にした
  • GNU Pth はプリエンプションには対応していないが、 コード切り替えを起こすようなコードを dynamic instrumentation で埋め込むことで対応

コード変換

• 監視コードの挿入
  • デバッガ側の要求に従い、イベントに対応するハンドラを呼ぶ
    • イベント : デバッガの監視する挙動 (e.g. メモリの読み書き)
    • ハンドラ : C言語で記述された関数
• 分岐先の変更
  • 本来の分岐先に分岐せず、仮想マシンに制御を戻す

主な監視対象

• 基本的なもの
  • メモリの読み書き、レジスタの読み書き、分岐、関数の呼び出し、復帰、システムコール
• マルチスレッドに関連したもの
  • スレッドの作成・終了・コンテキストスイッチ・排他制御

実行の記録・再生

• 全く同じプログラムでも、実行するたびに結果が変わってしまうことがある(プログラムの実行の非決定性)
• デバッグを行う際に大きな問題となる
• ⇒ 仮想マシンに実行を記録・再生する機能を導入
  • 非決定性の要因となる振る舞いを記録・再生する (e.g. システムコール、シグナル、コンテキストスイッチ)

スライシング

• Dynamic Data Slicing
  • Forward Computation という手法を用いる
• Dynamic Data Slicing
  • 動的な依存関係を分析 (def-use chain)
• Forward Computatin
  • プログラムの実行と同時に、並行してスライスを計算する
  • backward computation に比較して消費するメモリ量が少ない

可逆実行

• ロギング方式[Chen01]と再実行方式[Boothe00]がある。
  • ロギング方式　実行時に状態履歴を保存し、後に復元
    • e.g. メモリ変更時に、変更前の内容を保存しておく
  • 再実行方式 : プログラムを先頭から再実行する
    • 適切な時点で停止させることにより、擬似的な逆実行を実現
• ロギング方式の特徴
  • 利点: 単距離の逆実行は比較的高速
  • 欠点: ログ取得のコストが大きい。マルチスレッドには対応しづらい (終了したスレッドを復元したりする必要)
• 再実行方式の特徴
  • 利点: 実装が比較的容易、ログ取得のコストもない
  • 欠点: 逆実行に時間がかかる場合がある
• 両方実装したが、スレッドを使う場合には再実行方式のみ。

追記

丁度、先日 Google Japan Blog: Debugging Backwards in Time - Google Tech Talk 紹介シリーズ ( 2 ) に逆実行出来るJavaデバッガの話が出ていた。

λ. 松下、web限定「Let'snote プレミアムエディション」は250GB HDD＆ターボメモリー搭載ジェットブラックモデル

これ欲しいなぁ。

λ. 『寄生獣 (6)』 by 岩明 均

を読んだ。

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

第22章「黒帯のためのLISP」と第23章「実践：スパムフィルタ」。

λ. CPLに関数定義を導入

CPLのHaskell実装に久しぶりに手を入れて、関数定義を導入した。 これで、

let uncurry(f) = eval . prod(f, I)

とか

let primrec(f,g) = pi2.pr(pair(0,f), pair(s.pi1, g))
let fact = primrec(s.0, mult.prod(s,I))

とか、書けるようになった。

あとはIOをどうにかして導入すれば、変態言語として使えるようになるかな。 しかし、久しぶりにソースをいじると、昔の自分のコードがひどすぎて、一から書き直したくなるなぁ。

λ. 焼肉

大学時代からの友人と焼肉など。 肉の万世に多分初めて行った。