2008-10-28 [長年日記]
λ. Seven Trees やっと解けた
一部で流行っていた Seven Trees の問題。 乗り遅れてしまって、等式変形をどうやるのか一人寂しく悩んでいたのだけど、Tn + Tn+3 = Tm + Tm+3 が成り立つことに気づいて、ようやく等式変形が出来た。
- 1 + T3 = 1 + T2 + T4 = T + T4 = T(1 + T3)
- 帰納法により 1 + T3 = Tn + Tn+3
- よって Tn + Tn+3 = 1 + T3 = Tm + Tm+3 for all n, m
- ゆえに T = T0+T2 = T0+(T1+T3) = T1+(T0+T3) = T1+(T4+T7) = (T1+T4)+T7 = (T6+T9)+T7 = T6+(T7+T9) = T6+T8 = T7
等式変形が出来たら、同型の証明をAgdaで書こうと思ってたのだけど、関数として書くのが案外面倒そうなので、なんだかもういいやという気分になってしまった。 しかし、中野さんの5種類のパターンの分岐で定義ってのは分からなくて、気になるなぁ。
> 一部で流行っていた<br>ものすごく狭い「一部」でね :-)<br>> 5種類のパターン<br>これは全然わかりませんねー。
> ものすごく狭い「一部」でね :-) <br>まあ、それは(^^;<br>でも、もっと流行ってもいい問題だったと思うんですけどね〜
Blassの論文の20stepsからなる同型から11種類の分岐が得られるのですが、これを圧縮すると<br><br>[0,0,0,0,0,0, (7a,(7b,(7c,(7d,7e))))] → (7a,(7b,(7c,(7d,(7e,0)))))<br>[0,0,0,0,0,0,7] → 7 <br>[0,0,0,0,0,6,7] → (0,(0,(0,(0,(7,6)))))<br>[0,0,0,0,(5a,5b),6,7] → (5a,(5b,(6,(7,0))))<br>[1,2,3,4,5,6,7] → (1,(2,(3,(4,(5,(6,7))))))<br><br>の5種類のパターンになるんで、こんな感じのものじゃないかなぁ。
あのー、横レスですが<br>＞こんな感じのもの<br>も何も、Blassの論文にはダイレクトな5分岐の答えが載ってるじゃないですかｗ
中野さんの導いた5種類のパターンはこれとは違うかもしれない、という思いがふとよぎって、こんな表現をしてしまいました。すんません。
ryoさん、たけをさん、ありがとうございます。<br>Blassの論文を読んでみようと思います。
Blassの論文と中野さんの解答を読みました。<br>中野さんの解答はryoさんのパターンとほぼ同じものでしたね。<br><br>＞たけをさん<br>Blassの論文では、Proof of Theorem 1 に相互に重ならない11個のパターンによるものは書いてありましたが、ryoさんの解答のような優先順位つきの5個のパターンによるものは明示的には書いてないような……<br><br># Blassの論文の構成的集合論に関する部分が良く分からない…… orz
へ？？いや、あんまりマジメに読んでないし（ごめんなさい）、今もちょっとマジメに読む余裕がないので流し読みですが、Proof of Theorem 1 にあるのって、Case1〜Case5で場合分けされてる奴でしょ？<br><br>＞5個のパターンによるものは明示的には書いてない<br>別に「相互に重ならない11個のパターン」も明示されてないように思うし、Case1〜Case5を都合よく並べ替えて得られる5個のパターンの方が、11個のパターンを考えるより遥かに自明に思えるんですけど？？実際、上のryoさんの書いたパターンって、Case1から5の並べ替えですよね。<br>あれ、何か勘違いしてるのかなぁ。だったらごめんなさい。
まず、Case 1 〜 Case 5 は There are eleven p's and eleven corresponding q's と書かれているように実際には11個のパターンからなっていて、続く説明からこれらのパターンは自明に得られます。また、パターンが相互に重ならない事は very explicit の定義に含まれています。<br><br>で、「ダイレクトな5分岐の答えが載ってる」って書いてあったので、順序を導入して重なりを許した場合についても明示的に書いてあるのかと思ってたら、それが書いてなかったので「あれ?」っと思ったというだけです (^^;<br>結局、Proof of Theorem 1 の Case 1 〜 Case 5 のことだったようなので、疑問は解決しました。
んー、やっぱりひっかかるだけど、「パターンが相互に重ならない」とか「順序を導入して重なりを許す」って、どういう意味？パターンが相互に重なるケースって、どういうケース？<br><br>Case1が事実上4つ、Case5も4つあって正確には全11パターンあるのはそりゃそうだけど、それはどれも、考慮せずにパターンマッチでCase1、Case5でまとめて書けますよね。<br>さっき書いた「5個のパターンの方が、11個のパターンを考えるより遥かに自明」ってのは、そういう意味だったんだけど…
ここで二つのパターン p, q が重なると呼んでいるのは、それらが単一化可能なこと(ある代入θが存在して pθ=qθ が成り立つこと)です。例えば、Blassの11個のパターンは相互に重なり合わないですが、上の [1,2,3,4,5,6,7] と [0,0,0,0,0,0,7] は θ={1:=0, …, 6:=0} によって単一化可能なので重なり合います。<br><br>「順序を導入して重なりを許す」と書いたのは、要は普通の関数型言語のようなパターンマッチにするということです。<br>{(pi,qi)}_i∈I に対応する very explicit function f は piθ を qiθ に写像する関数として定義されるわけですが、もし pi と pj が重なり合ってしまうと、x=piθ=pjθ に対する f(x) の値が qiθ と qjθ で定まらないので、fが関数にならない可能性があります。それを避けるためにIに順序を導入して、x=piθ=pjθ に対する f(x) の値を i<j ならば qiθ にするということ。<br><br>> 正確には全11パターンあるのはそりゃそうだけど、それはどれも、考慮せずにパターンマッチでCase1、Case5でまとめて書けますよね。 <br><br>……というようなことがBlassの論文には書いてなかったので、「ダイレクトな5分岐の答え」がどこを指しているのか、最初分からなかったという話です。<br>自明と言われればそれまでなんですが。
ああ、なんか聞き方が悪かったですね。面倒な説明をさせてしまって申し訳ない。それならそれで僕の理解と合ってます。<br><br>一応論文にも We refrain from explicity exhibiting the results of this splitting of cases. とはあるんで、文意からして5パターンで考えればよい、という事だと思います。まぁ、「ダイレクト」ではないかもしれませんけど。