日々の流転

λ. ++age == 20

はぁ。

λ. 借りた本

小説すばる 7月号

集英社

『景気と経済政策』

小野善康[著]　岩波新書576

クーやクルーグマンの主張に比べて、サプライサイドの主張はこれまでどうもピンと来なかったので、この本で興味があるのはその辺りかな。

『マインドコントロールの恐怖』

スティーヴン・ハッサン(Steven Hassan)[著]　浅見定雄[訳]　恒友出版ノンフィクションブックス　原題「COMBATTING CULT MIND CONTROL」

λ. 読んだコミックス

『サイレント・メビウス SIDE1』

『サイレント・メビウス SIDE2』

『サイレント・メビウス SIDE3』

麻宮騎亜

λ. 写真

λ. 今日から授業開始。何かやる気が出ない。

λ. 予算編成論

面白そう。

λ. マクロ経済Ⅱ

「復習」とか言われてそんなにガーっと説明されても……すっかり忘れてるし(涙)

λ. 今期の萩野服部研はSICPを読むことに

今期は火曜の方では『計算機プログラムの構造と解釈』(SICP)を読むことになったらしい。それで本を貰ってしまったのだが、積み上げられたSICPはなかなか壮観だったのだ。

λ. art_affine_invert

マニュアルに以下のようにあってビックリした。Affine群というからにはinvertibleなものだけをAffine変換と呼ぶと思っていました。invertibleでないものもAffine変換って呼ぶのでしょうか?

All non-degenerate affine transforms are invertible. If the original affine is degenerate or nearly so, expect numerical instability and very likely core dumps on Alpha and other fp-picky architectures. Otherwise, dst multiplied with src, or src multiplied with dst will be (to within roundoff error) the identity affine.

λ. 学内でRubyが使われていたとは……

何かの授業の登録か何かを管理するRubyで書かれたサーバが落ちて、手作業で作業したとかいう話を聞いた。何でもDRbがsolaris-2.6でトラブったとか……

λ. 西岡研

暇だったので覗いてみることに。符号理論がテーマで代数の入門から。

シラバスには

とっつきにくい代数系ではあるが、近年の計算機の発達のおかげで、大変な計算も記号的に処理され、瞬時に結果が得られるようになってきた。このため、学習する手法もすこし変わってきつつある。

と書いてあったので、Computer Algebra Systems をバリバリ使って学習/研究することを期待してみる。

λ. "Topology via Logic" を輪講することに

今期は"Topology via Logic"を輪講することになった、……というかした。やるぞー

λ. Otter: An Automated Deduction System

Our current automated deduction system Otter is designed to prove theorems stated in first-order logic with equality. Otter's inference rules are based on resolution and paramodulation, and it includes facilities for term rewriting, term orderings, Knuth-Bendix completion, weighting, and strategies for directing and restricting searches for proofs. Otter can also be used as a symbolic calculator and has an embedded equational programming system. Otter is a fourth-generation Argonne National Laboratory deduction system whose ancestors (dating from the early 1960s) include the TP series, NIUTP, AURA, and ITP.

Currently, the main application of Otter is research in abstract algebra and formal logic. Otter and its predecessors have been used to answer many open questions in the areas of finite semigroups, ternary Boolean algebra, logic calculi, combinatory logic, group theory, lattice theory, and algebraic geometry.

メモ。paramodulationって何?

【2006-06-29追記】 萩谷先生の「命題論理の演繹体系」という講義録にparamodulationの解説がある。

λ. ACL

についてちょっと調べてみる。

• Solaris における File ACL (Access Control List)の設定方法

λ. 夕食

水龍。

λ. 誕生日

というわけで今日は誕生日でした。本当に色々な人に祝ってもらえて、とても嬉しかったです。どうもありがとうございます。

川井君にアイスクリームをおごってもらった。

それから、Zinniaさんにねういちさんという方と同じ誕生日だと教えてもらいました。これまで不思議と同じ誕生日の人に会ったことがなかったので、ちょっと嬉しい。それに、この方のTODOには「rubyの勉強」「卒研」「親知らずを抜く」といったキーワードが並んでいて、何だか親近感を感じるのでした (^^;

λ. Zukachan Index - The Five Star Stories

.

λ. let age' = age + 1 in ...

というわけで、今日は誕生日でした。ささやかに祝ってもらった。

λ. 誕生日

今日は誕生日。

最近時間が過ぎ去るのがずいぶん速い気がする。 こんな調子だと人生なんかあっという間に終わってしまうに違いない。 けど、それは流石に困るので、もう少し気合入れて色々頑張らねば。

λ. Build, Augment and Destroy, Universally. Neil Ghani, Tarmo Uustalu, and Varmo Vene

<URL:http://lambda-the-ultimate.org/node/1717>で知って何気なく読んだのだが、「うわっ、やられたっ」と思った。何故これを自分で思いつけなかったのかと思うと悔しい。

帰納的なデータ型を関手Fの始代数としてではなく、忘却関手 U_F: F-Alg → C の極限錐(limiting cone) として特徴付ける。U_Fの錐(C,Θ)から極限錐(μF,fold_F)への一意な射への対応を与えるのがbuild。この特徴づけと始代数による特徴づけは等しい。

ここで、(C,Θ)が錐になっているために必要な条件は ∀h:(X,φ)→(Y,ψ). U_F(h)∘Θ_(X,φ) = Θ_(Y,ψ) で、ちょっと書き換えると ∀h:X→Y. (∀φ:FX→X, ψ:FY→Y. h∘φ = ψ∘Fh ⇒ h∘Θ_(X,φ) = Θ_(Y,ψ)) となり、実はΘを hom(F-,-)→hom(C,-) と考えたときの strong dinaturality になっていたりする。

もちろん、fold/build だけでなく unfold/destroy についても同様のことが言える。また、buildのさらなる一般化であるaugmentもモナドを使って同様に扱うことが出来る(が、こっちは結構ややこしい)。

【2006-11-15追記】augment周りのコードをHaskellで書いてみる

maoさんが<URL:http://d.hatena.ne.jp/m-a-o/20061107#p2>で「augmentを書こうとして挫折した。Monadに持ち上げるとこの(>>=)が定義できねー」と書いていたので、試しにHaskellで書いてみた。Control.RecursionモジュールはCategory Extrasのもの。 型クラスのインスタンスを定義するためにnewtypeでラップしているために、元の定義よりだいぶ複雑になってしまっている。あと、Category Extras でのFixpointクラスにあたるようなクラスを定義できれば、もっと扱いやすい定義が可能かも知れない。

import Control.Recursion
import Control.Monad

data T' h a x
    = Eta' a
    | Tau' (h x)

t' :: (a -> b) -> (h x -> b) -> (T' h a x -> b)
t' f g (Eta' a)  = f a
t' f g (Tau' hx) = g hx

instance Functor h => Functor (T' h a) where
    fmap f = t' Eta' (Tau' . fmap f)

newtype T h a = T{ unT :: Fix (T' h a) }

eta :: Functor h => a -> T h a
eta = T . In . Eta'

tau :: Functor h => h (T h a) -> T h a
tau = T . In . Tau' . fmap unT

ext :: forall h a b. Functor h => (a -> T h b) -> (T h a -> T h b)
ext f = fold (t' f tau) . unT

instance Functor h => Monad (T h) where
    return  = eta
    m >>= f = ext f m
instance Functor h => Functor (T h) where
    fmap = liftM
instance Functor h => Fixpoint (T' h a) (T h a) where
    inF  = T . inF . fmap unT
    outF = fmap T . outF . unT

augment :: Functor h =>
           (a -> T h b) ->
           (forall x. (T' h a x -> x) -> (c -> x)) ->
           c -> T h b
augment f theta = theta (t' f tau)

λ. 植芝理一のマンガみたいな人

MORILOG ACADEMY - 【図工】　特別講義２の記述を読んで、最上の日々(2006-09-25)と同じく「植芝理一のマンガみたい」という感想を持った。いやー、世の中には面白い人がいるものだ。

λ. 小泉首相退任

小泉政権が発足したのが2001-04-26だったから、それから大体5年半がたったことになる。その間には色々なことがあった。

• 派閥推薦を受け入れない組閣
• 経済財政諮問会議主導の予算編成と歳出削減
• 「改革無くして成長なし」という言葉に代表される構造改革路線。不良債権処理の加速。景気の低迷と失業率の増加。
• 産業再生機構の発足。ペイオフ解禁の延期。金融機関の保有株買い入れ。
• 911の同時多発テロと、その後成立したテロ対策特別措置法に基づいた後方支援
• 外務省改革と、田中真紀子と鈴木宗男の対立
• クリントン政権下で冷え込んだ日米関係の改善
• 電撃的な訪朝と平壌宣言。拉致被害者5名およびその家族の帰国。その後の日朝関係の行き詰まり。
• 米国のイラク攻撃に際しての率先した支持
• イラク特別措置法の成立と、それに基づくイラク復興支援
• 靖国神社参拝をきっかけとした中韓二カ国との関係の冷え込み
• 有事法制の成立
• 東シナ海の天然ガス田開発に関する日中の対立
• 道路公団民営化をはじめとする特殊法人改革
• 年金改革
• スマトラ沖地震と津波災害に対する支援
• 郵政民営化と郵政解散
• 狂牛病騒動
• 北朝鮮によるミサイル発射実験
• ……

評価は人それぞれだけど、振り返るとそれなりに感慨深いものもある。 個人的には「改革無くして成長なし」の誤りを認めずに退任してしまうことは残念だし、個別の政策には批判したい部分が多々あるが、同時に小泉政権は概ねよくやっていたのではないかとも思う。 ともあれ、5年半お疲れ様でした。

λ. 誕生日

λ. UFJのスヌーピーEdyカードを解約

約2年前にスヌーピーEdyカードを作ったが、卒業した事により学生カードのメリット(年会費無料,海外旅行傷害保険,ショッピング保険)が無くなってしまうのと、あとAmazonカードを作ってからは使うこともほとんど無くなってしまっていたので、とうとう解約。 電話するのが面倒で伸ばし伸ばしにしていたが、解約は簡単だった。 カードはこちらで裁断してくれということなので、チョッキン。哀れ、スヌーピー真っ二つ。

ただ、ちょっと気になっているのは、まだ引き落とされていない支払いがちょっとだけ残っている点。 普通に考えると、期限の利益の喪失により一括で債務を返済することになると思うのだけど、どうなるのかしらん。

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

を読んだ。「ほんっっと情のかけらもない!!」「だからそうだってば」とか、もはやお約束のやり取り。

λ. 誕生日

λ. 誕生日

age <- arr (+1) -< age

λ. 誕生日