2003-01-01 [長年日記]
λ. 明けましておめでとうございます。
昨年は色々と迷惑をお掛けしたと思いますが、本年もぜひよろしくお願い致します。
λ. 読書
- 『テニスの王子様 16』
- 許斐 剛 [著]
2003-01-02 [長年日記]
λ. 最小不動点と最大不動点
A Categorical Programming Lanuage の論文では
left object nat with pr is zero: 1 -> nat succ: nat -> nat end object
に対応するright objectとして
right object conat with copr is pred: conat -> coprod(1,conat) end object
を定義していた。ここでnatは NatF(X)=1+X の最小不動点に、 conatはNatFの最大不動点になってる。 対称性は、natの定義を以下のようにcoprodを用いたものに書き換えると 明らかでしょう。
left object nat with pr is α: coprod(1,nat) -> nat end object
論文には(何故か)取りあげられていないのですが、 さらに同様にして、
left object list(X) with prl is nil: 1 -> list cons: prod(X,list) -> list end object
に対応するright objectとして
right object colist(X) with coprl is α: colist -> coprod(1,prod(X,colist)) end object
が定義できるはずだ(しかし、natural transformation αの良い名前が思いつかなひ)。 listが有限のリストを、inflistが無限のリストを表わしているのに対して、 こいつは有限と無限の両方のリストを表わすはず。 listとinflistからの埋め込みはそれぞれ
- list2colist = coprl(prl(in1, in2.prod(I, case(nil, cons))))
- inflist2colist = coprl(in2.pair(head,tail))
となる。
λ. Haskellとの関係
ところで、Haskellのリストがlist,inflist,colistのどれに対応するかを考えると、Haskellのリストは有限のリストも無限のリストも共に表わすことが出来るので、明らかにcolistに対応するはず。
代数的データ型の意味はfunctorの最小不動点として与えられるとよく言われるが、Haskell等のlazyな言語ではそのlazynessのために最大不動点になっているように思える。
2003-01-04 [長年日記]
λ. チュチュ
豊田さんもプリンセスチュチュ見てるですか。あのアニメはわりと楽しいですよね。でも、チュチュという名前が「主体(チュチェ)思想」を連想してしまって……。
λ. CPL
1/2のlist2colistには間違いがあったので訂正。正しくは「list2colist = coprl(prl(in1, in2.prod(I, case(nil, cons))))」。あー、ややこしー。ところで、colistの長さはnatでは表せないけど、conatは無限大も含むのでcolistの長さはconatで表す事が出来る。すなわち「colist-length = copr(coprod(I, pi2).α)」。
λ. ||=
私はわりと良く使う気がします。
λ. 共変化(covariance)
へたれ日記(2003-01-04) に書いてあった「共変化」。最初、何の訳か分からなかったけど、考えてみれば「covariant functor」は「共変関手」と訳されてるわけだし、なるほどという感じ。
ただ、「ルーチンの引数の型および結果の型を子孫クラスの型に変更することを共変化 (covariance)といいます」と書いてあるけど、結果の型を子孫クラスに変更できるのは自然なのだ(参考: exponential functor の variance)けど、引数の型を子孫クラスに変更する際にはどういう扱いになっているのだろう……。
λ. ヴァンパイアハンターD / VAMPIRE HUNTER D
ふとCATVの番組表で目に止ったので見てみた。スタイリッシュな世界観が何ともいえない。そういえば、原作の文庫は図書館で何回か見掛けたような気がする。こんど読んでみよっかな。
……なんて事やってる場合じゃないんだよなぁ……。もう明後日から学校だよ。ぎゃー
2003-01-06 [長年日記]
λ. 寝坊。
λ. Ruby-CPL (仮称)
型推論部分で設計ミスに気付く。引数を持たないようなClosedFunctorialExpressionはsubstitutionによって引数を増やすことが出来ない……。ぎゃー。
λ. コンパイラ構成論
レポートは木曜まで。やばい。
λ. 東方妖々夢
ようやくプレイ。ミスディレクション楽しいですね。あと、アンディレクティッド・レーザーもいい感じ。
λ. 読書
- 『全日本妹選手権 3』
- 堂高 しげる [著]
λ. 代替スタイルシート
Opera7で具合いが悪いようなので、代替スタイルシートを全部外してみました。
λ. 継承(or subtyping)とvariance
なるほど。やっぱりFAQだったのですね。(Eiffel FAQ,日本語訳)でしたか。ふむふむ、理論的な解決をしているわけではなく、コンパイラによるチェックまたは実行時の例外という扱いなのですね。
それから、Satherはこの場合contravarianceなのか。
2003-01-07 [長年日記]
λ. システムプログラミング
X11。今時XLoadFontやXDrawStringなんて特殊な目的でしか使わないのだから、FontSet系やXmb系のAPIの方を教えれば良いのに、と思わなくもない。
λ. ぎゃー
……とか言っていても仕方がないので、とりあえずダミーのClosedFunctorialExpressionを受け取れるようにして、length=prl(zero, succ.pi2) の型が「list(*a) -> nat」である事が計算できるようになった。ただ、これはあまりにも汚いので何とかしたいけど、木曜日に間に合わせるためには四の五の言ってられないか……
2003-01-14 [長年日記]
λ. アッカーマン関数と高階原始帰納関数
アッカーマン関数は原始帰納的でないので計算できないと思っていたら、萩野先生に「アッカーマン関数は高階原始帰納関数なので、exponentialを使えば書ける」と言われてしまった。ガーン。
自然数上での primitive recursion の定義は知っているけど、自然数に限定しない意味での primitive recursion はどのように定義されるのだろう?
2002-07-12に原始帰納関数と末尾再帰について書いたけど、nobsunさんはきっと自然数以外に対するprimitive recursionも考えていたんだろうなぁと想像。
2003-01-15 [長年日記]
λ. やばいやばいやばいやばいやばい……
λ. CPL
きゅぴーん!。curryがλ抽象に見えてキター
- K = curry(pi1)
- S = curry(curry(eval.pair(eval.pair(pi1.pi1, pi2), eval.pair(pi2.pi1, pi2))))
- I' = curry(I.pi2)
- K' = curry(K.pi2)
- S' = curry(S.pi2)
と定義する。当然「eval.pair(eval.pair(S', K'), K') = I'」は成り立って欲しいのだけど、実際に「simp full eval.pair(eval.pair(S', K'), K')」としてみると 「curry(eval.pair(eval.pair(pi1.pi1, pi2), eval.pair(pi2.pi1, pi2)). pair(pair(curry(curry(pi1).pi2. pair(pi1, pi2).pair(pi1, pi2).pair(pi1, pi2).pair(pi1, pi2).pair(pi1, pi2)), curry(curry(pi1).pi2.pair(pi1, pi2).pair(pi1, pi2).pair(pi1, pi2))).pi1, pi2))」 になってしまった。
FULL-C-FACTでEP,jがRそのものでない場合にはfactorizerの引数がelement(terminal objectをdomainとする射)でないので、通常の簡約を行えないのが原因。ad-hocな対処は簡単だけど、どうするのが良いのかな?
とりあえず、自己満足のために「eval.pair(eval.pair(S', K'), K')」の続きを手計算してみよう。
- = curry(eval.pair(eval.pair(pi1.pi1, pi2), eval.pair(pi2.pi1, pi2)). pair(pair(curry(curry(pi1).pi2), curry(curry(pi1).pi2)).pi1, pi2))
- = curry(eval.pair(eval.pair(pi1.pair(curry(curry(pi1).pi2), curry(curry(pi1).pi2)).pi1, pi2), eval.pair(pi2.pair(curry(curry(pi1).pi2), curry(curry(pi1).pi2)).pi1, pi2)))
- = curry(eval.pair(eval.pair(curry(curry(pi1).pi2).pi1, pi2), eval.pair(curry(curry(pi1).pi2).pi1, pi2)))
- = curry(eval.pair(eval.pair(curry(curry(pi1).pi2).pi1, pi2), eval.pair(curry(curry(pi1).pi2).pi1, pi2)))
- = curry(eval.pair(curry(pi1).pi2, curry(pi1).pi2))
- = curry(eval.pair(curry(pi1).pi1, pi2).pair(pi2, curry(pi1).pi2))
- = curry(pi1.pair(pi2, curry(pi1).pi2))
- = curry(pi2)
- = I'
2003-01-17 [長年日記]
λ. 言語の意味論
今回ばかりは敗北。徹夜してもレポート最後まで終わりませんでした。(T_T)
展望。
- Channel theory
- 例のあれ
- Institution
- Joseph Goguen がやっているとか。categoryを使っていてfunctorがinfomorphismに相当するらしい。
- Locale
- いわゆる pointless topology の理論(だと思う)
- Chu space
- 例のあれ
- Domain theory
- 例のあれ
- Semantic web
- ……
λ. 不定名詞句の指示と談話モデル
読んでないけど、言語の意味論のレポートを書いている途中に見掛けて、面白そうだったので。
λ. cpl.rbをデモ
cpl.rbをデモ……したのだけど、あんま面白く出来なかった。地味に動かしてみるだけじゃなくて、やっぱ絵になるものを用意しないとなぁ。
λ. 夕食
サイゼリア
2003-01-18 [長年日記]
λ. strict
strictの一般的な訳語って「正格」でしょうか。
λ. RONIN
を見た。これまで見たこの手の映画の中ではかなり面白かった。
2003-01-20 [長年日記]
λ. 論文読み会 "Fold and Unfold for Program Semantics"
この論文の前半について解説した。個人的にこの論文で面白かったのは polytypic fold/unfold をHaskellで表現するテクニックだったので、そこを取りあげられなかったのは少し残念。
つーか、CCSはカードキャプターサクラですか?
λ. 夕食
サイゼリア
λ. CPL
『どうせなので、単に実装しただけじゃなくて、こいつを利用して何か論文書けないかなぁ〜、でも「再実装しましたー」じゃ論文にならんしなぁ』とか思っていたら、未踏ユースにでも応募して何かやってみたらどうかと言われる。そっか、そういう選択もあるんだよなぁ。
2003-01-21 [長年日記]
λ. システムプログラミング
最後なのに質問一つなくて退屈だった。皆様他の授業で必死なんでしょうな。
λ. "Sketches: Outline with references"
を後で読んでみよう。
λ. CPLでアッカーマン関数
アッカーマン関数と高階原始帰納関数の続き。 書けた気がする。
- ack(0,y) = y+1
- ack(x+1,0) = ack(x,1)
- ack(x+1,y+1) = ack(x,ack(x+1,y))
は
- ack(0)(y) = y+1
- ack(x+1)(y) = ack(x)y+1(1)
と書き直せるので、
cpl> let times = eval.prod(pr(curry(curry(pi2)), curry(curry(eval.pair(eval.pi1, eval.pair(pi2.pi1, pi2))))), I) times : prod(nat,exp(*a,*a)) -> exp(*a,*a) defined cpl> let ack_0 = curry(s.pi2) ack_0 : *a -> exp(nat,nat) defined cpl> let ack_s = curry(eval.pair(times.pair(s.pi2, pi1), s.0.!)) ack_s : exp(nat,nat) -> exp(nat,nat) defined cpl> let ack = eval.prod(pr(ack_0, ack_s), I) ack : prod(nat,nat) -> nat defined
という感じで定義できる。確かに高階だけど原始帰納的な感じだ。
cpl> simp full ack.pair(s.s.s.0, s.0)
s.s.s.s.s.s.s.s.s.s.s.s.s.0.!
: *a -> nat
む、簡約後に型を再計算しているので、 簡約前よりも型が緩くなってしまう可能性があるのか。 これは不味いかなぁ。
2003-01-24 [長年日記]
λ. Re: Namazuと格闘。茶筅を使ってもうまく単語に分解することができない
良く分からないけど、茶筅がダメなら案山子を試してみるとか
λ. 社会と法 テスト
んなの知らねーよ。真面目に判例とか勉強してたのが馬鹿らしくなった。なんか気が収まらないので、東方妖々夢で時間を潰す。
λ. こないだのvarianceの話
C++で継承時にメンバ関数の返り値の型を共変化させることが出来るのなら、メンバ関数の引数の型に関してはどうかと思い試してみた。test_variance.cpp
継承時にメンバ関数の引数の型を変化させるとオーバーローディングと認識されてしまい、反変化も共変化も行えないようだ。
2003-01-25 [長年日記]
λ. Howto translate combinators into CPL
こないだのアイディアをもう少し整理して、具体的に翻訳を定義してみた。memo-0125.pdf
このメモを書いてから気が付いたのだけど、CCCは型付きλ計算のモデルなので、翻訳できるのは当たり前といえば当たり前なのか。
……というあたりで更に気が付いたのだけど、この翻訳結果にβ変換等の簡約規則に対応する書き換え規則を定義してやって、書き換えの間で対応が保存されている事を示せば、CCCの上で型付きλ計算のモデルを具体的に作ったことになるよね?
CCCが型付きλ計算のモデルであることの証明の中身自体は全然知らなかったので、自力でここまで到達出来たのは嬉しい。
2003-01-26 [長年日記]
λ. readline
でreadlineでコンテキストセンシティブな補完を実装するにはどうしたら良いのだろうと悩んでいたら、Enhanced Readline? というRCRがあった。
2003-01-27 [長年日記]
λ. 称賛なんかよりも心暖まる言葉が欲しい
λ. 雨が冷たい。凍えそう。君は今一体何処で何をしているの?
λ. テスト
コンパイラ構成論は特に準備していなかったけど(予想通り)何とかなった。知的財産権論は……どうなんだろ? 企業会計論は決算を何故するのかが書けなかったのが悔しい。「会計公準に基づいて」という事で無ければ書けたかもしれない。ともあれ、今学期のテストは一応これでお仕舞い。残る敵は——
2003-01-31 [長年日記]
λ. 研究会発表
無事に終わって一安心。これで今度こそ春休みに。
λ. 借りた本
- 『情報科学における論理』
- 小野 寛晰 [著]
- 『Information Flow: The Logic of Distributed Systems』
- Jon Barwise, Jerry Seligman [著]
