日々の流転

λ. たしかに適度に勘違いしてるほうが幸せだとは思うのだけど……う〜ん。

休学も割とよく考えるのだけど、自分を高めるための当面の手段として、大学に通い続ける事以上の手段が思いつかないのが悲しいところ。

λ. 1+1=2 であることを証明できる?

ユークリッド幾何学で「正三角形の内角はすべて 60 °である」が証明できるのと同様に、「1+1=2」はペアノ算術で証明できますよん。去年の12/20に書いたペアノ算術の公理から、1 + 1 = s(0) + s(0) = s(s(0) + 0) = s(s(0)) = 2

それから、「実際，ブール代数は1+1=0 となる数学の一分野です」と書いてあるけど、そうだっけ? それってブール代数ではなくて、2を法とする演算なのでは?

λ. Classificationと情報射の圏

昨日の定義だと「対象のペア (X,Y), (X',Y') が異なる ⇒ Hom(X,Y)∩Hom(X',Y')=φ」が成り立たなかった。でも、射の定義を拡張して、⊨_X と ⊨_Y の情報も含むようにすればよいだけの事。

λ. Hassan Ait-Kaci: Warren's Abstract Machine --- A Tutorial Construction

WAMの解説としてはこの本が良いと誰かに薦められた事があるのだけど、この本オンライン版があるようです。http://www.isg.sfu.ca/~hak/documents/wam.html が元々のURLらしいのだけど、アクセスでいないので……

• http://host.di.uevora.pt/~pq/clp/wambook.pdf
• http://host.di.uevora.pt/~pq/clp/wambook.ps
• http://host.di.uevora.pt/~pq/clp/wamerratum.txt

λ. 読書

『遊戯王 28』

高橋和希[著]

λ. 色々せっぱ詰まってたり。ゴールデンウィークなのに……

λ. 床屋

へ行く。

λ. いろいろ

プリンセスチュチュ見忘れた。魔探偵ロキは見たのですが。

λ. call/ccによるshift/resetの表現

メモ。ぐるぐる。

def _abort(&thunk)
  v = thunk.call
  Thread.current[:__meta_continuation__].call(v)
end
 
def reset(&thunk)
  th = Thread.current
  mc = th[:__meta_continuation__]
 
  callcc{|k|
    th[:__meta_continuation__] = lambda{|v|
      th[:__meta_continuation__] = mc
      k.call(v)
    }
    _abort(&thunk)
  }
end
 
def shift(&f)
  callcc{|k|
    _abort{
      f.call(lambda{|v| reset{ k.call(v) } })
    }
  }
end
 
p 1 + reset{ 3 } #=> 4
p 1 + reset{ 2 * shift{|k| 4 } } #=> 5
p 1 + reset{ 2 * shift{|k| k[4] } } #=> 9
p 1 + reset{ 2 * shift{|k| k[k[4]] } } #=> 17

shift/reset その2に続く。

λ. GHC 6.4 ソースコードHacking: メモ

[haskell-jp:590]によるとテーマは「多言語化」らしいので、そのための個人的メモ。

HaskellのCharはUnicodeなので、同じく文字をUnicodeで扱っているJavaや.NET等のモデルが参考になるはず。

Unicode文字列⇔マルチバイト文字列 の変換

選択肢:

iconv + nl_langinfo(CODESET)

-

libcのmb⇔wc変換関数

現在の Hugs は --enable-char-encoding=locale でコンパイルするとこれを使う。wchar_tがUnicodeである環境(WindowsやLinux)では問題ないが、*BSD等はそうではないので問題となる。wchar_t がUnicodeかどうかを調べるには defined(_WIN32) || defined(__STDC_ISO_10646__) で良いと思う。

その他のライブラリ

the m17n library 等。libm17nはちょっと使ってみた感じでは結構良さそう。

自前でテーブルを持つ

これは出来たら避けたいな

IO周りで、Unicode⇔マルチバイト の変換

基本的には GHC.IO を書き換えればよい。GHC.IOBase と GHC.Handle も参照。

FFI周りで、Unicode⇔マルチバイト の変換

Foreign.C.Stringを書き換えればよい。参考: Hugsへのパッチ

Text.Regex

参考: GHC 6.2 で Oniguruma を使うためのパッチ

コンパイラがマルチバイトで書かれたソースファイルを処理できるように?

IO周りを対応すれば自動的に対応できる?　プリプロセッサでエスケープするようにすればコンパイラ自体に手を入れる必要はない?

複数のエンコーディングを同時に使うためのAPI?

-

the m17n library のGUI周りと Input Method 周り?

-

CHISE とのインターフェース?

-

HsLocale

アレな部分もあるけど、パクれそうなコードがある。 HsLocale-win32.diff

λ. 第六回圏論勉強会

圏論勉強会も今回で六回目。今回はブラウワー(Brower)の不動点定理のセクションだったのだけど、このセクションは何度読んでも面白い。今回も、これまで「なんとなく」で読み飛ばしてしまっていたところを掘り下げることが出来て興味深かった。やっぱり、色々な視点があるっていいな。

それから、たけをさんがmixiにコミュニティを作ってくれました。mixi:圏論勉強会。

写真

λ. GHC ソースコードハッキング 1日目

圏論勉強会後にちょとと遅めの昼食をとり、そのままGHCソースコードハッキングへ。

とりあえず、the m17n library を使ってみる流れに。

λ. 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 って漢字だと「罗朝晖」と書くのでしょうか?

関連

• 強い直和?

λ. キャリーケースをゲット

クレジットカードのポイントでキャリーケースをゲット。 申し込んだのが数日前だったので、今回の大分行きには間に合わないかと思ったが、間に合って良かった。UFJニコス GJ!

λ. 『アンティゴネー』

古典と現在の授業で紹介されていた アンティゴネー (岩波文庫)(ソポクレース/呉 茂一) を読んだ。

λ. Amazon クレジットカード が届いた

数日前に申し込んでいたのがもう届いた。 まだ仮なので、本人確認書類を返送。

Amazon クレジットカードは作っておいて損のないカードだと思うよ。 年会費無料だし、Amazonでの買い物¥2000分キャッシュバックがあるし、ポイントがAmazonのギフト券になるし。

【2007-09-11追記】 ただし、<URL:http://www.edynavi.tv/aboutedy/edycharge/creditcard.php>によると「シティカードはご登録いただけません」とのことで、AmazonカードもEdyにチャージするのには使えないようだ。 残念。

λ. monadic logic

Monadic Logic で検索して <URL:http://www.cs.tau.ac.il/~rabinoa/logic6-1-04.pdf> というスライドを発見。 monadic logic の satisfiability が decidable であることの証明と、あと指標 {<, =} からなる有理数上の論理式がdecidableであることの証明が面白かった。

λ. 雑誌

家を整理していたら、学生時代*1の懐かしい雑誌が出てきたっぽい。