2003-09-16
λ. いろんな事が思うようにいかない。ちょっと疲れた。
λ. Re: 続・NP完全問題を解く決定性アルゴリズムについて
なるほど。勉強になります。先日の駄文を書いた甲斐がありました (^^;)
λ. Comonad (2)
先日読んだ "Codata and Comonads in Haskell" のコードは本当に動くのかと思って、Hugsで試してみる。echoは確かに動くのだけど、自分で
stdPutString :: String -> OI () -> ()
stdPutString [] t = coeval (t .>> ())
stdPutString (x:xs) t = coeval (t .>> x =>>
stdPutChar =>>
stdPutString xs)
とか定義して、「stdPutString "hogehoge" stdOI」とかやっても、何も出力されない。何がまずいのだろう。
λ. GUNSLINGER GIRL アニメ化
楽しみ。
λ. バイト
7-zipで圧縮しなおすと、jarファイルがちょっぴり小さくなるそうだ。サイズを小さくするために出来るのは、あとはクラスファイルのObfuscationくらいかなぁ……。とりあえず、幾つかツールをメモ。後で比較してみよう。
λ. 影鷹 - 縦書きブラウザ
影鷹（かげたか）は HTML を縦書きに表示するためのソフトです。最終的には Intenet Explorer や Mozilla などのようなブラウザを目指していますが、今はまだ普通の HTML（Javascript などを使っていない）を表示するのがやっとの状態です。
メモ。
2004-09-16
λ. 「東方戰騎譚」エキスパート攻略のようなもの
雪さんすきすき日記 (2004-09-11) より。ちなみに私はいまだノーマルの「死霊の舞踏」が抜けれていませぬ(最近はあんま挑戦してないけど)。
2006-09-16
λ. Mule-UCS は JIS X 0213 の文字を UTF-8 で保存できない?
Meadow2.xでMule-UCSを使っているのだけど、バッファ中に JIS X 0213 の文字(例えば⊗とか≅とか)が含まれていると、UTF-8で保存できなくて困ってしまう。UTF-8のファイルを読み込むときには JIS X 0213 の文字として読み込むくせに、保存できないというのは微妙すぎ。ひょっとして、Meadow3.x(Emacs22)では直ってたりするのかな……
【2006-09-26追記】 Meadow 3.x にしたけど解決しなかった。Mule-UCS を外してしまって、JIS X 0213 系のエンコーディングは jisx0213 without Mule-UCS で読み書きするようにすれば良い?
【2006-10-01追記】
<URL:http://www.m17n.org/mlarchive/mule-ja/200208/msg00014.html> によると、un-define-safe-charsets-for-coding-systemsにjisx0213がないためで、unicode-basic-translation-charset-order-listを設定すれば良かったらしい。
そのようにしたら解決した。
λ. 『ふつうのHaskellプログラミング』読書会
今日読み終わるかと思っていたけど、まだ続く。
λ. 『ハッカーズ』
PDFで半分公開されているので読んでみた。
結構引き込まれるものがある。
2007-09-16
λ. ヘンキン文
先日、「H↔Provable([H]) な H の真偽」というクイズを書いた。 反応が全く無くて少し寂しかったのだけど、忘れないうちに簡単な解説を。
この論理式はヘンキン文(Henkin sentence)と呼ばれていて、その名の通り1950年頃にヘンキンによってその真偽が問題にされたそうだ。 そして、この論理式が真であることは Löb によって1955年に示されている。 以下に簡単に証明するが、なかなかトリッキーで面白い。
- Löb, M. H. 1955. Solution of a problem of Leon Henkin. Journal of Symbolic Logic, vol. 20, pp. 115-18.
前提
証明可能性は可導性条件(derivability conditions)と呼ばれる以下の条件を満たす。
- D1
- T ⊢ P ⇒ T ⊢ Provable([P])
- D2
- T ⊢ Provable([P→Q]) → Provable([P]) → Provable([Q])
- D3
- T ⊢ Provable([P]) → Provable([Provable([P])])
また、不動点定理が成り立つ。すなわち、任意の一変数論理式 P(x) に対して、ある論理式Qが存在して T ⊢ Q↔P([Q]) が成り立つ。
証明
H は T ⊢ H↔Provable([H]) を満たすとする。
まず、不動点定理によって、ある論理式Dが存在して T ⊢ D ↔ (Provable([D])→H) を満たす。
S := Provable([D])→H とすると T ⊢ D → S
D1を適用して T ⊢ Provable([D → S])
D2を適用して T ⊢ Provable([D]) → Provable([S])
Sを展開してもう一回D2を適用して T ⊢ Provable([D]) → Provable([Provable([D])]) → Provable([H])
D3より T ⊢ Provable([D])→Provable([Provable([D])]) なので、T ⊢ Provable([D]) → Provable([H])
Hの定義より T ⊢ H↔Provable([H]) なので、T ⊢ Provable([D]) → H
Dの定義より T ⊢ D ↔ (Provable([D])→H) なので T ⊢ D で、D1 より T ⊢ Provable([D])
T ⊢ Provable([D]) と T ⊢ Provable([D]) → H とにMPを適用して T ⊢ H
様相論理との関係
Provable([X]) を □X と書くことにすると、D1は必然化に、D2はKに、D3は4に対応する。 さらに不動点定理に対応するものを様相論理で公理化して……という話があるがそれはまたそのうち。
![[かつ泉の看板]](./images/20070916_0.jpg)
2008-09-16
λ. 『ウルトラダラー』 手嶋 龍一
ウルトラ・ダラー(手嶋 龍一) を読んだ。だいぶ前に「伊藤洋一の Round Up World Now」で紹介されていて、読もうと思っていた本。人物描写は微妙だと思ったが、内容はとても面白かった。そういえば、ライトノベルとかでないちゃんとした小説を読むのはずいぶん久しぶりだ。
λ. Agda2 on Meadow
darcsレポジトリからとってきたAgda2のスナップショットをMeadow3の上で動かそうとした。
README の記述は NTEmacs22 を想定したものになっていて、ucs-fonts と mule-fonts をインストールして設定する方法が書いてあったけど、それらのフォントは基本的にはMeadowのパッケージで入っているはずなのでその辺りは無視。 そうしたら、「File mode specification error: (error "No fonts match `-misc-fixed-medium-r-normal--18-120-100-100-c-90-iso8859-1'")」と言われてしまった。
仕方ないので、READMEの記述に従おうとしたが、Meadowだとフォント周りはNTEmacsと若干異なっている部分があるみたいで、どうもうまくいかない。 結局、.emacsに「(setq agda2-fontset-name nil)」と書き、agda-mode.elの以下の部分をコメントアウトしたら、解決した。
(if window-system
(create-fontset-from-fontset-spec agda2-fontset-spec-of-fontset-agda2 t t))
2009-09-16
λ. 有限領域での推移閉包の公理化
昨日も書いたように、推移閉包は一般には一階述語論理では表現できないので、領域を有限に限定した場合でも領域のサイズの上限 n に依存した形、たとえば以下のような形でしか表現できないと思い込んでいた。
- ∀x,y. Tk(x,y) ⇔ R(x,y) ∨ σ1 ∨ … ∨ σn-2
- where σn := ∃z1,…,zn. R(x,z1) ∧ R(z1,z2) ∧ … ∧ R(zn-1,zn) ∧ R(zn,y)
Automating First-Order Relational Logic なんかでも、「The transitive closure is obtained by applying an operator that computes closure using iterative doubling, as explained in [15].」と、もう少し賢いけれども、やはり領域のサイズの上限に依存した形を使うとあったし……
だけど、これは誤りで、昨日も言及した“First-Order Logic as a Lightweight Software Specification Language - The ETPTP Toolkit”(Michel Rijnders) によると、モデル発見器 Paradox の作者の Koen Claessen が、(有限領域の場合の)領域のサイズに依存しないような形式化を考えた*1そうだ。 この論文では反射推移閉包の場合で説明していて、関数記号 s と関係記号 C を新たに導入して、以下のような公理を導入する。
- (I1) ∀x. T(x, x)
- (I2) ∀x, y. R(x, y) → T(x, y)
- (I3) ∀x, y, z. T(x, y) ∧ T(y, z) → T(x, z)
- (E1) ∀x, y. T(x, y) ∧ x ≠ y → R(x, s(x, y))
- (E2) ∀x, y. T(x, y) ∧ x ≠ y → T(s(x, y), y)
- (C1) ∀x, y. ￢C(x, x, y)
- (C2) ∀x, y, z, v. C(x, y, v) ∧ C(y, z, v) → C(x, z, v)
- (E3) ∀x, y. T(x, y) ∧ x ≠ y → C(x, s(x, y), y)
説明されてみれば「なるほど」と思うのだけど、こんな方法があったのかと感動した。 Koen Claessen すげー
本当に出来ているか Alloy で確認する
本当に反射推移閉包を公理化できているか、例によってAlloyで確認してみる。
まずは上記の公理をAlloyで書いてみる。今回はちょっとAlloy風に書いてみた。
sig U {
R : set U,
T : set U,
s: U -> one U,
C: U -> U
}
fact {
all x : U | x in x.T
R in T
T.T in T
all x : U, y : x.T | x!=y => (s[x,y] in x.R and y in s[x,y].T)
all x, y: U | not (x->x in y.C)
all v : U | (v.C) . (v.C) in v.C
all x : U, y : x.T | x!=y => x->s[x,y] in y.C
}
pred show() { }
run show
assert T_is_RTc_of_R {
all x : U | x.T = x.*R
}
check T_is_RTc_of_R for 6
それで、「run show」を実行すると、
Executing "Run show" Solver=minisat(jni) Bitwidth=4 MaxSeq=4 SkolemDepth=1 Symmetry=20 939 vars. 75 primary vars. 1308 clauses. 34ms. Instance found. Predicate is consistent. 19ms.
というような感じで、反射推移閉包になっている例が出てくる。 Nextを押して更に幾つか例を作ってみても、どれも反射推移閉包になっているっぽい。
それならばと、今度は「Check T_is_RTc_of_R for 6」を実行すると、
Executing "Check T_is_RTc_of_R for 6" Solver=minisat(jni) Bitwidth=4 MaxSeq=6 SkolemDepth=1 Symmetry=20 7640 vars. 516 primary vars. 12305 clauses. 136ms. No counterexample found. Assertion may be valid. 617ms.
という感じで、6要素までの領域では確かに反射推移閉包になっているようだ。
さらに、SATソルバーとして「Minisat with Unsat Core」を選択して、「Check T_is_RTc_of_R for 6」を実行すると、今度は Core というのが出てきて、以下のようにソースがハイライトされる。 ハイライトされている部分は、ここから論理式をひとつでも取り除いたら、反例(TがRの反射推移閉包になっていない例)が発見できてしまうような論理式の集合を表している。 この場合には公理全体が含まれているので、どの公理もTがRの反射推移閉包であることを表現するのに欠かせない公理であることがわかる。
*1 Koen Claessen の元のテクニカルレポート Expressing Transitive Closure for Finite Domains in Pure First-Order Logic は、残念ながらオンラインにはないみたいだ。
