2001-12-06
λ. ケインズとは決別したが
毎日新聞の朝刊に「ケインズとは決別したが」という経済財政白書についての社説があった。以下のようなくだりがあるのだけど、いつのまに「常識」になったんだ? 俺が流行に遅れてるのかねぇ?
なぜ日本経済はいつまでも低迷するのか。白書はその主因が潜在的な成長率の低下という供給サイドの問題にあるとし、過去の「負の遺産」である不良債権問題などが、潜在成長率を押し下げるメカニズムを明らかにする。
その上で潜在成長率の引き上げは経済構造改革なくしてありえないと論じた。今にして常識的かつ説得力のある主張だが、過去の白書からすれば大転換といえる。
λ. まあいいや。経済財政白書ってメディアセンターには入るのかな? そしたら読んでみよ。
λ. 研究会
で、Rubyについて発表しました。katokenさんに逃亡されてしまったので、これとかこれを映しながら、一人で小1時間ほど延々と喋ってたのですが、……発表って疲れるだけで発表してる側は全然楽しくないのね。なんか、もっと恍惚感みたいのを感じるんじゃないかと想像してたんだけど……
λ. まあ、リファレンスマニュアルのRWikiが落ちてて焦ったりといったハプニングはあったものの、なんとか無事に終わって良かったとホッとしている。
λ. しかし、やっぱり失敗したなぁというのが実感。1時間もダラダラ話してしまったせいでメリハリが全然無かったし、その一方で幾つか大事な話を言い忘れてたり、散々だったよ。プレゼンの技法って自然に身に付くとは思えないので、やはり意識的に学ぶ必要があるな。
λ. あと、内容自体についても、動的な言語を知らない人間に嬉しさをどうやって伝えるかとかもっと考えておくべきだった。コンパイル時のチェックがほとんど出来ないという明らかなデメリットの一方で、それ覆すだけの「嬉しさ」もあるんだけど、それを実際に使わずに実感するのは難しいわけで……
λ. 今日の英語: bestiality
- The unspeakable bestiality of Auschwitz and more recently, of Cambodia and other countries deprived many people of their faith in the goodness of humanity.
λ. 読書
- 『アクエリアンエイジ オリオンの少年』 第1巻
- 極楽院櫻子[著] ブロッコリー, 中井まれかつ[原作,原案]
- リンク:
λ. Re: 正規表現
scanは知ってますけど、僕のイメージしていたのは、(本来の正則表現としての)マッチ可能性を(バックトラッキングして)全て列挙するものなので、scanとは違うっす。
"abcd1".scan(/(.+)d(\d)/){|item| p item}
#=>
# ["abc", "1"]
2002-12-06
λ. 「風邪をひいた」と言ったら、「そうか、酒井君も人間だったんだ」と言われた。わたしゃ、ロボットか宇宙人か何かですか?
そーいや、以前に他の人に「それ以前にホモサピエンスかどうか……」とか言われたこともあったな。
λ. 言語の意味論
参照的読み，属性的読み，内部属性的読みの違いがサッパリ分からない。やばい。
それから、「情報とは何か?」というのは非常に難しいのね。しかし、「エネルギーや粒子と相互作用する可能性を含んだ実体」としてinfon(情報子)か存在すると考えている研究者もいるのか。Keith Devlin とかがそうらしいけど、そういう人には「世界」ってどんな風に見えてるんだろう……
λ. 電界図鑑 - Bit World Laboratory (ルククノック研究所)
「情報子」で検索していたらこんなサイトにたどり着いた。状況理論のinfonとは全然関係ないけど、なんかいいなぁ、こういうのって。
λ. 今日の向井研
発表者が一人もいない5限……
2003-12-06
λ. 借りた本
- 小説すばる 2003年3月号
- -
- 『アガサ・クリテスティーの食卓』
- 北野 佐久子 [著]
λ. 禁忌「恋の迷路」初ゲット
そういえばそろそろ黒幕の季節ですね。だからというわけでもないけど、最近久しぶりに紅魔郷やってます。で、禁忌「恋の迷路」初ゲットー! (リプレイ) それにしても妹様は強いなぁ。
λ. 慰安所運営関与の新証拠
毎日新聞夕刊に以下のような記事が載っていた。
- 慰安所運営関与の新証拠見つかる【ロサンゼルス共同】
5日付米紙ロサンゼルス・タイムズは、第二次世界大戦中の日本による従軍慰安婦問題で、旧日本軍が慰安所の運営に関与していたことを示す連合国軍総司令部(GHQ)の報告書が新たに見つかったと報じた。
同誌によると、見つかったのはGHQが戦後に行った戦争捕虜への聞き取り調査報告。各地の慰安所経営者らは軍から許可を得て運営し、顧客の軍人の階級や人数など詳細な記録の保管を求められていたほか、売上月報を軍に提出していた。
報告書はGHQが1945年11月にまとめたもので、米国や韓国の慰安婦問題研究チームが機密解除された米国の公文書の中から入手した。
こういう記事が出るということは、今回機密解除された文章からは今のところは強制連行の証拠は出てきていないのだろう。ところで、この証拠は旧日本軍による慰安所の経営への監査が行われていた事を示しているわけで、むしろ一部の論者の『旧日本軍には、慰安所業者の不法行為を意図的に放置した「不作為の罪」がある』という主張への反証となるように思える。
2004-12-06
λ. HaskellでScheme処理系を実装 (1)
研究会で書いてた処理系を、構文木を辿るやつからスタックマシンっぽいやつへと書き換えた。とは言っても操作的意味論すなわち状態遷移規則を素朴に実装しただけ(状態遷移用の関数 trans :: State -> IO State をひたすら呼び続けるだけ)なので、かえって遅くなってるだろうな。
とりあえず、これで末尾呼び出しの最適化とcall/ccの実装は出来た。あと、だんだんCのコードを生成する方式にしたくなってきた。
2005-12-06
λ. 差金決済取引
差金決済取引という概念と現物取引では差金決済取引が禁止されていることを知らなかったせいで、絶好の買い場を逃す。ネット証券で株取引を始めたイマドキの人間としては、取引が約定したら即座に受け渡しが行われているものだとばかり思っていたけど、実際にはそうではないということか。しかし、現物取引でも同一銘柄でない場合には差金決済取引にはならないし、またそもそも信用取引では差金決済取引は禁止されてないし……なんだか理不尽な規制に思える。とりあえず、チャンスが来たときにためにキャッシュポジションには余裕を持っておくべきか。あと、信用取引の口座も一応作ったほうがいいのかな?
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はあっても良いかと思っている。
関連
- newtype/datatype (was efficiency)
- Haskell と OCaml
- [haskell-jp:155] 質問: data, newtype のパターンマッチの動作の違いについて (2012年7月)
*1 「透過的」の意味については <URL:http://www.ipl.t.u-tokyo.ac.jp/~onoue/pub/drthesis02.pdf> を参照。
2007-12-06
λ. Coqで“無限オブ無限”
稲葉さんの「無限オブ無限」は余再帰的な関数(corecursive function)の良い例題なのではないかと思い、Coqでも書いてみることにした。 何故いつものAgdaではなくCoqかというと、Agdaはまだcodataに対応しておらず無限リストやストリームを直接扱うことが出来ないため。
まず、Coqでは余再帰的な関数は、全域関数であることを保証するために guarded corecursion の形で書かないといけない。ので、guarded corecursion の形で書こうとしたのだけど、色々試してもどうも書けない。
何故かと思って落ち着いて考えてみたら、そもそも iflatten (repeat []) が実効的(effective)に定義出来ないから、この関数 iflattern は全域的な計算可能関数ではないのだった。
色々細かい条件を色々加えればCoqでも定義できるだろうけど、Coq初心者の私にはそれは面倒なので、とりあえず無限リストの無限リストの場合のみで定義してみた。Coqでマトモに何かを書くのは初めてなので、変な書き方をしてるかも知れないけど、そこは識者のツッコミに期待しておきます(^^;
(* IFlatten.v *)
Section IFlatten.
Require Import List.
Require Import Streams.
(* anamorphisms (co-iteration) *)
CoFixpoint unfold (A X : Set) (phi : X -> A*X) (x : X) : Stream A
:= match phi x with
| (a, x) => Cons a (unfold A X phi x)
end.
Implicit Arguments unfold [A X].
Inductive CV (A X : Set) : Set :=
| CVLast : X -> CV A X
| CVCons : A * CV A X -> CV A X.
Implicit Arguments CVLast [A X].
Implicit Arguments CVCons [A X].
(* futumorphisms (course-of-values co-iteration) *)
Definition futu (A X : Set) (phi : X -> A * CV A X) (x : X) : Stream A
:= let psi cv :=
match cv with
| CVLast x => phi x
| CVCons p => p
end
in unfold psi (CVLast x) .
Implicit Arguments futu [A X].
Definition add_prefix (A : Set) (xs : list A) (X : Set) (cv : CV A X) : CV A X
:= fold_right (fun a cv => CVCons (a, cv)) cv xs.
Implicit Arguments add_prefix [A X].
Definition iflatten (A : Set) (ss : Stream (Stream A)) : Stream A
:= let phi x :=
match x with
| (ss, ls) =>
let s := hd ss in
let ss2 := tl ss in
let ls2 := tl s :: List.map (fun x => tl x) ls in
( hd s
, add_prefix
(List.map (fun x => hd x) ls)
(CVLast (ss2, ls2))
)
end
in futu phi (ss, nil).
Implicit Arguments iflatten [A].
End IFlatten.
(* Haskell のコードを出力する *)
Extraction Language Haskell.
Extraction "IFlatten" iflatten.
これをCoqIDEに読み込ませたら、ちゃんと通った。 Coqで定義が通ったので、少なくともちゃんと全域関数になっていることは分かる。そして、ExtractionでHaskellのソースコードを生成したので、正しく定義できているか簡単に確認してみることに。 このままだと試しにくいのでまずは簡単なラッパを定義する。
import IFlatten l2s :: [a] -> Stream a l2s (x:xs) = Cons0 x (l2s xs) s2l :: Stream a -> [a] s2l (Cons0 x xs) = x : s2l xs iflatten' :: [[a]] -> [a] iflatten' xss = s2l $ iflatten $ l2s [l2s xs | xs <- xss]
で、試す。
Main> take 10 $ iflatten' [[(i,j) | j<- [1..]] | i<-[1..]] [(1,1),(2,1),(1,2),(3,1),(2,2),(1,3),(4,1),(3,2),(2,3),(1,4)]
うん、ちゃんと定義できてるみたい。 折角Coqで定義したので、題意を満たしていることをちゃんと形式的に証明したいところだけど、それはまだやっていない。
【2007-12-10追記】 にわとり小屋でのプログラミング日記のyoshihiro503さんが、形式的な証明をしてくれたようです。わーい。 ⇒ Coqで”無限オブ無限” - にわとり小屋でのプログラミング日記
2008-12-06
λ. 風邪でダウン中 (3)
熱は37℃台のままだけど、お腹の調子が悪化中で一日中悶えていた。 今日は20回くらいはトイレに駆け込んだよ……
λ. ビッグ３公聴会：格付け会社「破綻回避７５０億ドル必要」
自家用ジェット機が批判されたからって、ミシガン州から800キロ超の距離を10時間以上かけてワシントンに入るって……
