技術がどうのという話ではなくて、こんなことができるのだということに気づいてすぐに作って回るようにするというのが偉い。myGengo

雲をつかむような話といえば、coinductiveな証明。

モンテーニュのエセーが大好きで、いろいろと、わからない。わかるわけがない。いろいろ言われるが、そもそもそんなものは本当にあるのか。まぁ、文字列を書き写せるものがあるくらいのことくらいは認めるしかないような気がするので、そのくらいのものの存在だけ認めればできることをする。とりあえず。

Coders at WorkのSimon Peyton Jonesのインタビューを読んでみたら、けっこうおもしろい。

• 機械語を打ち込むところからプログラミングをはじめた話
• レジスタ一つを残してすべての記憶容量が計算結果で埋まるプログラムを組んだぜという話…自分で自分を上書きしていく
• 起業するには、金欠で元気が増す人じゃないと向いてないと思った話
• どんなつまらないことでもはじめてごらんという言葉に助けられた話
• プログラムが動かなくなるような変更はやめてなんて昔は無かった話

というような話があったような印象が残っている。

この3年間くらい、哲学者が思い悩むような問題が、なかなか問題に見えない。おそらく、一つのイデオロギーに取り込まれてしまいつつある。これは問題である。

曲を作って暮らしている人と、深夜の研究室でまったり話し合ってみた。

頼まれ仕事は、あんまり儲からないし、楽しくもないのだそうだ。これはソフトウェアづくりに似ていると思った。

てきとうに思いついたフレーズは、はなうたボックスにためてあって、それとは別に当座片付けなくてはならない仕事はいつも目の前においておいて、使えるときに使えるものを使いながら仕事をするらしい。なんだか自分の作業と似ている。

なんか、SEPのピタゴラスの項目に、The Pythagorean Way of Life という項目があって、どうやったら数学ができるようになるのか書いてあるのだと思って、見てみた:

• 犠牲を捧げる
• 肉を食べないかも。豆も食べないのかも
• 5年間沈黙すると入門できるらしい
• 理性をもつものには、神と人間と、ピタゴラス的ななにかの三種類がいるらしい。

難しいなぁ。

例によってTuring machineをencodeする。別にやり方が一つcanonicalに決まるというわけではない。堤防のどこかに穴を開ければ十分で、別に正しい位置に穴を開けたいわけではない。なんとかencodeできれば、なんでもよい。気楽。

とりあえず、半群。Turing machineのテープに書いてあることと、ヘッドの位置と、ヘッドの状態をまとめてwordで書くことにして、あとは、状態遷移を表す等式たちを入れると、有限表示 (finitely presentedってこの日本語?) な半群でTuring machineをencodeできる。半群のword problemは決定不能。

このとき作った半群の形は決まっているので、それを使って変な群を作る。もちろん、作った半群のwordに対応する群のwordがあるように作る。半群の word problemと、群のword problemが同じことになっていると嬉しい。

半群の中で、word同士がequalなことを使って、対応するword同士が群の中でもequalなのは、まぁあたりまえなんだ。るんるん。けれども、逆が難しい。群だと、両辺に左からなんかの逆元をかけて、あったものを打ち消したりできるし。そんなこと半群じゃ普通できないし。群のほうが、いろんな理由でequalになりうる。

ぐっとこらえて考える、半群のword problemを使うといっても、実は、どんなwordとどんなwordについてもequalか否か判定する必要はない。Turing machineの停止問題で頭がいっぱいのひとに聞かれるword problemの問題の形は決まっているので、それに対応した群のword同士が等しい場合に、半群の中のequalityを言えるだけで十分だ。大目的のためには、途中の結果に変な条件がついても気にしないことですね。Booneの補題というそうだ。

えぇ、Booneの補題の変な条件のおかげで、wordの形が決まっているので、群で1になるwordを一生懸命patten matchして、どういう形をしているのか細かく調べていけます。こういう群で1を表しているwordだから、こんな形をしているよね、という標準形定理をがんがん使う。読んだものだと、HNN拡張についての標準形定理(的ななにか)である、Brittonの補題ばっかり使っていた。なんでもpinchが存在するのだそうですよ。Pinchというのはつねるんですね。よくわかんないwordでも、つねったところからちぎりとると、もっと簡単な群の元になっているwordが取れる。これは嬉しい。まぁ、結び目をほどいていくのに似ていると言われるとそんな気もしてきた。

HNN拡張していくことによってpatten matchが効く群を作っていく手法って、似たようなことをすると、なんかへんてこりんな論理のmodelを作りたいときには便利かもしれん。