2001-12-16
λ. Prologを作ろう! (2)
とりあえず最初の実装は捨てることになるだろうと割りきって、solveという名前の関数を再帰的に呼び出すだけの今の実装をもうちょっと進める。これでバックトラッキング出来るようになった。ad-hocに連言を実装してみた。この方法だとcutの実装も面倒そう。
……ってか、Prologなんか作ってる場合じゃなくて、データベース概論の宿題を進めなくちゃならんのに……全くの白紙状態。やばすぎー
2002-12-16
λ. コンパイラ構成論
課題その2が出た。TinyCのソースは以前にkjanaさんに紹介してもらって、簡単に目を通したことがあるので、TinyCの構造についてレポートするのが楽そう。だけど、やっぱり、CPLの処理系を作って見たいなぁ。
λ. 読書
- 『リストラ軍師大前鷹山』
- しりあがり 寿
λ. Jena
「プログラミング入門」の授業のテキストを読みながら、Jenaに触ってみる。
λ. 夕食
あろ〜むへ。パーティーは魔王豊ピーと愉快な仲間たち。
λ. 東方紅魔郷
今日はノーコンテニューで「レッドマジック」にまで到達したのに結局やられてしまった。ところで、「レッドマジック」って森博嗣の小説に出てくるOSと同じ名前ですね。
伏屋さんに、Extraでボム一個と一機を犠牲にしてパチュリーに擦りまくるというテク(?)を教えてもらう。
λ. 論文読み会 "Java バイトコードを編集するためのAPI"
Javassistの論文。
2006-12-16
λ. Deriving Structural Hylomorphisms From Recursive Definitions by Zhenjiang Hu, Hideya Iwasaki, Masato Takeichi
m-a-oさんも書いていたが、Warm Fusion と比べるとシンプルで良いな。
ただ、CPOで多項式関手の始代数が存在するとか言っている*1のが、ちと不安だけど。
ここで扱っている言語はネストした再帰呼び出しを含まない。そのためアッカーマン関数やたらいまわし関数のような関数は扱えない。
2007-08-28 追記
書くのを忘れていた*2が、Grant Malcolm の Data structures and program transformation を実際に確認。“Data structures and program transformation”ではデータ型を圏論的に特徴付けて promotion 等を扱っているが、CPO等の具体的な圏でそれらのデータ型や関手が存在するとは言っていない。 むしろ、それらのデータ型定義から自由生成される圏で議論をしていると考えるべきところだろう。 また、polynomial functors という言葉も使っていない。
なのでこの論文(Deriving Structural Hylomorphisms From Recursive Definitions)での、「Thrughout this paper, our default category C is a CPO, the category of complete partial orders with continuous functions. (略) It is known that an initial algebra in the category of F-algebras exists when F is a polynomial functors[Mal90].」という記述は……
*1 Data structures and program transformationを参照しているので、これも後で調べる
*2 2006-12-22に複写を入手して読んではいたのだけど、修論関係のゴタゴタで忘れていた
2007-12-16
![[ガルベスアドベンチャー]](./images/20071216_0.png)
λ. 円定期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%)になるようだ。 結構、こういうキャンペーンをやっているところはあるのね。
*1 利付国庫債券(5年)第68回
λ. 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」と書いてあった。どうやって証明するのかしばらく悩んでしまったのだけど、ヒルベルト流の証明を考えて、証明の構造に関する帰納法で証明出来ることを確認した。ヒルベルト流は色々と面倒なので、証明できることを確認しただけで実際に証明はしていないけど。
2008-12-16
λ. Information Flow: The Logic of Distributed Systems 読了
2008-11-11に購入した Information Flow: The Logic of Distributed Systems (Cambridge Tracts in Theoretical Computer Science)(Jon Barwise/Jerry Seligman) を読み終えた。後半はざっとしか読めてないけど、これで心残りがひとつ片付いた。
