日々の流転

λ. Epilogue for Epigram

うひょ、Epigramの開発についてのブログがあったのね。これは読まねば。

ちなみに、Epigramは依存型(dependent type)をサポートした強力な関数型言語。自然演繹のスタイルでプログラムを書くのとxemacsが必要なのがとっつきにくいけど、色々と注目してる。特に注目してるのは、proof-irrelevance, observational equality, codata 辺りの議論。

関連エントリ

• Epigram
• Why Dependent Types Matter.
• Extensional Equality in Intensional Type Theory.
• Codata

λ. 知識発見法とか古川研の勉強会とか

知識発見法の授業に初出席(ぉ。Prologは懐かしいけど正直どうでも良い。早くProgolの話とかに入って欲しいなぁ。実は、この授業四年前に一度聴講したんだよな。当時は帰納論理プログラミングという科目名だったが。当時の私は今の私と比べても格段に無知で、理解できない点が多くて悔しかったので、そのリベンジを果たしたい。

それから、古川研のAbduction勉強会に飛び入り参加。いろいろあって勉強会自体は中止になってしまったけど、雑談は結構楽しかった。ちなみに、読んでいた論文は An Abductive Event Calculus Planner 。私は最初のほうしか読んでないがプランニングや発想推論(Abduction)については結構分かり易かった。それから、こういうことをやってる人はやっぱり一階述語論理が好きっぽいな。

あと、金城(kinjo)さんとなんか色々話した。

• コンピューターサイエンス・エンジニアリング系研究会
• 統計力学じゅーよー
  • Thermodynamics and Garbage Collection (.html, .ps.gz)
    • (追記: 20060904#p02も参照)
• ゲーム理論
  • ゲーム意味論(Game Semantics)
    • <URL:http://www.cogs.susx.ac.uk/users/guym/papers/marktoberdorf.ps.gz>
    • <URL:http://web.comlab.ox.ac.uk/oucl/work/samson.abramsky/gsem/index.html>
  • 決定性公理(AD,Axiom of determinacy)
  • あとなんだっけかな
• グラフマイニング
  • 古川研:ネットワーク分析およびグラフマイニングをつくる会
• 学習理論とモンテカルロ法
• 還元公理(axiom of reducibility)の問題
• 他にも色々

λ. CCの後継色々

CC(Calculus of Constructions)を発展させた型理論には色々あるが、それぞれどういう関係にあるんだろう。どっかに系統図とかないかな…

• GCC (Generalized Calculus of Constructions)
• ECC (Extended Calculus of Constructions)
• UTT (A Unifying Theory of Dependent Types)
• CIC (Calculus of Inductive Constructions)

λ. “ECC, an Extended Calculus of Constructions” by Zhaohui Luo

• <URL:http://citeseer.ist.psu.edu/luo89ecc.html>
• <URL:http://jp.citeulike.org/article/612085>

とりあえず、ECCの定義だけ確認した。ECCはCCに強い依存直和(strong dependent sum)と型の階層(cumulative type hierarchy)とを導入したもの。CCに強い依存直和を追加したものではジラールの逆理が成り立ってしまうことが知られているので、どうするんだろうと思っていたんだが、型の階層を導入し強い依存直和の規則をpredicativeなものにすることで回避している。

また、型の階層は Prop⊆Type₀⊆Type₁⊆Type₂,…のような階層になっていて、一番下のPropの依存直積だけはimpredicativityを許している。例えば ∏(A:Prop).(A→A)→A→A はPropに属するので、Recursive types for free!の方法で再帰的データ型を表現可能(c.f. AgdaのようなMartin-Löf流のpredicativeな型システムだとこれは不可能)。

欠点としてはη簡約とsurjective-pairingを含まないことがある。それらを追加するとチャーチ・ロッサー性が成り立たなくなる。

ところで、Zhaohui Luo って漢字だと「罗朝晖」と書くのでしょうか?

関連

• 強い直和?

λ. ストリームの表現

ストリームの直観的な表現はsigを使った次のような表現だが、この定義はtermination checkerに怒られる。

Stream :: Set -> Set
Stream A = sig
             head :: A
             tail :: Stream A

別の定義として以下のようなものが考えられるが、今度はストリームを生成する関数がtermination checkerに怒られることになる。

data Stream (X::Set) = SCons (x::X) (xs::Stream X)

from :: Nat -> Stream Nat
from n = SCons n (from (succ n))

実のところ、agdaにはcodataを扱う機能がないので、ストリームのようなcodataを直接扱うことは出来ない。そこでストリームと同型でかつagdaで表現可能なデータ型を考える。ストリームの直観的な意味は無限個の直積 A^ω なので Nat -> A という関数型として表現することが考えられる。基本的な演算も同時に定義すると以下のようになる。

Stream :: Set -> Set
Stream A = Nat -> A

head (|A::Set) :: Stream A -> A
head s = s zero

tail (|A::Set) :: Stream A -> Stream A
tail s = \n -> s (succ n)

unfold (|A,|X::Set) :: (X -> A × X) -> (X -> Stream A)
unfold phi x n =
    case phi x of
    (a,x)->
        case n of
        (zer  )-> a
        (suc m)-> unfold phi x m

この表現で一つ嫌な点は外延性が成り立たない点。つまり Ext = (A::Set) -> (s1,s2::Stream A) -> ((n::Nat) -> Id (s1 n) (s2 n)) -> Id s1 s2 は要素を持たないし、双模倣(bisimulation)の関係にあるストリームが等しいことも一般には証明できない。内包的(intentional)な型理論の世界で作業している以上仕方がないところではあるが、これはやっぱし嫌な感じだし、ある程度の外延性を持った型理論がいいなぁ……

ところで、このストリームの表現は Representations of First order function types as terminal coalgebras. の対応を逆に使ったものなので、他のcodataにも同様の方法で表現できるものがある。しかし、νX. 1+A×X のように直和が入ってくるとこの方法では表現できないと思うし、やはり組み込みのcodata対応は欲しいところか。OTT(Observational Type Theory) と Observational Epigram (Codata参照) に期待。それから、IsabelleやCoqではcodataの扱いはどうなってるんだろう。Coqはcodataをサポートしているらしいが…

【2007-09-11追記】 直和が入ってくるような場合でも、20070905#p01のようにすれば表現可能。

λ. yhcの仮想マシンについて調べる

ふと、yhcの仮想マシンとバイトコードについて調べてみた。 結構シンプルだ。

• Yhc/RTS
• Yhc/RTS/hbc
• Yhc - Bytecode Documentation

YARVアーキテクチャと少し比べてみる。yhcのコードをYARVで動かすことを考えると、スタックのトップ以外の要素を操作する命令がもう少し欲しくなりそうか。

λ. 焼肉

λ. 『ファイブスター物語 12巻』

を読んだ。個人的に見所だったのは、ダイ・グの苦悩とクリスティンの決意。それから、KOGがガクガクブルブルしてるのにウケた。いや、ストーリーよくわかってないんだけどね。

Quotation

もう泣かぬ……
もう恐れぬ

戦と血しか知らずに死んでゆくことを
恐れることはもうない

たとえ花壇に花は咲かずとも
私はもう一生に足りる恋をした！

陛下に赤子を千人殺せと言わるれば殺そう！
一国を滅ぼせと言わるればこの手で灰にしよう！

これ以上何を望むか！
生きる証はここにある！

λ. 知識発見法と古川研勉強会

• <URL:http://bruch.sfc.keio.ac.jp:5130/dsweb/View/Collection-1867>
• <URL:http://bruch.sfc.keio.ac.jp:5130/dsweb/Get/Document-13375/11-54-13-23-1.ppt>
• 窃盗犯にさせられるソクラテスwww
• 発想推論 + イベント計算 = Plannning
• ATMS = assumption-based truth maintenance system
• Prologメタインタプリタによるアブダクション。Prolog楽しい。<URL:http://web.sfc.keio.ac.jp/~mukai/2006-LP/04/practice/meta.html>
• 古川研:Abduction勉強会

λ. RubyKaigi 2006

チケット予約。 一時間かそこらで売り切れたそうなので、間に合って良かった。

λ. 『ビジョメガネ』

みんなメガネ好きだよねー

λ. ディスクトラブル

またもやディスクトラブル。RAID使ってても避けられないトラブルがこう続けてくると、呪われてるんじゃないかという気がしてくる。そして、復旧作業をあまり手伝えずにごめんなさい。

λ. 今日のITシステム

• Matteo Baldoni, Cristina Baroglio, Nicola Henze. Personalization for the Semantic Web. Reasoning Web 2005: 173-212 <URL:http://www.springerlink.com/openurl.asp?genre=article&id=doi:10.1007/11526988_5>
• B. Rachlevsky-Reich, I. Ben-Shaul et. al.: GEM: A Global Electronic Market System. In: Information Systems Vol. 24 No. 6, 1999, 495-518 <URL:http://citeseer.ist.psu.edu/rachlevsky-reich99gem.html>
• 自分のやりたいことで、キーとなるテクノロジーは何か?
• 中間発表では、予想される結論は言うべき。

λ. ロバ文と依存型と

「Every farmer who owns a donkey beats it.」のような文をロバ文(donkey sentence)といい、一階述語論理の限量子では適切に量化出来ない例として良く知られている。が、ふとこれは依存型の存在するある種の型理論で「∏x:(∑f:Farmer. ∑d:Donkey. own(f,d)). beat(p1(x), p1(p2(x)))」みたいに表現すればいいじゃんと気づいた。

でも、喜んだのは一瞬だけで、調べたらそんなアイディアは Ranta さんらによってとうにやりつくされているのでした。俺なんかがふと思いつく程度のアイディアは誰かにやられていて当たり前だけどね。たはは。

しかし、強力な型理論で自然言語の意味論を扱うのは結構面白そうだ。それに、考えてみればMontagueの理論は個体,真理値,内包的指標からなる単純型付きラムダ計算に基づいていると言えるわけで、この方向は必然だったとも思う。

λ. 鳳梨酥

台湾のお土産らしい。

λ. Game Semantics. Samson Abramsky and Guy McCusker.

• <URL:http://www.cogs.susx.ac.uk/users/guym/papers.html>
• <URL:http://citeseer.ist.psu.edu/abramsky99game.html>
• <URL:http://jp.citeulike.org/article/625286>

だいぶ前にsyd_sydさんのところで紹介されていたのでざっと読んだ。後半面倒くさくなって真面目に追ってないが、雰囲気は分かったし面白かった。ただ、形式化があまり直観的でないと感じた。もっと分かり易い形式化が可能なのではないかという気がしてならない。あと、big-stepの操作的意味論は存在は知ってたけど初めて見たよ。

λ. 久しぶりに向井先生と雑談

久しぶりに向井先生と雑談してきた。 以下メモ。

• TeX
  • Powerdot
  • \begin{proof}\end{proof}で囲むと最後にQEDの四角がつく
  • 集合の内包表記では \mid を
  • \align
• 斜体(skew field)
  • どの辺りが skew なんだろう
• イデアル(ideal)
  • 連続関数全体のなす環　連続関数環
    • 元の空間がコンパクト(?)だと、連続関数環から元の空間が復元できる?
    • 連続関数環の極大イデアルが元の空間の点を表す?
    • ある点で0にするような多項式の全体は極大イデアル
    • 極大でないイデアルは想像上の(fictionalな)点を表してると考える
  • forcing と generics
  • idealとfilterが双対
  • 昔はこういう話は良く分からなかったけど、CABAの極大フィルタ(ultra filter)が集合の点に対応する話とかを知った今は、だいぶイメージ出来るようになった気がする。
    • Stoneは凄い
      • 「1930年代に M.H. Stone はブール代数の表現定理を証明し，ブール代数が豊かな数学的内容を持つことを示した．当時まだ一般的概念としては存在しなかった可換環の素イデアルの空間(スペクトル)とカテゴリーにおけるアジョイントの概念が実質的に用いられているという，時代に先駆けた結果である．」(田中俊一『位相と論理』より引用)
• プロセス代数
  • 関係を保存する代数という意味で「代数」と呼んでいるのか?　例えば自然数と不等号の場合 a≦b ならば a+c ≦ b+c 成り立つが、同様のことがプロセスと遷移関係についても言えるので。
• クリフォード代数 <URL:http://en.wikipedia.org/wiki/Clifford_algebra>
• 検証
  • 様相論理での program = modal operator という見方
  • ホーア論理はもう古いと、ホーアさん本人が言ってたとか
• indexed-category, fibration, Grothendieck construction
• Higher Operads, Higher Categories. <URL:http://www.maths.gla.ac.uk/~tl/book.html>
• 『入門Haskell—はじめて学ぶ関数型言語』
  
• 『数学基礎論講義—不完全性定理とその発展』
  

λ. Haskellの複素数計算

404 Blog Not Found:%w(Complex Number).reverseで「Pythonやその他のLLに関しては、他の人によるdemoきぼんぬ」とあったので、Haskellでも試してみよう。Haskellではiやeは定義されていないのでまずそれらを定義しておく。

import Complex

i :: RealFloat a => Complex a
i = 0 :+ 1

e :: Floating a => a
e = exp 1

で、ghciで試す。

Main> i
0.0 :+ 1.0
Main> pi
3.141592653589793
Main> e
2.718281828459045
Main> e**(i*pi)
(-1.0) :+ 1.2246063538223773e-16
Main> exp (i*pi)
(-1.0) :+ 1.2246063538223773e-16
Main> log (-1)
NaN
Main> log (-1) :: Complex Double
0.0 :+ (-3.141592653589793)

Haskellには暗黙の型変換は一切ないが、型クラスを用いて定数や演算を多重定義しているため、さほど不便さを感じることはない。それから、log(-1) の結果が他の言語での πi ではなく -πi になってる。これはまあどっちでも良いわけだけど、どうして違ってしまっているかは気になる。

それから、誰かML系の言語でのdemoをきぼんぬ。

……と書いたら速攻でOCaml版が! そして、SML版とGCaml版も。

• OCaml
  • jijixi's diary - OCaml の複素数計算
  • 晩ごはんの履歴 - OCamlの複素数計算
  • どーんとやってみよう - OCaml の複素数計算
• SML
  • Garage uenoB - SMLの複素数計算
• GCaml
  • soutaroにっき - GCamlで複素数

Cの複素数計算

おまけ。

#include <complex.h>
#include <math.h>
#include <stdio.h>

void cprint(const char* const expr, const double complex x)
{
    printf("%-9s = %g+%gi\n", expr, creal(x), cimag(x));
}

int main(int argc, char** argv)
{
    cprint("pi", M_PI);
    cprint("e", M_E);
    cprint("e**(i*pi)", cpow(M_E, I*M_PI));
    cprint("exp(i*pi)", cexp(I*M_PI));
    cprint("log(-1)", clog(-1));
    return 0;
}

実行結果

pi        = 3.14159+0i
e         = 2.71828+0i
e**(i*pi) = -1+1.22461e-16i
exp(i*pi) = -1+1.22461e-16i
log(-1)   = 0+3.14159i

λ. オイラーの式

Matz日記より。

そういや、私もオイラーの等式は「へ〜、そうなんだ。すごいね〜」くらいに思ったことはあるが、それ以上に感動した記憶はない。というか、今でも解析系の話はよく分からないし(汗。そんなわけで、すずきひろのぶさんが「オイラーの業績は、オイラーだけを見てもあんまり意味がなくって、歴史的文脈で読まないとわからない。だから公式を一個をとりあげてすごいとかいう奴は本当の天才か、あるいはインチキがどちらかですよ。」と言っているのを見て、なんだか安心した。

λ. A groupoid model refutes uniqueness of identity proofs. Martin Hofmann and Thomas Streicher.

• <URL:http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=316071>
• <URL:http://www.citeulike.org/article/602344>

を読んだ。groupoidの圏とfibrationを使って、Idの要素がequalityでなくgroupoidのendomorphismを表すようなモデルを作る話。そうすると、nontrivialなendomorphismが存在するgroupoidについてはIdは複数の要素を持つ。言っていることはそんなに難しくはないのだが、indexed-category とか presheaf とか fibration とか grothendieck construction とか 2 category とかに不慣れ*1なことと、一部にインフォーマルな表記がされていることから、きちんと追いかけるのが大変だった。大変だったけどその分これらに少しは馴染めたような気がするが……

まあ、なんにせよ、Propositional equality の証明の equalityでの悩みはとりあえず解決か。

λ. NやList(N)のUIP

上記論文によると、NやList(N)のような型に関しては「UIP is actually syntactically derivable in the presense of a universe」らしいのだが、どうやるのかわからん。とりあえずゼロの場合は以下のように証明出来たのだが……

--#include "Hedberg/SET.alfa"
open SET use Id, refId, Unit, tt, Nat, zero, succ

Lem (x,y::Nat) (p::Id x y) :: Set
  = case x of
      (zer  )-> case y of
                  (zer  )-> Id p (refId zero)
                  (suc m)-> Unit
      (suc m)-> Unit

lem (x,y::Nat) (p::Id x y) :: Lem x y p
  = case p of
      (ref z)-> case z of
                  (zer  )-> refId (refId z)
                  (suc m)-> tt

prop (p::Id zero zero) :: Id p (refId zero)
prop = lem zero zero p

【2006-05-18 追記】 二日くらい必死で考えてようやく証明できたが……これ死ねるよ*1。termination-checkerは通らないけど、引数が小さくなっているのは明らかだからとりあえず良いよね。綺麗に書き直すのはまた今度ということで。それはそうと、Universeの強力さを初めて実感した。

--#include "Hedberg/SET.alfa"
open SET use Id, refId, substId, Nat, zero, succ, Zero

uipNat (n::Nat) (p::Id n n) :: Id (refId n) p
uipNat =
    let T (|n1,|n2::Nat) (p::Id (succ n1) (succ n2)) (q::Id n1 n2) :: Set
          = case q of
              (ref x)-> Id (refId (succ x)) p 
        lemT (x,y::Nat) (p::Id x y) :: Set
          = case x of
              (zer   )->
                  case y of
                    (zer   )-> Id (refId zero) p 
                    (suc y')-> Zero
              (suc x')->
                  case y of
                    (zer   )-> Zero
                    (suc y')-> (q::Id x' y') -> T p q
        lem (x,y::Nat) (p::Id x y) :: lemT x y p
          = case p of
              (ref n)->
                  case n of
                    (zer  )-> refId (refId zero)
                    (suc m)->
                        \(q::Id m m) ->
                        let lem2 :: Id (refId m) q 
                            lem2 = uipNat m q
                            lem3 :: T p (refId m)
                            lem3 = refId (refId (succ m))
                            lem4 :: T p q
                            lem4 = substId (\q -> T p q) lem2 lem3
                        in lem4
    in case n of
         (zer  )-> lem n n p
         (suc m)-> lem n n p (refId m)

λ. 人狼審問 : (1453)ホームズからの挑戦状

観戦中。

関連リンク

• 「推理とは何か実験村」実行委員会
• B1/1453村 - 人狼ファンWiki
• マーガレット(raruさん)の感想

λ. 単相性制限 (monomorphism restriction)

<URL:http://d.hatena.ne.jp/a-san/20060511>の話。 普段は気にしないし、避けるのは難しくないのだけど、こういうときに説明に困ってしまうな。

メモ。

• <URL:http://www.sampou.org/haskell/tutorial-j/pitfalls.html#sect12.3>
• <URL:http://haskell.org/onlinereport/decls.html#sect:monomorphism-restriction>
• <URL:http://hackage.haskell.org/trac/haskell-prime/wiki/MonomorphismRestriction>

λ. ブルバキとモーニング娘。と

<URL:http://d.hatena.ne.jp/yaneurao/20060514> での「ブルバキみたいなやっちゃな」「そう、日本ではモーニング娘。ていうんだよ」というやり取りが少し面白かった。

λ. 知識発見法

Rudolf Carnap の Confirmation ?

今期はProgolではなくAleph (A Learning Engine for Proposing Hypotheses)というシステムを使うそうだ。

聞くところによるとAlephはProgolよりも速いらしい。Cで書かれたProgolよりもPrologで書かれたAlephの方が速いと言うのは何かムカつく(苦笑　Windows版のYap-5.1.1で実行したら「YAP OOOPS: likely bug in YAP, segmentation violation.」で落ちる。Linux版のYapだと問題なく実行出来た。SWI-Prolog は5.2.6 だとエラーで、5.6.12 だと問題なく実行できた。

簡単なサンプルを実行してみたがなかなか面白い。調子に乗ってリストのinterleaveを学習させようとしたが、正負の事例の与え方がまずいのか、パラメータの指定がまずいのか、すごく時間がかかり結果が出てこない。後で、色々試してみよう。

λ. 古川研:Abduction勉強会

An Abductive Event Calculus Planner の 3.1 An Abductive Meta-Interpreter for the Event Calculus 。

メタインタプリタを部分評価する際に効率的な評価順に。結果としては幅優先の評価順のようになっている。

Close World Assumption と Clark's Completion。ここでは述語に関する情報が前もって完全に分かっているわけではないので、これらの条件は成り立っていない。そのため、否定を単純なnegation-as-failureで解釈してしまってはまずい。そこで、失敗を確認したゴールを記録しておき、residueが変更されるごとにそれらが(依然として)失敗することを再チェックする。面白い。

λ. 今日の写真

λ. Towards Observational Type Theory. Thorsten Altenkirch and Conor McBride

• <URL:http://www.cs.nott.ac.uk/~ctm/ott.pdf>
• <URL:http://www.citeulike.org/user/msakai/article/585944>

Extensional Equality in Intensional Type Theory の話を発展させたもの。前の論文では proof irrelevance が本質的な役割を果たしていると思っていたが、実際にはそれほど本質的ではないというのにまず驚いた。

(詳しくは後で書く)

OTTは理論的にも面白いし、実用的にも便利そうな型理論だと思う。Epigramを使ってみたくなった。

λ. 高校の勉強ムズス

• 接弦定理なんて知らね
• 漢文の返り点の結合順位を誰か教えてくれ

λ. バグ?

以下のゴールをrefineしようとすると、「Id |(Wrap A) (In a1) (In a2) = ?197 is unsolvable since Expression a1 is not equal to a」等と言われてしまう。この文脈ではa,a1,a2の間には definitional equality が成り立っていないといけないと思うので、これはバグっぽい気がする。

--#include "Hedberg/SET.alfa"
open SET use Id, refId, Zero

data Wrap (A::Set) = In (a::A)

Bug (A::Set) (x,y::Wrap A) (p::Id x y) :: Set
Bug = case x of
        (In a1)->
            case y of
              (In a2)->
                  let f (q::Id a1 a2) :: Set
                      f = case q of
                            (ref a)->
                                {! Id p (refId (In a)) !}
                  in Zero

λ. モデル検査法のソフトウェア検証への応用. 中島震

コンピュータソフトウェア, Vol.23, No.2 (2006), pp.72-86.

を読んだ。 チュートリアルというよりはサーベイのような気がしないでもない。

λ. John Major's equality

最近のAgdaにはagda-show-contextというコマンド(キーバインディングは「C-c |」)が実装されていて、これを使うと現在のコンテキストから見えるシンボルの一覧が表示できる。で、何も読み込んでいない状態で、これを実行してみたところ、幾つかの基礎的なデータ型やモナドと一緒に以下のようなシンボルが表示されているのを見つけた。

JMeq :: (A::Set) -> (x1::A) -> (B::Set) -> (x2::B) -> Set
same :: (A::Set) |-> (x1::A) |-> JMeq A x1 A x1

どうやらJMeqの唯一のデータ構築子(あるいは導入規則)がsameのようだが……これは何じゃ!?　JMeqで検索してみると、Coq-Clubメーリングリストの[Coq-Club] Playing with equalityというスレッドが見つかった。

なるほど。予め型が等しいと分かっていない二つの値を等号で結ぶための型で、(inductive familyとしての)通常の除去規則とは異なった除去規則を持っている。そして、通常の等号の型IdにUIPを追加したものと等しいと。この辺りから想像がつくが、内包的な型理論の内部では定義出来ない。そこで、CoqのCoq.Logic.JMeqではAxiomを使って定義している。agdaでもpostulateを使って同様に定義する方法もあったと思うが、agdaは組み込みの型としてJMeqのパターンマッチを特別扱いしているようだ。JMeq A a A aのような型の値には通常はcaseが使えないようチェックされているが、JMeqの場合には引っかからずにcaseが使えるできる。

それから、John Major's equality という名前が最初に使われたのは C. Mc Bride 氏の PhD thesis の Dependently Typed Functional Programs and their proofらしい。そのページのp.119に由来が書いてあった。John Major ってどっかで聞いたことのある名前だと思ったら……

It is now time to reveal the definition of ≃, the ‘John Major’ equality relation.² John Major's ‘classless society’ widened people's aspirations to equality, but also the gap between rich and poor. After all, aspiring to be equal to others than oneself is the politics of envy. In much the same way, ≃ equations between members of any type, but they cannot be treated as equals (ie substituted) unless they are of the same type. Just as before, each thing is only equal to itself.

---

² John Major was the last ever leader of the Conservative Party to be Prime Minister (1990-1997) of the United Kingdam, in case he slipped your mind.

classless society ってメージャー首相の言っていたいわゆる「階級なき社会」ってやつですね。それから、Epilogue に書いてあった「telescopic」という言葉についても p.120 に書いてあった。

λ. 箱の中のカードがダイヤである確率

ニャー速。 - この問題おかしい!!*1 より。

ジョーカーを除いたトランプ５２枚の中から１枚のカードを抜き出し、表を見ないで箱の中にしまった。そして、残りのカードをよく切ってから３枚抜き出したところ、３枚ともダイアであった。このとき、箱の中のカードがダイヤである確率はいくらか。

λ. ミニ丸シーサー

ちょっと前になるが、沖縄のお土産に貰った。可愛い。

λ. 向井先生の Haskell 講習会 (RHG読書会)

雨が降りそうで、なんか面倒になったので欠席(ぉぃ

• RHG読書会::東京 Revolution::ふつうのHaskellプログラミング
• 発表資料

λ. Extensible datatypes. Andres Löh

を読んだ。

λ. Inductive Types for Free

を読んだ。

• Containerは存在自体は知っていたが、嬉しさがようやく理解できた
• strictly positive の定義は?
  • 【追記】 下の Representing Nested Inductive Types using W-types の方に書いてあった。
• LCCC = locally cartesian closed category
• Representation Theorem 面白い
• Martin-Löf category = LCCC + W-types
• 「M-types can be constructed from W-types」というのはどうやるのだろう?

λ. Representing Nested Inductive Types using W-types

• <URL:http://www.cs.nott.ac.uk/~txa/publ/icalp04.pdf>
• <URL:http://www.cs.nott.ac.uk/~txa/publ/>

∑_A: C/A → C が π_B^*: C/A → C/∑_AB の左随伴というのは何を言っている?

coproduct が disjoint であるときに、A+B ⊢ C ⟼ (A ⊦ κ^* C, B ⊢ κ'^* C) で定義されている関手 C/A+B → (C/A)×C/B がequivalenceになるのがどうしてなのか、わからない。

λ. 順序数をプログラミング言語の中で実現する

以前に順序数の概念を理解するために書いたコードがあるので、そのときのコードを晒してみます。といっても、当たり前のことを当たり前に書いただけのコードですが。

-- ストリーム
data Stream a = Stream a (Stream a)

instance Functor Stream where
    fmap f (Stream h t) = Stream (f h) (fmap f t)

unfold :: (s -> (a,s)) -> (s -> Stream a)
unfold phi = h
    where h s = case phi s of
                (a,t) -> Stream a (h t)

-- 順序数
data Ordinal
    = OZero
    | OSucc Ordinal
    | OSup (Stream Ordinal)

add :: Ordinal -> Ordinal -> Ordinal
add a OZero     = a
add a (OSucc b) = OSucc (add a b)
add a (OSup b)  = OSup (fmap (add a) b)

mul :: Ordinal -> Ordinal -> Ordinal
mul a OZero     = OZero
mul a (OSucc b) = add (mul a b) a
mul a (OSup b)  = OSup (fmap (mul a) b)

pow :: Ordinal -> Ordinal -> Ordinal
pow a OZero     = OSucc OZero
pow a (OSucc b) = mul (pow a b) a
pow a (OSup b)  = OSup (fmap (pow a) b)

omega :: Ordinal
omega = OSup (unfold (\a -> (a, OSucc a)) OZero)

• OSupの引数のストリームには何らかの正規化のようなことを行うべきだろうか?
• 増大列でない列を排除するのは依存型を使うのが自然だろうけど、GADT等を使ってHaskellで無理やりやる方法はないだろうか?

λ. 今日のITシステム

• The Internet and the future of Financial Market. <URL:http://www.e-businessforum.gr/content/downloads/Internet_and_FinancialMarkets.pdf>

λ. 『よつばと! 5』

読んだ。 『よつばと!』はいいなぁ。

グウゼンの積み重ねで「そこにある日常は決して珍しいものでなく、あちき達が通ってきた道なんだよなぁと再確認。そのディティールが描かれているから凄い」と書かれていたので、そういや自分が子供の頃はどうだったかなぁと思ったのだけど、正直子供の頃のことはあまり覚えていない……ちょっと哀しくなった。

Quotation

やどかり
家を借りてるからやどかり

だれにかりてるの！？

え？　……貝？
いつかえすの！？

…たぶんこいつはかえさない

かえせよ！
でもかわいい！
きにいりました！
ぐるぐるだし

λ. ソーシャルブックマークサービスっておいしいの?

流行から遥かに遅れた話だが、ふとソーシャルブックマークとやらを使ってみたくなった。そこで、とりあえずMM/Memoを使いはじめてみた(<URL:http://1470.net/mm/mylist.html/813>)。しかし、ソーシャルブックマークサービスにも色々あるみたいで、どれを選んだらよいのか良く分からない。del.icio.usとかの方が便利なのだろうか?

λ. 推定無罪

を見た。そこまで面白いとも思わないが、雰囲気と結末は好き。

λ. ガロア理論について雑談

研究会の前にちょっとお邪魔して雑談。 ガロア理論について色々と聞く。 ガロア理論、興味はあるんだけどねぇ……

• 『群の発見』は群の「こころ」がわかる良い本らしい。
• Francis Borceux の『Galois theories』はガロア理論を圏論等の近代的な道具で整理したとか。ちなみに、この人は『Handbook of categorical algebra I』なんて本も書いている
• 順序集合(poset)の随伴(adjunction)を galois connection と呼ぶのは結局何故?　昔から気になって仕方が無い。ガロア理論は群の圏と体の圏の一種の随伴を考えるらしい(?)が、その辺りと何か関係ある?　仮にそうだとして、現在の定義に一般化される経緯はどのようなものだったんだろうか?
• 「群・環・体—ガロア理論入門」
• ガロア理論 - その標準的な入門. 中野伸 <URL:http://www.saiensu.co.jp/magazine-htm/spsk-200309.htm>
• xⁿ - 1 = 0 をベキ根で解けるというガウスの定理
  • ガロア理論で重要
  • ガウスの証明は複雑だが、ガロア理論ではあっさり証明できるらしい

ガロア理論で思い出したが、飯田君は元気だろうか……

λ. 古川研:Abduction勉強会

• 「resolve(G,R,Gs) :- member(G,R).」のGsは[]の間違いだと思われる。
• 工夫したnegation-as-failureで否定を扱うのではなく、メタインタプリタで述語に応じた特別な書き換えを行うことの理由がイマイチ良く分からない。

λ. Ruby-GNOME2 再び

久しぶりにRuby-GNOME2のソースをいじっている。 なんだか少し懐かしい。

λ. sinθ+cosθ=3/2 のとき、sinθ×cosθはいくつか？...

面白い。よくこんなの捻り出したなという感じ。 少し悩んでしまった。

私はmixi日記の方を先に読んでしまったのだけど、それよりは「ちょっと感心したパズルの問題」「昨日の問題のつづき」をこの順序で読んだ方が楽しめると思う。

λ. 第十七回圏論勉強会

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

慶早戦で授業は無し、と思ったら大学院の授業は普通にあるのだな。すっかり忘れていて、さぼってしまった。

λ. 古川研:Abduction勉強会

3.2 Protected Links, Threats, Promotions and Demotions。保護リンクがclippedの否定が保たれることで実現されるのはわかったが、PromotionとDemotionに対応する順序がどこで導入されるかが良くわからなかった。

λ. 博士号を取得するとは

帰り道の途中で博士号を取得するとはどういうことかという話が耳に入った。政治学の人のようだ。むちゃくちゃ要約すると「研究は質よりも量。教授をうんざりさせられれば勝ち。量は誠意」という話。結構嫌な気分になる。

λ. アニメ版「夢使い」

アニメ版の「夢使い」をちょっと見た。これはこれで面白いとは思うが、結構複雑な気分。原作は、倒錯的で妖しい雰囲気とか、オカルティックなところとか、あるいは異様なまでの描き込みによって表現された「異界の歪んだ空気」みたいなものとか、そういった雰囲気が大好きだったのだが、アニメ版はそういう雰囲気は無くて、なんというか無難で健康的な雰囲気になってしまっている。そして、毒が抜けた分元気がないというか……。原作を再現する必要はない*1し、あれをアニメでやるのは不可能だとは思うが、やはり残念。ただ、キャラクターの絵と声は良かったと思う。

• 夢使い★公式サイト

λ. 今日のITシステム

• 「これをやって修論になるのかな」「なるんじゃない、するんだ」
• 絶賛迷走中
• 技術を出発点にすると論文書きにくい。「何が不便か」を出発点にすると比較的書きやすい。
• 組み合わせられるテクノロジーは何か?
• 「これを解決しました」というのが言えるとよい。

λ. "Youtube to me" 改造版

Greasemonkeying with Google Video and YouTube が便利そうだったので使おうとしたのだけど、期待通りに動かなかったので、ちょっと改造してみた。youtube_to_me.user.js

【2007-09-29追記】 久しぶりに使おうとしたら、flvのURLが変わっていて使えなくなっていた。 仕方ないので直したが、javascriptを忘れていて焦る。

λ. 部分評価

<URL:http://alohakun.blog7.fc2.com/blog-entry-306.html> より。

流石に「Lispのマクロ展開」とか「融合変換」は部分評価とは呼ばない気が……。だって、それらはそもそも「評価」の一部ではないと思うし。

(後で部分評価について少し書く)