群のword problemの決定不能性

例によって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を作りたいときには便利かもしれん。