トップ 最新 追記

日々の流転


2006-12-01 [長年日記]

λ. 『壷中の天国』 倉知 淳

壷中の天国 (角川文庫)(倉知 淳) を読了。

Tags:

λ. 随伴とモナド

半順序集合(N,≦)の上の随伴でちと面白いと思った例。

  • p(n)≦m ⇔ n≦g(m)
  • p(0) = 0
  • p(n) = n番目の素数
  • g(m) = m以下の素数の数

擬順序(preorder)上のモナドは closure operator と呼ばれる。

  • a≦T(a)
  • T(T(a)) ≦ T(a)

半順序集合の場合には T(T(a))=T(a) が言える。


2006-12-02 [長年日記]

λ. Remily the Strange by GenocideKitten

少し前に某画像掲示板で見かけて、衝動的に注文してしまった。 色々と素敵。

Tags: 東方

λ. 風邪

風邪引いた。 昨日は喉が痛かったのだが、今日それが直ったら、今度は鼻水が止まらん。


2006-12-03 [長年日記]

λ. 計画停電

計画停電のついでに研究室のサーバ環境を色々リプレース。今回は参加してみたかったけど、風邪でしんどかったので自宅に引きこもっていた。

Tags: tom

λ. GROW CUBE Ver 0.1k

EP1066のレスター(hishouさん)が紹介していたのでプレイしてみる。パーツの依存関係を見極めるのが肝だと思うのだけど、結構むずい。以下のスクリーンショットは、水→人→緑の元→チューブ→鉢→皿→火→骨→玉→バネの順番の場合。こっから先が分からん……

[GROW CUBE のスクリーンショット]

本日のツッコミ(全2件) [ツッコミを入れる]

ψ hato [これ面白いですよね。 私は後輩に教えてもらって、 やってみたらハマリすぎて夜が明けかけた事が……]

ψ さかい [これは確かにはまりますねぇ。 私も気分転換に始めたのに、気がついたらずいぶん時間が経ってしまっていて、危なかったです..]


2006-12-05 [長年日記]

λ. GROW RPG Ver.0.1f

クリア。GROW CUBE に比べるとだいぶ簡単なような。
[GROW CUBE のスクリーンショット]

だいぶ楽しませてもらったので¥500投げ銭。


2006-12-06 [長年日記]

λ. newtypeはHaskellの仕様に不要では?

向井さんのdataとnewtypeのちがいのわかりやすい例というエントリへの便乗なのだけど、newtypeはHaskellの仕様に不要だったのではないかと私は思っている。

向井さんの例でいうと「data T2 = T2 !Int」と「newtype T3 = T3 Int」の表す領域は全く同じである。違うのは「メモリ上のデータの表現の効率」と「パターンマッチの意味」だけ。しかし、この場合にはメモリ上のデータ表現はコンパイラによる最適化が可能であろうし、そのような最適化はプログラマにとって十分透過的*1だろうから、プログラマがメモリ上の表現を明示する意味はあまり無いはず。また、newtypeで宣言した場合のパターンマッチの意味については、dataで宣言した場合でも遅延パターンを用いれば実現できる。

仮にHaskellの仕様にnewtypeがなくても困ることはないと思うし、newtypeの存在はHaskellを仕様を無駄に複雑化しているだけではないか?

【2012年7月追記】

ただ、newtypeを単純に無くしてしまって、同等なdata宣言を用いることにすると、newtypeと同じ効果を実現するために、正格性フラグや遅延パターンなど、「既存の型の別名をつける」という典型的なユースケースに比べてややこし過ぎる機能を利用しなくてはならなくなってしまうので、最近は、単純なことを単純にすませるための妥協として、newtypeはあっても良いかと思っている。

関連

Tags: haskell

*1 「透過的」の意味については <URL:http://www.ipl.t.u-tokyo.ac.jp/~onoue/pub/drthesis02.pdf> を参照。

本日のツッコミ(全3件) [ツッコミを入れる]

ψ 向井 [じつは私も不要だと思っています。それはコンパイラが最適化で頑張ることなんじゃないの、と。 例のエントリは、そこのとこ..]

ψ 山本和彦 [プラグまでもよかったんじゃないですかね。]

ψ さかい [dataとnewtypeには意味上の違いがあるので、今と同様の分け方なら、プラグマではなく言語内での記述であるべきだ..]


2006-12-07 [長年日記]

λ. Applicative Programming with Effects by Conor McBride and Ross Paterson

Monad(Strong Monad)とArrowの間に位置する抽象化だとか、コンビネータのSとKを抽象化したものとかいう話は耳にしてたけど、期待していたよりも面白かった。以前に書いた行列のコードなんかは、これを使って整理できそうだ。

圏論の言葉でいうと Applicative は strong lax monoidal functor になっているということなのだが、(モナドでない)一般の関手の場合のstrengthの「standard equations」なんて知りませんから!(後で調べる)

<2007-03-04追記> standard equations は
\xymatrix{ I\otimes TA \ar[r]^\tau \ar[dr]_{l} & T(I\otimes A) \ar[d]^{T(l)} \\ & TA }

\xymatrix{ (A\otimes B)\otimes TC \ar[rr]^\tau \ar[d]_\alpha && T((A\otimes B)\otimes C) \ar[d]^{T(\alpha)}\\ A\otimes (B\otimes TC) \ar[r]_{\mathrm{id}\otimes\tau} & A\otimes T(B\otimes C) \ar[r]_\tau & T(A\otimes (B\otimes C)) }
の二つだろう </2007-03-04追記>

それから「Note that B and FC swap places in the above diagram: strong naturality implies commutativety with pure computations.」という部分を理解するのにちと苦労した。

あと、最後のexerciseの「fmap swap (pure x ★ u) = u ★ pure x」の証明が案外面倒だった。もっと短く出来ないかな。

[lemma]
pure (f . g) <*> x
= {- homomorphism -}
  pure (.) <*> pure f <*> pure g <*> x
= {- composition -}
  pure f <*> (pure g <*> x)

fmap swap (pure x ★ u)
= {- definition of ★ -}
  fmap swap (pure (,) <*> pure x <*> u)
= {- homomorphism -}
  fmap swap (pure ((,) x) <*> u)
= {- definition of fmap -} 
  pure swap <*> (pure ((,) x) <*> u)
= {- lemma -}
  pure (swap . ((,) x)) <*> u
= pure (\y -> swap (x,y)) <*> u
= pure (\y -> (y,x)) <*> u
= pure (\y -> (\f -> f x) ((,) y)) <*> u
= pure ((\f -> f x) . (,)) <*> u
= {- lemma -}
  pure (\f -> f x) <*> (pure (,) <*> u)
= {- interchange -}
  pure (,) <*> u <*> pure x
= {- definition of ★ -}
  u ★ pure x

いや、「The Monoidal laws and the above definition of pure imply that pure computations commute past effects: fmap swap (pure x ★ u) = u ★ pure x」と言っているのだから、Applicativeの性質からではなく strong lax monoidal functor の性質から示すべきか。むむむ……

<2007-03-04追記> strengthを明示的に使ってはいないが、こんな感じか。

fmap swap (pure x ★ u)
= {- definition of pure -}
  fmap swap (fmap (\_ -> x) unit ★ u)
= fmap swap (fmap (\_ -> x) unit ★ fmap id u)
= {- naturality of ★ -}
  fmap swap (fmap ((\_ -> x)×id) (unit ★ u))
= fmap ((\y -> (y,x)) . snd) (unit ★ u))
= {- left identity -}
  fmap (\y -> (y,x)) u
= {- right identity -}
  fmap ((\y -> (y,x)) . fst) (u ★ unit)
= fmap (id × (\_ -> x)) (u ★ unit)
= {- naturality of ★ -}
  fmap id u ★ fmap (\_ -> x) unit
= u ★ fmap (\_ -> x) unit
= {- definition of pure -}
  u ★ pure x

</2007-03-04追記>

あと、「pure f <*> x1 <*> x2 <*> … <*> xn」を「iI f x1 x2 … xn Ii」と書けるようにする方法は Idiomatica.lhs に詳しい。しかし、こういうこと考えるやつは頭おかしいと思う……

λ. 『伝わる・揺さぶる!文章を書く』 (山田 ズーニー 著)

伝わる・揺さぶる!文章を書く (PHP新書)(山田 ズーニー) を読んだ。

Tags:
本日のツッコミ(全4件) [ツッコミを入れる]

ψ たけを [教えてくん質問で恐縮ですが、strong monad ってどういうのを言うんでしょう?]

ψ さかい [一般に strong ??? というのは適当な条件(coherence condition)を満たす自然変換 τ_{..]

ψ たけを [丁寧な回答ありがとうです。ぐは、むずいー。 strong monoidal functor というのが Mac La..]

ψ さかい [> 丁寧な回答ありがとうです。ぐは、むずいー。 条件の細部はあまり気にする必要ないと思います。 結局のところ、τが..]


2006-12-08 [長年日記]

λ. 自由変数と限量子∀∃

かがみさんが「自由変数って」ということを書いていたので、自分の自由変数の理解を書いてみる。

任意の言語Lに対して、Lに含まれない定数記号xを新たに加えた言語をL{x}とする。そして、自由変数を含む式 φ(x) はLの式ではなくL{x}の式と考える。L{x}に更に新たな定数記号yを加えた言語はL{x}{y}と書けるが、L{x}{y}とL{y}{x}は区別せずに単にL{x,y}と書くことにする。そうすると、論理式φの自由変数の集合がFV(φ)であるとき、φ∈L(FV(φ))が成り立つ。

それから、LからL{x}への埋め込み I: L→L{x} が定義できる。この埋め込みには右随伴 L{x}→L や左随伴 L{x}→L が存在する場合があり、それぞれ(∀x)や(∃x)と書かれる。すなわち、任意の φ∈L, ψ∈L{x} に対して

  • I(φ) |-L{x} ψ iff φ |-L (∀x)(ψ)
  • (∃x)(ψ) |-L φ iff ψ |-L{x} I(φ)

【2006-12-14 追記】 檜山さんが「論理とはなにか? (4:完) -- 論理から圏へ」で、「論理と圏の対応関係がうまくいっている例として直観主義論理があります」と書いていましたが、限量子を随伴で説明できることから、述語論理も圏と対応させることが出来ることがわかります。

本日のツッコミ(全4件) [ツッコミを入れる]

ψ かがみ [こんにちは、鏡です。 モデル理論で全称記号や存在記号の解釈を行う場合、定数を水増しする手法が有効なことは知っていたの..]

ψ ささだ [かみさんが、と読んでびびった。 あと、数式が顔文字に見えた。]

ψ あろは [ものすごく細かくて恐縮ですが φ∈L(FV(φ)) ではなく, φ∈L{FV(φ)}が成り立つ。 のような気..]

ψ さかい [>かがみさん お役に立てたみたいで良かったです。 モデル理論での事については知らなかったのですが、それも面白そうです..]


2006-12-09 [長年日記]

λ. iTunesの作るUnicodeのファイル名ではまる

iTunesで「[iTunes Music] フォルダを整理する」という設定にすると、曲名等に基づいてファイル名が決まるのだけど、曲名にCP932で表現不可能なUnicodeの文字が含まれていても、そのままファイル名になってしまう。「Mont Saint Michæl et Sa baie」という曲の「æ」はCP932で表現不可能だったために、そのファイルが古いアプリケーションからアクセスできずにはまった。iTunesに「現在のコードページで表現不可能な文字をファイル名に使わない」というオプションがあると嬉しいかも……

【2006-12-28 追記】 バックアップには、Unicodeファイル名に対応している 7-Zip を使うとよいかも。 なお、Linux上でp7zipで展開すると、ファイル名をちゃんと現在のlocaleのエンコーディングに変換して展開してくれた。ただし、ファイル名の中に現在のlocaleで表現できない文字が一文字でもあると、全ての非ASCII文字を「?」に変換するようだ。

λ. 宇迦之御魂神

というページを偶然読んだ。

さて、お稲荷さんといえば誰でも狐をイメージするはずである。それくらいにポピュラーな存在だけに、狐を稲荷神と錯覚している人もいるくらいだ。しかし、これまで述べてきたように、稲荷神というのは宇迦之御魂神のことであって、狐はその稲荷神の使いとされる霊獣なのである。
また、稲荷神の使いとしての狐には、人に取り憑いて害をなすようなおどろおどろしくて気味の悪いイメージがつきまとう。これは、狐が霊力を持ち妖術を駆使する、という中国の考え方が日本にも入ってきて、稲荷神が真言密教の陀枳尼天と習合したときに発生したものである。

全く知らなかった…… orz

教養が欲しいなぁ……

λ. tdiary-mode を https で

久しぶりにtdiary-modeを使おうとしたらhttpsで使えなかったので、ssl.elを使って対応してみる。プロキシの扱いについては、わからんので放置。どうせ私は使わないし。http-20061209.el

Matzにっき(2005-07-21) によると、まつもとさんも同じようなことをしているようだ。あと、<URL:https://www.codeblog.org/codeblog-users/11.html>には「tdiary-mode.el は HTTPS や TypeKey に対応していませんが、 typekey.el をインストールすると使えるようになります」と書いてあった。

Tags: tDiary

2006-12-10 [長年日記]

λ. 第二十四回圏論勉強会

今日は圏論勉強会だった。写真

Tags: 圏論

λ. 英語で「天の声」は何?

圏論勉強会後の飲み会で「天の声」って英語でなんて言うのだろうかという話があったが、毎日新聞と毎日デイリーニュースの対応する記事を幾つか比較してみた限りでは、「天の声」に直接対応する言葉はないようだ。

例:

談合は「bid-rigging」。わいろは「bribe」。収賄は「bribe-taking」。

Tags: 英語

2006-12-11 [長年日記]

λ. Shortcut fusion is correct by Patricia Johann

以前から読まなくちゃと思ってはいたのだけど、<URL:http://d.hatena.ne.jp/m-a-o/20061206#p1>で見かけたのをきっかけに読んでみた。操作的(operational)なモノの見方に慣れていなかったので苦戦。証明は追えたけど、いまいち実感がわかない。

TT-closedness の定義は面白い。 スタックの関係と項の関係の間の sT⊇s ⇔ r⊆rT という随伴から定義されるclosure。

「lazy PolyPCF」の lazy の意味は lazy λ-calculus (20040102#p03 を参照)のと同じ意味。lazy PolyPCF を扱うには、Free Theorems in the Presence of seq でのように inequational logical relation にすればよいのだろうけど、もう結果は出てるのかな?

結局、operational に考えることのメリットは何か? impredicative polymorphism があるとモデルを考えるのが大変なのに対して、operational semantics と contextual equivalence に基づけば、複雑なモデルを考えなくて済むということか? しかし、fix と impredicative polymorphism を持つ言語のモデルで、admissibleな関係に限定したparametricityが成り立つモデルは知られていないのだろうか? もしそのようなモデルが知られているのなら、同程度の労力で short-cut fusion の正しさを示すことは可能であるように思う(TT-closednessを示すのも領域理論的なadmissibilityを示すのも似たようなものだろう)。

Tags: 論文

2006-12-12 [長年日記]

λ. 今日のIT-system

Tags: tom

λ. スンニ派とシーア派の違い

生徒の作文で宗教対立を扱っていたところから、スンニ派とシーア派の違いの話に。調べてみると、こんな違いがあったのね。へぇ、へぇ、へぇ。

イスラームという宗教が生まれて間もない初期のころ(正統カリフ時代)に、預言者の後継者(ハリーファ(カリフ))を誰にするかという問題において、ムハンマドの従兄弟かつ娘婿であるアリーとその子孫のみがイマームとして後継者の権利を持つと主張したシーア・アリー(「アリーの党派」の意。後に略されて「シーア」、すなわちシーア派となる)に対し、アブー=バクル・ウマル・ウスマーンのアリーに先立つ三人のカリフをも正統カリフとして認めた大多数のムスリム(イスラーム教徒)がスンナ派の起源である。
本日のツッコミ(全2件) [ツッコミを入れる]

ψ takot [1時は朝だお!( ^ω^)]

ψ さかい [そういえば、こないだ起きたら3時だったお!( ^ω^)]


2006-12-13 [長年日記]

λ. 著作権の価値評価と相続税

小熊さんのところで著作権は無体財産権として相続税がかかるということを知る。考えてみれば当たり前だけど、これまで考えたことが無かった。国税庁の通達の「著作権の評価」の部分を読むと、「複利年金現価率」とか難しい言葉を使っているけど、将来の印税収入の割引現在価値みたいな感じで評価されるようだ。「年平均印税収入の額×0.5×評価倍率」の0.5倍という数字がどこから来ているのか謎だけど。

それから、その形算式に権利の存続期間が全く入っていないという話ですが、「相続税は資産すなわち経済的価値への課税であり、権利への課税ではないから」ということではないでしょうか。経済的価値の評価であれば、権利の存続期間ではなく「著作物に関し精通している者の意見等を基として推算したその印税収入期間」を基準にするのは適切でしょう。もちろん、推算した印税収入期間を超えても権利の存続期間であれば収入を生じる可能性はありますが、この「可能性」は価値評価するのが難しく、そのため相続税として正当化するのもまた難しいのではないかと思います。

λ. 『硫黄島からの手紙』

『硫黄島からの手紙』を観てきた。平日の昼間だからガラガラだと思っていたが、混んでるとまでは言えないにしても、結構人が入っていた。内容は、涙無しには見れないというほど没入することは出来なかったが、心を打つものはあった。ただ、ある程度の前提知識を持っていないと、タイムスケジュールが分かりにくいのではないかと思った。

Tags: 映画
本日のツッコミ(全3件) [ツッコミを入れる]

ψ 小熊善之 [そうか! 「著作物に関し精通している者の意見等を基として推算したその印税収入期間」を存続期間にしちゃえばいいんだ!(..]

ψ タナカコウイチロウ [硫黄島とOR 映画とは直接関係有りませんが、硫黄島の戦いを数理的に分析したものが有ります。 佐藤 著、自然の数理と社..]

ψ さかい [>小熊さん それ案外良いかもしれませんよ (笑 さらに相続者をその推算のプロセスに巻き込むなどすれば、存続期間を印税..]


2006-12-14 騏驎も老いては駑馬に如かず [長年日記]

λ. Domain Theoretic Models Of Polymorphism by Thierry Coquand and Carl A. Gunter

読みかけ。

cocontinuous な functor F: C→DEP から、Grothendieck construction で圏 ΣF と射影 p:ΣF→C を定義する。CがdomainならΣFもdomainになっている。pのcoconitnuousなセクション C→ΣF とその間の自然変換からなる圏を ΠF とする。Cがdomainなら ΠF もdomainになっている。

CをDEP自身とする。このときΣFは半順序集合にならない。ΠFは半順序「集合」にはならずクラスになるが、圏同値なdomainが存在する。このΠを使って多相型を扱う。

このモデルはuniformに振舞わないような多相的な要素を含む。 admissibleな関係に限定した場合のparametricityは……やっぱり成り立たないのかな?*1

Tags: 論文 圏論

*1 もし成り立つのであれば Shortcut fusion is correct はインパクトを持たない気がするし

λ. 凄い漢字

<URL:http://www.rubyist.net/~matz/20061204.html#p02> にツッコミをいれようとしたら、spamフィルタに弾かれたみたいなので、こっちに。その「うしのあゆみがおそい」はU+3E2A(「㸪」)として既に含まれているような。


2006-12-15 [長年日記]

λ. 著作権保護期間の延長問題を考える国民会議第1回公開シンポジウム

心情の問題は議論するだけ不毛だと思うので、公共政策としての議論をもっと聞きたかった。あと、「いわゆる作家の作品だけでなく、論文や新聞記事も全て著作権法の影響を受ける」という話は忘れてはいけないと思った。

ちなみに、個人的な意見は田中辰雄氏とほぼ同じ。

個人的意見

そもそも、著作権法第1条(目的)に「著作物並びに実演、レコード、放送及び有線放送に関し著作者の権利及びこれに隣接する権利を定め、これらの文化的所産の公正な利用に留意しつつ、著作者等の権利の保護を図り、もつて文化の発展に寄与することを目的とする」と謳われているように、著作権制度の究極的な目的は著作者個人の保護ではなく、「文化の発展」という社会全体の利益であり、これを実現するのに最も適した制度を選択すべき。

「文化の発展」というのは抽象的で何を指しているか曖昧だけど、私は「著作物によって生み出される純便益がより大きな社会」を「より文化の発展した社会」と定義するのが良いのではないかと思っている。まあ中立的な定義だと思うし、比較も出来るし。で、著作物の便益とは、それを消費することによって得られる効用や、それを利用することによって間接的に生じる波及的な便益のはず。(ちなみに権利から得られる収入自体は別に便益ではない。生産者にとっての収入は利用者にとっての費用で、社会全体でみれば±0だし)

著作権保護期間の延長によって生産者の権利を大きくする場合のことを考えると、「著作物の消費や利用への制限が強くなるので、個々の著作物から生じる便益は減少する」という効果と、「生産者が得られる利益が増えるため、著作物の生産が増える」という二つの効果があり、どちらの影響が大きいかによって社会全体の便益は大きくなる場合もあれば小さくなる場合もある。そのどちらが起こるかを判断するデータがなければ、賛成も反対も出来ないなぁ。

現状では判断できないけど、一度延長すると短縮は難しいから、延長によって社会全体の便益が増加するという定量的データがない限りは延長には慎重であるべき。

また、より根本的に著作権制度を考えるのなら、小熊さんが以前に書いていた「無方式で発表後30年、その後は文化庁に登録(要登録料)で、最大著者の死後70年(勿論、特許権と同様に、時間の経過と共に登録料が加算される)という制度」のような制度も検討すべきだと思う。

λ. 著作権の価値は著作権保護期間延長でどれだけ増加するか?

上のシンポジウムのレッシグの話ではノーベル賞経済学者がどうとか言っていたが、試しに簡単な数字で計算してみる。

作品は著作権保護期間内は毎年1単位の印税収入をもたらすとし、作品公表後20年後に作者が死亡するとするものとする。また、割引率は3%とする。そうすると、著作権保護期間が死後50年の場合、作者の生前20年間と死後50年間の印税の現在価値の合計は \[\sum_{i=1}^{70} \frac{1}{1.03^i}\] ≒ 29 。保護期間が死後70年の場合生前20年間と死後70年間の印税の現在価値の合計は \[\sum_{i=1}^{90}\frac{1}{1.03^i}\] ≒ 31 。この場合、保護期間を50年から70年に延ばせば、6.5%くらい著作権の価値が上昇することになる。

けど、実際には90年間コンスタントに印税が入り続ける作品なんて存在するはずも無く、時間の経過と共に印税は減少するから、実際の価値の上昇はこれより遥かに低いだろう。著作権の価値に影響する他の要因に比べれば、保護期間延長による価値の増加は結局ノイズ程度だろうと思う。クリエイターに与えるインセンティブは限定的だろうし、遺族の生活保障という話も怪しい。

λ. 今日の「言語の意味論」

  • 時制(tense)とアスペクト
    • Aktionsart (動作相, 為相, 動詞様態, 動作様態, 動作様式)
  • 裸の複数名詞句(bare plural)とCarlsonオントロジー(存在論)
  • 中立叙述と総記
  • 名詞句化(Nominalization)
  • ロバ文
  • DRS

λ. 今日の向井研

  • Kleisli圏
  • 自然変換の水平合成
  • 自然化?
Tags: 向井研

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].」という記述は……

Tags: 論文

*1 Data structures and program transformationを参照しているので、これも後で調べる

*2 2006-12-22に複写を入手して読んではいたのだけど、修論関係のゴタゴタで忘れていた


2006-12-19 [長年日記]

λ. 何か変な夢見た

何か変な夢見た。 切羽詰ってくると変な夢みるよなぁ。

λ. ハマスとファタハ間の緊張高まる - パレスチナ自治区

とおやまさんのところから。 なんでハルヒなんだろう……

【追記】 翌日、S氏にファンタ with 涼宮ハルヒの憂鬱というのを紹介されて、「ファタハ with 涼宮ハルヒの憂鬱」と激しく空目した。

Tags: ネタ

2006-12-20 [長年日記]

λ. ゆで卵だと思って割ったら

ゆで卵だと思って割ったら、温泉卵だった。しょぼーん。勢い良く回転するのも確認したのに……

λ. 頭の体操: 3引数flip

現実逃避にやってみる。当たり前だけど、({id,flip31,flip32,flip33,flip34,flip35}, (.), id)は群をなし、{a,b,c}上の置換群と同型。

flip31 :: (a -> b -> c -> d) -> (a -> c -> b -> d)
flip31 = map flip
  where
    map :: (x -> y) -> ((z -> x) -> (z -> y))
    map = (.)

flip32 :: (a -> b -> c -> d) -> (b -> a -> c -> d)
flip32 = flip

flip33 :: (a -> b -> c -> d) -> (b -> c -> a -> d)
flip33 = flip31 . flip32

flip34 :: (a -> b -> c -> d) -> (c -> a -> b -> d)
flip34 = flip32 . flip31

flip35 :: (a -> b -> c -> d) -> (c -> b -> a -> d)
flip35 = flip32 . flip33
Tags: haskell

2006-12-21 [長年日記]

λ. Scheme:マクロ:CommonLispとの比較

黒田さんの About Scheme を読んだときには、「Scheme のマクロは hygienic なのに、何を勘違いしているのだろう。Schemerは反論すればよいのに」と思っていたのだけど、単なる反論よりもずっと興味深い話が出てきた。

Schemeのマクロは、「展開結果内での自由変数」を正しく扱うために、S式だけでなくマクロ定義の「環境」も同時に扱っていて、そのため syntactic closure と呼ばれていると。

Tags: scheme

2006-12-23 天長節 [長年日記]

λ. RHG読書会::東京 入門JavaScript

ECMAの仕様書を予め用意して行けば良かったと後悔。 しかし、Javascriptは気持ち悪くて楽しい。

Tags: javascript

λ. 奉祝・天長節

世界の平和と我が国の末長い繁栄を祈念致します。


2006-12-24 [長年日記]

λ. Pandora Internet Radio - Find New Music, Listen to Free Web Radio

Pandora is the music discovery service that helps you find new music based on your old and current favorites. Create custom internet radio stations, listen free.

chikoにっき (2006-12-15) より。曲名やアーティスト名を入れると、好きそうな曲を勧めてくれる。全然知らないけど似てる曲が次々紹介されるので、聴いてて楽しい。

Tags: 音楽

λ. アインクライネスオーケストラ定期演奏会

アインクライネスオーケストラの定期演奏会に行ってきた。

  • 歌劇「魔笛」序曲 by モーツァルト
    Mozart / Die Zauberflëte Overture K.V 620
  • ハイドンの主題による変奏曲 Op.56a by ブラームス
    Brahms / Variationen über ein thema von Joseph Haydn Op.56a
  • 交響曲第7番 イ長調 Op.92 (ベーレンライター原典版) by ベートーヴェン
    Beethoven / Symphonie Nr.7 in A-dur Op.92
  • クリスマスソングメドレー (アンコール)
Tags: 音楽

2006-12-26 [長年日記]

λ. almost epi

メモ。終対象への射はepiだとは限らない。 例えば、始対象0が存在する場合を考えると0→1はepiとは限らない(少なくともSetではepiでない)。

けど、almost epi にはなっている。φ:F→M が almost epi なのは、任意の g:M→M について gφ=φ を満たすならばgがautomorphismであるとき。この almost epi の定義は Relative Ext Groups, Resolutions, and Schanuel Classes by Henrik Holm より。他の定義もどっかで見たことがあるような気はするが。

Tags: 圏論

2006-12-27 [長年日記]

λ. mixiミュージック

今更だけど、mixiミュージックを始めてみた。 同人CDの作者とかも結構エントリがあって面白い。

<URL:http://music.mixi.jp/list_music.pl?id=14025>

Tags: 音楽

2006-12-28 [長年日記]

λ. agda-mode.el と cl-push

久しぶりにアップデートしたら何やらcl-pushが無いとかいうエラーが出たので、一行パッチ。

agda-mode.el.diff

Tags: agda

2006-12-29 [長年日記]

λ. ドライブのサイズ変更ではまる

デスクトップ機のメインのドライブが少し手狭になってきたので、50GBほどサイズを増やした。

partedはNTFSの操作に対応していないので、ntfsresizeを使う。ただ、ntfsresizeはファイルシステムの操作だけなので、パーティション自体のサイズは予め別のツールで変更しておく必要がある。partedはファイルシステムを無視してパーティションのサイズだけを変更する機能がないので、今回はfdiskを使ってみる。パーティションを一度削除して、同じ開始位置で大きなパーティションを作ればよいかと思ったのだが、元のパーティションがシリンダ単位にアラインされていなかったので、同じ場所に作れなかった(追記: uオプションを与えればセクタ単位に出来たらしい)。しかも、そこで一回パーティションテーブルを保存してしまった上、パーティションテーブルのバックアップもとっていなかったため、困ってしまう。

最終的には結局partedを使った。rescueコマンドで元のパーティションを一回復元し、パーティションの位置をちゃんと確認(以前にパーティションを見失った時にはgpartを使ったが、便利になったものだ)。 rmコマンドでパーティションを削除後、mkpartコマンドで同じ開始位置の大きなパーティションを作成(追記: PartedはMB単位で小数点以下3桁しか表示しないので、同じ開始位置のパーティションを作るにはやはりfdiskを使うべき)。 そして、ntfsresizeでファイルシステムのサイズを変更。

fdiskのような不慣れなツールに手を出さなければ良かった。あと、partedがlibntfsに対応しているか、もしくはファイルシステムを無視したパーティションサイズの変更に対応していれば良いのにと思った。

本日のツッコミ(全2件) [ツッコミを入れる]

ψ yaizawa [チキンな私はとりあえずPartition Magicに逃げてます.(汗 HPFS扱えるし.← 意味なし]

ψ さかい [Partition Magic 買っても良かったのだけど、新しいツールを使うのが面倒くさくて、使い慣れたツールに頼っ..]