日々の流転

λ. データベース概論

wwwからccz03にruby-postgresで接続しようとしたら、#<PGError: No pg_hba.conf entry for host 133.27.4.212, user s01397ms, database s01397ms >。まさか、本当にpsqlコンマンドの出力を加工せよと? もう泣きたい。

λ. matrix.rb

ある commutative semiring の行列計算をmatrix.rbでやろうとして、matrix.rbはNumericの派生クラスしか対象にしていない事に気付く。仕方ないので0と1をそれぞれ加算と乗算の単位元にcoerceするようにして誤魔化す。

そういえば、[ruby-list:28917]とか[ruby-math:355]の話ってどうなったのかなぁ……

λ. Jenaで無名ノードを含むN-TRIPLEからModelにデータを読み込む

Jenaで無名ノードを含むN-TRIPLEからModelにデータを読み込む際には、3引数の方のreadを使ってURIのbaseを指定してあげなくちゃいけないのね。あぁ、こんな単純な事に一体何時間悩んでたんだろう……

λ. 妖々夢Extra: 721787560点

Extraをすこし頑張ってみる(replay)。721787560点。飯綱権現降臨で感覚が狂って3機ミスしてしまったのが悔しい。8億目指してたのにぃ。

λ. IO::Writable

「puts,print,printf,putc,<<をIOからIO::Writableみたいなモジュールに移せば良いのに」とruby-devに書こうとして[ruby-dev:15987]に気づく。危ない、危ない。

λ. ニダの司祭

彼ら「北朝鮮」は70年代初頭から営々と行動を始め、 日本から英国までを駆けずり回って膨大な日本人を集めて回り、 北朝鮮に移送したのだ。 料理店店員・整備員・主婦・中学生・大学生 etc etc、 小さな者は13歳から、大きな者は52歳まで。 なんで知ってるってるかって顔だね。 手助けしたのさ、我々(在日)が、強力にね。

ヘルシングのマクスウェルのネタ。不謹慎なのは分かってるけど、吹き出してしまったよ。

λ. GHC Version 6.2 (released 16 Dec 2003)

.

λ. ドラえも

Zinnia hacks tomorrow. (2003-12-17) より。いい味だしてるなぁ。

λ. 黒くひ単

ATOKで勝手に自主規制かまして出ない数々の凶悪な言葉を2500語ほどまとめてみました。

メモ。今も普通に使われている言葉がだいぶ含まれているけど、これが全部変換できないとしたら、ATOKって使い物になるのかしら。

λ. 借りた本

『重光・東郷とその時代』

岡崎 久彦 [著]

svnseeds’ ghoti! (2003-12-16)を読んで興味を持ったので、借りてみた。

λ. RHG読書会::東京 Reloaded

2週目終了。

λ. 『猫の地球儀 焔の章』, 秋山 瑞人 著, 椎名 優 イラスト

を読んだ。今頃になって読むのは、かなり今更な気もするけど。

λ. 第十ニ回圏論勉強会

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

写真

モナド=メイド説とかわけわからんてw　IOメイド, Readerメイド, Writerメイド, Stateメイド, Listメイド, ..., モナドカフェ...

ビーフン鍋は辛かったよ。

λ. 懸賞サイトの裏側(?)

先日、とある懸賞サイトのゲームのswfファイルをデコンパイル*1してみたら、絶対に当選しないようなコードになっていた。「〜が当たる」と書いてあるのに……これって不当表示じゃね?　そのサイトや他の個人サイトに書いてある当選者の声ってのもサクラなのかね。香ばしい世界だ。

まあそれはおいておいて、どうなっていたかと言うと、サーバ側を呼び出して結果がある条件を満たしたときには当選可能のフラグが立つようになっているし、当選時の処理もちゃんと書かれている。ただ、そのフラグを落とす処理が途中に入っているんだな。なんで、こんなことになっているのかを想像するとちょっと楽しい。 最初は宣伝効果を考えて当選を出してたけど、カモが十分増えたので、もう当選しなくしたとか?　でも、それならサーバ側を書き換えたほうが良さそうだしなぁ。単にバグというオチだったらつまらん。

λ. 『反社会学の不埒な研究報告』, パオロ・マッツァリーノ

結構面白かった。 リフレに関する記述など幾つかツッコミたい部分はあるが。

• スタンダード　反社会学講座
• 初版正誤表

λ. ddとダブルバッファリング(?)

ふと、「ddは読み込みと書き込みを別スレッドに分けて、ダブルバッファリングのようなことをしているのだろうか」というのが気になり、GNU　coreutils のソースを確認してみたが、特にそんなことは無いようだ。

λ. かも鍋

λ. Gabaマンツーマン英会話の無料体験レッスン

Gabaマンツーマン英会話の無料体験レッスンを帰りに受講してきた。

最初に20分くらい日本人のカウンセラとのカウンセリングで、現在の自分で思っているレベルや、目的・ゴールや、気になっていることなどを確認。その後、ネイティブスピーカのインストラクタと40分弱のレッスンをする。最初に目標などの話をしていたので、今回はレッスン部分は通常よりも若干短かった。

目標に関しては、以下のような感じに。

• needs English at work (conferences)
  • discussion
  • deal with travel situations

それで、Level 6 (Low Intermediate) の Conversation Strategies というのを薦められ、Conversation Strategies: Pair and Group Activities for Developing Communicative Competence(David Kehe/Peggy Dustin Kehe/Andrew Toos) をテキストに本来のレッスンを。 今回はテキストの最初の項目だった Rejoinder について。 テキストを簡単に見た後に、適当なテーマについて雑談しながら、テキストに出てきた受け答えなどを使ってみる。

レッスンの結果の現状分析は以下のようになった。

• Positive Points
  • relatively strong base
  • stronger listening skills
  • comfortable with familiar language
• Points to Improve
  • speaking
    • vocabulary (natural + formal)
    • quick response
    • express smoothly and clearly

「Points to Improve」に挙がった点は、自分でも弱いと思っていた部分なので、納得。 また、ICレコーダを使ってレッスンを録音して聞きなおすと良いというアドバイスをもらった。そういうことをさせて貰えるものだとは思っていなかったので、ちょっと嬉しい驚き。

その後、カウンセラとインストラクタと三人で結果について確認し、それからカウンセラとコースや見積もりの話に。教育訓練給付制度の対象になるコースだと、どの教室でもレッスンを受けられるオプションを付けられなくなってしまうのが、悩み所。

カウンセラの人もインストラクタの人も非常に好印象だったのだけど、他の英会話学校を知らないと比較も出来ないので、とりあえず次は他の幾つかの英会話学校の無料体験レッスンを回ってみるつもり *1。

2008-12-30 追記

ずっと、「ギャバ」と読んでいたが、読みは「ガバ」らしい。 ぐぐる先生に教えて貰った。

λ. 『独房の修道女』 Paul L. Moorcraft

独房の修道女 (扶桑社ミステリー)(ポール・L. ムーアクラフト/Paul L. Moorcraft/野口 百合子) を読了。 ケッチャムみたいなのを期待してたんだけど、ケッチャムのような陰惨・凄絶な物語ではなく、普通のエンターテイメントとして楽しめた。

Quotation

p.215

マーダは完全な沈黙、完全な闇の中に残されたが、自分を誇らしく感じた。少し前までは、絶望的な恐怖に震えるでくのぼうにすぎなかった。いまは、あの狂人を哲学的議論に引き込むことになんとか成功した。彼のルールに従っているようにふるまえばいい。あの男は彼女の心身を支配したがるだろうが、支配できるのは体だけだ。心は自分のものだ。そして、彼のゲームで彼を打ち負かしてやる。

λ. 関数型プログラマにとっての副作用

「Haskell に副作用なんて、あるわけないじゃん。大げさだなぁ」(死亡フラグ)と思っていたけれど、HAMA#3の話をみて自分の考え方を整理できた気がするので、ちょっと書いてみる。

入出力は副作用?

命令型プログラマに説明するときの便法としては、kazuさんの説明は確かに効率が良いとは思うものの、自分がこの説明をするのには結構抵抗がある。

どこに抵抗があるのかというと、その背後にある「入出力するなら副作用がある、Haskellは入出力する、だからHaskellには副作用がある。」というような考え方。 この考え方では、言語がどのようなものであろうと、最終的に実行時に計算機上の現象として入出力が発生すれば、副作用が存在するということになってしまう。 しかし、関数型プログラマにとって、副作用とはあくまでも言語や式の性質であって、実行時に計算機上で発生する現象のことではない。 だから、実行時の現象のことを指して「副作用」と呼ぶのは category mistake だと感じてしまう。

要は「副作用」の定義の違いなのだけど、実行時の現象を指して副作用と呼ぶことの不合理はいくつかあるように思える。

第一に、この呼び方だとC言語の処理系を副作用のない言語で実装すれば、C言語には副作用が存在しないことになってしまうのではないか、という点。C言語に副作用が存在することは多くの人が認めるところだと思うので、これは矛盾であるように思える。(副作用のない言語なんて存在しないというなら別だけど)

第二に、以下のようなCプログラムは副作用を持つか? という問題。

int main(int argc, char** argv)
{
     return argc;
}

このプログラムは、外部からコマンドライン引数という入力を受け取って、そしてステータスコードを外部に出力しているので、明らかに入出力のあるプログラムである。 したがって、入出力は副作用という考え方に従えば、副作用があることになる。 しかし、実際には多くのプログラマは「このプログラムには副作用は含まれていない」と考えるはず。

関数型プログラマにとっての副作用とは?

では、関数型プログラマは何を副作用と呼んでいるのか?

副作用という言葉は色々な意味で使われるけれど、狭義には状態を書き換えることを指す。さらに広い意味で使われることもあって、この広義の副作用は、effectと呼ぶことが多いのだけど、これは式が持つ値以外の意味の総称である。 これには値を求める際に発生する、狭義の副作用、入出力、非決定性、それから例外や大域脱出などの制御(controll)などが含まれる。 また、非停止性などもeffectと考えることがある。

したがって、関数型プログラマの言う「副作用がない」ということの意味は、「式の意味は値であって、値以外の意味を考える必要はない」ということ。この性質はしばしば「参照透明性」と呼ばれる(実は参照透明性の定義も色々あって、ややこしいのだけど)。

だから、最終的な現象として入出力が発生したとしても、それが言語の上で値以外の意味を導入しない形で実現されていれば副作用は存在しないと言うし、最終的な現象として入出力が発生しないとしても、値以外の意味が存在すれば副作用があるという。 (例えば、この意味で例外による大域脱出は副作用である)

副作用を用いずに入出力を記述する

では、副作用を用いずに入出力を記述するプログラミング言語は可能だろうか?

入出力を記述するには、要は入力と出力の関係さえ定義出来ればいいので、そんなのは別にどうとでもなる。

例えば、入力と出力がそれぞれ標準入力と標準出力しかないとしたら、入力と出力の関係を定義するには String → String という関数を定義すれば十分である。なので、そのような関数としてプログラムを記述することにすれば良い。 もちろん、これは非常に単純な場合しか扱っていなくて、問題も色々あるのだけど、副作用を用いずに入出力を記述するプログラミング言語が可能であることを示すには十分だろうと思う。

実際には標準入出力だけではなく、様々な種類の入出力を扱う必要があるので、実用的なプログラミング言語にするには、より一般的かつ柔軟な方法にする必要がある。 Haskellでは、過去には色々な方法が試みられていたけれど、今はIOモナドという方法に落ち着いている。 IOモナドを使う方法は、入力と出力の関係を String → String という関数で定義することに比べると遥かに複雑で巧妙な方法であるけれど、基本的な考え方には大きな違いはない(と思う)。

この話の目的はHaskellが採用している方法の詳細を説明することではないので、これで終わり。モナドやIOモナドについてのちゃんとした話はまたそのうち。

関連

• Haskellには副作用がないのか？ - あどけない話 (2009-06-27)
• Haskellに副作用はないのか？ - HaHaHa! (2009-07-02)
• 「Haskellで副作用のあるプログラムを作れることをどうやって説明したらいいの?」まとめ - みずぴー日記(2009-12-10)
• Haskellと副作用 - あどけない話 (2009-12-14)

λ. Beyond Classical Domain Theory by Alex Simpson

これは面白い。Synthetic Domain Theory って、昔、長谷川立氏のチュートリアル「パラメトリック・ポリモルフィズム」で

• 「この節では，パラメトリシティ原理を満たすモデルを幾つか紹介してみたい．いずれもかなり重たい数学を用いるので，深入りはしないことにしておく」
• 「もう1つのモデルは，直観主義的宇宙を用いる方法で得られる．これにはさらに難しい数学が必要なので，表面的なことを述べるだけにする」

と難しいことが随分強調されていたので、きっと難しいのだろうなと思って近づいていなかったんだけど、このスライドは分かりやすかった。effective topos とか realizability interpretation とか計算可能性とか、そういう難しいことを一切知らなくても、直観主義論理と圏論さえ知っていれば使えそうだと感じた。

そういえば、Synthetic Domain Theory については、長谷川真人氏の「自己言及の論理と計算」(参考: ヒビルテ(2003-06-29))の「Advanced Topic 直観主義的抜け道について」でも触れられていたな。ついでに、以下のように書いてあったので、今CLTT読書会で読んでいるCLTTにもそういう話が出てくるらしい。

これらの事柄はかなり専門的であり，今のところ研究論文以外に情報源はあまりないが，B. Jacobs: Categorical Logic and Type Theory (North-Holland, 1999) には，そのような直観主義的集合論のモデルに関するくわしい解説が含まれている．

以下、読んでいて気づいた点のメモや練習問題を解いてみたりしたもの。

Simple constructions (20)

集合の直積が集合なのは、A×B = {z | ∃x∈A, y∈B. z=(x,y)} = ∪_x∈A ∪_y∈B {z | z=(x,y) ∨ z=(x,y)} で、Indexed union axiom と pairing axiom から。

クラスA, 集合X に対してのクラス A^X の定義は、⊆の定義をクラスに一般化すれば、P(A)の定義もクラスに一般化されるので、Aが集合の場合と同じでよいはず。

• A⊆B ⇔ (∀x. x∈A ⇒ x∈B)
• P(A) = {z | z⊆A}
• A^X = {f ∈ P(X×A) | ∀x∈X. ∃!y∈A. (x,y)∈f}

Countable choice (22)

• axiom of choice を ∀x∈X. ∃y∈Y. φ ⇒ ∃f∈Y^X. φ[f(x)/y]
• countable choice を ∀n∈N. ∃y∈Y. φ ⇒ ∃f∈Y^N. φ[f(n)/y]

と書いてあるが、これらはそれぞれ

• ∀x∈X. ∃y∈Y. φ ⇒ ∃f∈Y^X. ∀x∈X. φ[f(x)/y] と
• ∀n∈N. ∃y∈Y. φ ⇒ ∃f∈Y^N. ∀n∈N. φ[f(n)/y]

の誤りだろう。

【2010-12-23 追記】 それはそれとして、型理論やBHK解釈に慣れ親しんでいると、選択公理は推論規則から自明に証明できてしまう気がするけど、こう書いてあるということは、ここではそうではないということで、なんだか少し気持ち悪い。どういう体系になっているのか、気になるところ。

Truth values (23)

⌜_⌝に関する幾つかの性質

• ⌜φ⌝=⊤ ⇔ {∅ | φ}={∅} ⇔ φ
• ⌜φ⌝=⊥ ⇔ {∅ | φ} = {φ | ⊥} ⇔ ¬φ
• X∈Ωに対して、∅∈⌜X=⊤⌝={∅ | X=⊤} ⇔ X=⊤ ⇔ ∅∈X より、 ⌜X=⊤⌝=X

以降では ⌜φ⌝=⊤ のことを単に ⌜φ⌝ と書いているようだ。

P(X) ≅ X→Ω の証明は、

• F: P(X)→(X→Ω)
  F(A) = {(x, ⌜x∈A⌝) | x∈X}
• G: (X→Ω)→P(X)
  G(f) = {x∈X | f(x)=⊤}

とおけば、

• GF(A) = {x | ⌜x∈A⌝=⊤} = {x | x∈A} = A かつ
• FGf = {(x, ⌜f(x)=⊤⌝) | x∈X} = {(x, f(x)) | x∈X} = f

なので言える。

Booleans (24)

Ω⊆2がLEM(排中律)と同値であることの証明。

LEMを仮定すると、以下より Ω⊆2

x∈Ω
⇒ (∃y. y∈x)∨¬(∃y. y∈x)  {- by LEM -}
⇔ x=⊤ ∨ x=⊥
⇔ x∈{x | x=⊤ ∨ x=⊥}=2

逆にΩ⊆2とすると、任意のφに対して、⌜φ⌝∈Ω⊆2 ⇒ ⌜φ⌝=⊤ ∨ ⌜φ⌝=⊥ ⇔ φ ∨ ¬φ なので、LEMが成り立つ。

Semidecidable properties and Markov's principle (25)

p,q∈Σ ⇒ p∧q ∈ Σ の証明

• p∈Σ より、P: N→2 が存在して p=⌜∃n∈N. P(n)⌝
• q∈Σ より、Q: N→2 が存在して q=⌜∃n∈N. Q(n)⌝

R(n) = P(π1(n))∩Q(π2(n)) とおくと、p∧q = {∅ | ∅∈p ∧ ∅∈q} = {∅ | ∃n∈N. P(n) ∧ ∃n∈N. Q(n)} = {∅ | ∃n∈N. R(n)} ∈ Σ

「p: N→Σ ならば (∃n∈N. p(n)) ∈ Σ」というのがあるけど、結論部は (∨_n∈N p(n)) ∈ Σ のことだろう。 ∀n∈N. p(n)∈Σ より ∀n∈N. ∃Q:N→2. p(n)=⌜∃m∈N. Q(m)=⊤⌝ で、ここで可算選択公理(countable choice)を使うと、 f : N→N→2 が存在して ∀n∈N. p(n)=⌜∃m∈N. f(n)(m)=⊤⌝ 。R(n) = f(π1(n))(π2(n)) とおくと、∨_n∈N p(n) = ∪_n∈N p(n) = {x | ∃n∈N. x∈p(n)} = {x | ∃n∈N. ⌜∃m∈N. f(n)(m)=⊤⌝=⊤} = {x | ∃n∈N, m∈N. f(n)(m)=⊤} = {x | ∃n∈N. R(n)=⊤} ∈ Σ

Towards synthetic domain theory (27)

N, 2, Q が fixpoint property を持たないこと。

Nの場合sが不動点を持たない。P={n∈N|s(n)≠n)とおくと、s(0)≠0なので0∈P、n∈Pとするとs(n)≠nなのでs(s(n))≠s(n)でs(n)∈P 。よって P=N 。

Ωの場合 not: Ω→Ω を not(x) = ⌜∅∉x⌝ とすると not(x)=x ⇔ ⌜∅∉x⌝=⌜∅∈x⌝ ⇒ ⊥ より、notには不動点が存在しない。

2の場合も、not を 2→2 に制限すれば同じ。

Basic propertis of probabilistic domains (66)

「Then (I,0,⊕) ⋌ η_D since (I,0,⊕) is an object of ProbDom'_⊥⊕」というのが理解できず悩んでしまったが、これはまさにユニットの性質そのもの。