コラッツ予想がとけたらいいな
■ このスレッドは過去ログ倉庫に格納されています
525 名前:132人目の素数さん[sage] 投稿日:2012/09/03(月) 18:24:27.22 http://d.hatena.ne.jp/righ1113/ コラッツ予想について、証明を考えてみました。 ご指摘ご意見ご感想など、ぜひよろしくお願いします。 次に、8個1/12ステップの[0,0,0,0,1,1,1,1,1,1,1,1]の全ての順列に対して、上3つを除外します。 またもやHaskellですwww import Data.List (permutations, nub) cycleN :: Int -> [Int] -> [Int] -> [Int] cycleN 0 la _ = la cycleN x la lb = cycleN (x-1) (la++lb) lb remove_0_0 :: [Int] -> Bool remove_0_0 [_] = True remove_0_0 (0:0:xs) = False remove_0_0 (_:x1:xs) = remove_0_0 (x1:xs) remove_1_1_1 :: [Int] -> Bool remove_1_1_1 [_,_] = True remove_1_1_1 (1:1:1:xs) = False remove_1_1_1 (_:x1:x2:xs) = remove_1_1_1 (x1:x2:xs) remove_1_1_0_1_1 :: [Int] -> Bool remove_1_1_0_1_1 [_,_,_,_] = True remove_1_1_0_1_1 (1:1:0:1:1:xs) = False remove_1_1_0_1_1 (_:x1:x2:x3:x4:xs) = remove_1_1_0_1_1 (x1:x2:x3:x4:xs) *CollatzPatt> let multi=filter remove_1_1_1 $ filter remove_0_0 $ nub $ permutations [0,0,0,0,1,1,1,1,1,1,1,1] ←1時間ぐらいかかる *CollatzPatt> filter remove_1_1_0_1_1 $ filter remove_1_1_1 $ map (cycleN 2 []) multi [] 空リストになったので、(※)が証明できました。 Xsを12ステップで区切った時、8個以上1が入る事はありません。(※) Coq版できました。 ただnub permutationsの部分がCoqでは12時間計算しても終わらなかったので、 そこだけHaskellで495行出力して(それでも1時間かかる)、permu.vに書いています。 permu.v Require Import List. Definition nub_permu: list (list nat) := ((0::0::0::0::1::1::1::1::1::1::1::1::nil):: (1::0::0::0::0::1::1::1::1::1::1::1::nil):: ---略--- (1::1::1::1::1::0::1::0::0::1::1::0::nil):: (1::1::1::1::1::1::0::0::0::1::1::0::nil)::nil). collatz06.v Require Import Omega. Require Import List. Require Import Coq.Program.Wf. Require Import permu. Fixpoint cycle{A} (n:nat) (la:list A) (lb:list A) :list A := match n with | 0 => la | S m => cycle m (app la lb) lb end. Fixpoint remove_0_0 (l:list nat): bool := match l with | nil => true | _::nil => true | 0::0::_ => false | l1::ls => remove_0_0 ls end. Fixpoint remove_1_1_1 (l:list nat): bool := match l with | nil => true | _::nil => true | _::_::nil => true | 1::1::1::_ => false | l1::ls => remove_1_1_1 ls end. Fixpoint remove_1_1_0_1_1 (l:list nat): bool := match l with | nil => true | _::nil => true | _::_::nil => true | _::_::_::nil => true | _::_::_::_::nil => true | 1::1::0::1::1::_ => false | l1::ls => remove_1_1_0_1_1 ls end. Fixpoint beq_list (l:list nat) (m:list nat): bool := match l,m with | nil, nil => true | nil, _ => false | _, nil => false | l1::ls, m1::ms => if beq_nat l1 m1 then beq_list ls ms else false end. Fixpoint elem (x:list nat) (l:list (list nat)): bool := match l with | nil => false | l1::ls => if beq_list x l1 then true else elem x ls end. Fixpoint nub (l:list (list nat)): list (list nat) := match l with | nil => nil | l1::ls => (if elem l1 ls then nil else (l1::nil)) ++ (nub ls) end. Definition bnt_nat (x:nat) (y:nat): bool := if beq_nat x y then false else true. Fixpoint concatMap (f:nat->list (list nat)) (l:list nat): list (list nat) := match l with | nil => nil | l1::ls => (f l1) ++ concatMap f ls end. Fixpoint replace (x y:nat) (l m:list nat): list nat := match m with | nil => l | m1::ms => if beq_nat x m1 then replace x y (y::l) ms else replace x y (m1::l) ms end. Program Fixpoint permutations (l:list nat) (cnt:nat) {measure cnt}: (list (list nat)) := match cnt with | 0 => ((nil)::nil) | _ => match l with | nil => ((nil)::nil) | ls => concatMap (fun x => (map (fun y => x::y) (permutations (filter (bnt_nat x) ls) (cnt-1)))) ls end end. Next Obligation. omega. Qed. Definition multi1: list (list nat) := filter remove_1_1_1 (filter remove_0_0 (* (nub (map (replace 2 0 nil) (map (replace 3 0 nil) (map (replace 4 0 nil) (map (replace 5 1 nil) (map (replace 6 1 nil) (map (replace 7 1 nil) (map (replace 8 1 nil) (map (replace 9 1 nil) (map (replace 10 1 nil) (map (replace 11 1 nil) (permutations (0::1::2::3::4::5::6::7::8::9::10::11::nil) 12)))))))))))) *) nub_permu). Definition multi2: list (list nat) := filter remove_1_1_0_1_1 (filter remove_1_1_1 (map (cycle 2 (nil)) multi1)). Theorem multi2_is_nil: multi2 = nil. Proof. compute. reflexivity. Qed. やっぱQed.が通ると気持ちが良いですね。 俺じゃ理解できないけどどうやら進んでるようで、おめ ちょっとは読みやすくなったと思います。 https://drive.google.com/file/d/0B_FTpAj7C52FZGNTSXBTWkw3cGc/view?usp=sharing ----- 「ライトエッジパターン」というものを定義する。 これは、右端が繰り上がった時は1、そうでない時は0を置くものである。 x=319のライトエッジパターンは、[-,0,1,1,0,1,0,1,1,0,1,0,1,0,1,1,0,1,1]である。 ----- >>1 コラッツパターンとかライトエッジパターンとかよくわからん。 もし余力があればideoneにプログラム上げてくれんか? 好きな数を入力してそれに対してそのパターンを出力してほしい。 http://ideone.com/ haskellも選べるからたぶんもうすでに書いたものがあるだろ? Excelマクロでも良いですか? https://drive.google.com/file/d/0B_FTpAj7C52FVHlFNWt4UU1Vb3M/view?usp=sharing A列に10進数で数を入れて、「計算」ボタンを押すと、 B列にライトエッジパターンが、 C列からにコラッツパターンが表示されます。 ideoneはよく分かりませんでした。 エクセルマクロはうごきました。 サンクス。 左端がどう決まってるのかいまいち分かってないんだけど 2で割れた回数とかだよね? >>439 のは英語だったからいまいち自信がもてない。 コラッツパターンの左側は、 コラッツ操作で<2で割った回数-1>を蓄積しているものです。 >>173 にもあります。 (マクロやpdfでは0を書いてないけど) 左端を伸ばすパターンの説明で 3. Becomes the next x from the left end of the 1 to 1 on the right. てのがあるんだけど、どう訳せばいいのかよくわからんw 教えて〜 「次のxとして、左端の1から右端の1までを取る」という意味です。 _111111001 =x0が 1011110111 =x1になった時、 x1は左端の1から右端の1までを取るね、という事です。 実は英語は苦手で、いつも赤点でしたwww まだ理解できてないが左端を伸ばすパターンもエクセルマクロあるの? あるならオクレ。 左端を伸ばすパターンは数が左に伸びるのと、 ステップが無限に続くので、作れてないです。すみません。 んー左に伸ばすパターンって出力のサイズを制限したらプログラム書ける? 制限しても難しい? https://drive.google.com/file/d/0B_FTpAj7C52FVHlFNWt4UU1Vb3M/view?usp=sharing A列に10進数で数を入れて、「計算」ボタンを押すと、 B列にコラッツパターンのライトエッジパターンが、 C列に左端を伸ばすパターンのライトエッジパターンが、 D列からにコラッツパターンと左端を伸ばすパターンが表示されます。 B,C列で色が変わっている所は、コラッツパターンと左端を伸ばすパターンの右端がずれている所です。 大きい数を入れると「列が足りない」エラーが出るかもしれませんが、 Excel2007以降を使っているならば、Officeボタンから「変換」を選んで開きなおすと、 最大列が256列から16384列になります。 以前より進化しました。 諸兄におかれましては何卒よろしくご査収の上ご批評賜りたくよろしくお願い申し上げます。 http://koubeichizoku.ix-web.tk/collatz/ >>455 おおう、乙カレ。やるね。 左端を伸ばすパターンの正体がいまいちわかってないんだけどどういう思想で出来たものなの? 説明できるなら説明クレクレ。 333入れたら結果が出てこなかったんだが? なんか制限とかあるんだっけ? よくわかってなくてスマン。 コラッツ予想を2進数で考える、というのは前々からあって、 コラッツパターンを見出した時に、最後のルール 「最後に、左端に+1する」 を外したら面白いんじゃね、と思って左端を伸ばすパターンが出来ました。 まあ、偶然の産物ですね。 >>458 自分の環境では出てきます。 ・マクロを有効にする ・数字を入れた後一回Enterを押して、カーソルを合わせ直して実行する あたりを試してみてください。 >>460 でました。 カーソル合わせてなかったのかな?多分。 ライトエッジを12個づつに区切ったとき8個以上1が入らないことが言えると なぜコラッツ予想が証明されたことになるの? 今はそこで悩んでる。 左端パターンとコラッツパターンのずれが有限だとコラッツの予想が証明されたことになるの? やっぱまだよくわからん。 >>463 X0とy0B*2^(py0+1)は右端が1ずれた(y0Bが大きい)状態からスタートします。 y0Bの12区切りのライトエッジパターンは1が7個はいっていて、 もしX0の12区切りのライトエッジパターンに1が8個以上入らなければ、初期値の1ずれがずっと維持されるので、 X0 < y0B*2^(py0+1)が言えるわけです。 これ自体でコラッツ予想は証明されないです。 >>464 >左端パターンとコラッツパターンのずれが有限だとコラッツの予想が証明されたことになるの? 次のセクションで、ずれが有限であることを利用して、 「5 there is no loop other than 4-2-1 in Collatz conjecture」 「6 Collatz conjecture is not the number that diverges to infinity」 で、「コラッツ予想に4-2-1以外のLoopがない」「コラッツ予想で無限大に発散する数はない」 事を個別に証明しています。 >>465 2個目のX0 < y0B*2^(py0+1)は間違いで Xs < ysB*2^(pys+1) です。 >>1 頑張ってもらってるのにスマンが俺の頭じゃいまいち理解が追いつかない。 面白そうではあるんだけど。 まあ、ボチボチ読んでみます。 5章の(14)(15)の式なんだけど By the product of the loop 1 cycle X X x X x X ... It will be but , X > 1 so, either X x X x X x ... > 2 ^ 3 てのがよくわからないんだけど、つまりXって何なの? スレでは>>92 ですが、 実際は違いますが、9→7→11→17→9とループしたとすると、 X=(1+1/(3*9))*(1+1/(3*7))*(1+1/(3*11))*(1+1/(3*17))となります。 これは明らかに1より大きいので、 X*X*X*... > 2^3となって、 (1+1/(3*x0))...(1+1/(3*x_s-1)) < 2^3と矛盾します。 よくわからん。 1→1のループは X=(1+1/(3*1))=4/3>1 となって X * X * X * >2^3となって (1+1/(3*x0))...(1+1/(3*x_s-1)) < 2^3と矛盾しないの? 1→1のループは除外します。 全体的にこの論文は、コラッツ操作で1にたどり着く直前までを考えます。 1になった後のコラッツパターンを考えると、左端を伸ばすパターンとのずれは際限なく大きくなりますから。 http://cdn-ak.f.st-hatena.com/images/fotolife/r/righ1113/20160624/20160624002528.jpg つまり、コラッツ操作で1にたどり着いた後は、 (1+1/(3*x0))...(1+1/(3*x_s-1)) < 2^3 が成り立たなくなります。 とりあえず、色々コンピュータで検証してます。 4.1 Xsを12ステップで区切ったときライトエッジパターンに8個以上1が入ることはない、についてだけど 2連続の0はない 3連続の1はない 11011のパターンはない で計算したところ以下のパターンが出てきたんだが。 110101101011 これは問題になる? 110101101011は、二回繰り返すと 110101101011110101101011となって、 3連続の1が出てくるので、除外されます。 Coqでは、>>468 のpdfで、25ページの下の方の (filter remove_1_1_1 (map (cycle 2 nil) remove_8_12’)で、 cycle 2でパターンを二回繰り返して、filter remove_1_1_1で3連続の1を除外しています。 どゆこと? ライトエッジパターンは必ず周期12のループになるの? そっかー、ならないですね。 二周期目を調べる時は、 12ステップで除外しきれなかったパターンの直積を取って、filterをかけないとダメですね。 ……と思ったら「12ステップで除外しきれなかったパターン」って上の110101101011しかないんですね。 だったらcycle 2も直積も同じことで、110101101011110101101011となって、やはり除外されます。 これでどうでしょうか? いや、なんか怪しいです。 もうちょっと考え直してみます。 他スレのご指摘により数式だけでなく日本語の説明を加えました。 諸兄におかれましては何卒よろしくご査収の上ご批評賜りたくよろしくお願い申し上げます。 http://koubeichizoku.ix-web.tk/collatz/ ここで論じられているビットパターンは拙論では 2^p×3^m×g±1 (gは 6a±1) として捉えており、これらは素因数分解の一意性 からユニークな数であることに着目しています。 コラッツ予想の題意に従った奇数から奇数への変化のうち奇数間で増大するものを ≫+で表せば 2・2^p・g−1 ≫+ 2・2^(p-1)・3^1・g−1≫+ 2・2^(p-2)・3^2・g−1 ... ≫+ 2・2^1・3^(p-1)・g−1 ≫+ 2・3^p・g−1 となって L(p,g):={2・2^p・g−1,2・2^(p-1)・3^1・g−1, 2・2^(p-2)・3^2・g−1 ... ,+ 2・2^1・3^(p-1)・g−1 ,2・3^p・g−1} となって 相異なる(p,g)のL集合同士は互いに素 また同じく相異なるLの和集合同士も互いに素となります。(L(p,g)∪ L(p',g')=φ)(p≠p’)∨(g≠g’) ここで論じられているビットパターンは拙論では 2^p×3^m×g±1 (gは 6a±1) として捉えており、これらは素因数分解の一意性 からユニークな数であることに着目しています。 コラッツ予想の題意に従った奇数から奇数への変化のうち奇数間で増大するものを ≫+で表せば 2・2^p・g−1 ≫+ 2・2^(p-1)・3^1・g−1≫+ 2・2^(p-2)・3^2・g−1 ... ≫+ 2・2^1・3^(p-1)・g−1 ≫+ 2・3^p・g−1 となって L(p,g):={2・2^p・g−1,2・2^(p-1)・3^1・g−1, 2・2^(p-2)・3^2・g−1 ... ,+ 2・2^1・3^(p-1)・g−1 ,2・3^p・g−1} とすれば、 相異なる(p,g)のL集合同士は互いに素 また同じく相異なるLの和集合同士も互いに素となります。(L(p,g)∪ L(p',g')=φ)(p≠p’)∨(g≠g’) >>479 coqが通ったのに何が怪しいの? なんのためのcoqなの? coqは通ったけど、通った命題そのものがトンチンカンな主張だったってこと? >coqは通ったけど、通った命題そのものがトンチンカンな主張だったってこと? まあ、そういう事です。 Coqに通すまでの論証に穴があったという事です。 そうならないように始めの命題からCoqで一気通貫で証明を通すことが望ましいね。 実際には難しいだろうけど。 110101101011は除外出来ない事が分かりました。 そこで証明を次のように修正します。 12区切りのライトエッジパターンに110101101011が現れたとする。 末尾は1なので、次の12区切りは先頭が0である。 「先頭が1」「2連続の0」「3連続の1」「1,1,0,1,1」を除外した、12区切りで1が7個入るパターンは、 次の6つしかない。(Haskellで確認済み) [0,1,0,1,0,1,1,0,1,0,1,1] [0,1,0,1,1,0,1,0,1,0,1,1] [0,1,1,0,1,0,1,0,1,0,1,1] [0,1,1,0,1,0,1,1,0,1,0,1] [0,1,1,0,1,0,1,0,1,1,0,1] [0,1,0,1,1,0,1,0,1,1,0,1] 1~3個目は11で終わっているため、次の12区切りも0始まりとなってループする。 再び110101101011が来る余地は無い。 4~6個目は、次の12区切りで1始まりが可能なので、さらに調べる。 「先頭が10」で、「2連続の0」「3連続の1」「1,1,0,1,1」を除外した、12区切りで1が7個入るパターンは、 次の8つしかない。(Haskellで確認済み) [1,0,1,0,1,0,1,0,1,0,1,1] [1,0,1,0,1,0,1,1,0,1,0,1] [1,0,1,0,1,1,0,1,0,1,0,1] [1,0,1,1,0,1,0,1,0,1,0,1] [1,0,1,0,1,0,1,0,1,1,0,1] [1,0,1,1,0,1,0,1,1,0,1,0] [1,0,1,1,0,1,0,1,0,1,1,0] [1,0,1,0,1,1,0,1,0,1,1,0] 1個目は11で終わっているため、次の12区切りも0始まりとなってループする。 2~5個目は1で終わっているため、次の12区切りも1or0始まりとなってループする。 6,7個目は、連続して並べると、 110101101011 [0,1,*,*,*,*,*,*,*,1,0,1] [1,0,1,1,0,1,0,1,1,0,1,0] 110101101011 [0,1,*,*,*,*,*,*,*,1,0,1] [1,0,1,1,0,1,0,1,0,1,1,0] となって「1,1,0,1,1」が現れるので除外される。 8個目は、連続して並べると、 110101101011 [0,1,*,*,*,*,*,*,*,1,0,1] [1,0,1,0,1,1,0,1,0,1,1,0] 110101101011 となって「1,1,0,1,1」が現れるので110101101011にはならない。 よって、二回以上110101101011が現れることはない。 初期値をX0 とy0B * 2^(py0+2)(1ずらし→2ずらし)から始めれば、 Xs はysB * 2^(pys+2) を超えないので、Xs < ysB * 2^(pys+2) である。 さて、これをCoqでどうやってやろう…… どうせその論証にも穴がある。 都合の悪い並びはいつまで経ってもなくならない。 穴を埋めようとすると >「先頭が10」で、「2連続の0」「3連続の1」「1,1,0,1,1」を除外した こんな感じの細かい条件がさらに追加される。 それでもなお、都合の悪い並びはなくならない。 キリがないどころか、そもそもこのやり方では本質的に不可能。 0と1の並び方の規則を探求すること自体が全くの無駄。 こいつらは基本的にランダム列に近づきたがっている。 途中で不完全燃焼を起こしてループに陥るだけで、 それまでの間はランダム列に近づきたがっている。 そうやって規則がない方向に行こうとしている対象について 規則を探求しても、うまく行くわけないだろ。 それよりも、「ランダム列に近づきたがってる」ことを 実際に証明した方が早い(もちろん現状では未解決)。 >>489 これ検証すんの結構つらいわw Coqでなんとかならんか? 1が7個のパターンだけ考えてるみたいだけど 1が6個以下のパターンを除外していい理由がよくわからん。 Coqは考え中です。 (ちゃんとやってないですけど) 1が6個のパターンは、0,0が除外されるので [0,1,0,1,0,1,0,1,0,1,0,1] [1,0,1,0,1,0,1,0,1,0,1,0] しかないんんですけど、こんなパターンは無いかなあと。 (どこかで1,1,が現れるはず) 1が5個以下のパターンは、必ず0,0が含まれるので、 全て除外されます。 >>こんなパターンは無いかなあと。 数学の証明しようってのにずいぶんずぼらだなw まあ気持ちはわかるが。 ポエムのうちは読む気はないけど証明されたら眺めてみようかくらいに思ってる人はそれなりにいると思うからがんばってね。 12区切りで1が6個入るパターンは除外される証明ができました。 >>468 の7ページを見ながらご覧下さい。 http://cdn-ak.f.st-hatena.com/images/fotolife/r/righ1113/20160628/20160628023431.jpg ライトエッジパターンでは「2連続の0」「3連続の1」「1,1,0,1,1」に加えて「0,1,0,1,0,1,0」 も除外されるという事です。 >>468 発散する初期値がないことの証明も間違ってるように見える。 実際に (log_2 x_s)/s の挙動を計算してみると、 発散する初期値があろうがなかろうが、無条件で有界であることが分かる。 まず、9ページ目の(3)式はコラッツの軌道のsステップ目を表現しただけだから、 何の条件もなしに成り立っている。以下、(3)式から出発して x_s = x_0(3^s/2^t)(1+1/(3x_0))・・・(1+1/(3x_{s−1})) ≦ x_0(3^s/2^t)(1+1/3)・・・(1+1/3) = x_0(3^s/2^t)(1+1/3)^s = x_0(3^s/2^t)(4/3)^s ≦ x_0(3^s)(4/3)^s = x_0 4^s となるので、log_2 x_s ≦ log_2 x_0+slog_2 4 となって、 (log_2 x_s)/s ≦(log_2 x0)/s + 2 となる。よって、 発散する初期値があろうがなかろうが、無条件で有界になっている。 このことから、pdfの10ページ目にある 「 Here, from Fig.3 (傾きが垂直に近づくので) 」 のところは自動的に間違いとなる。 こういうのはどうでしょうか。 xは発散するとする。 (1+1/3x_0)…(1+1/3x_{s-1}) < 2^4 だから (1+1/3x_1)…(1+1/3x_s) < 2^4 も成り立つ。 t=saと置き、(1+3/t)^t < (1+1/3x_1)…(1+1/3x_s)が成り立つようにaを定める。 s→∞でt→∞だから、 lim[t→∞](1+3/t)^t = e^3 ≒ 20 > 16 だから、 無限大に辿り着く前に16を超える。越えた所をs'と置くと、 (1+1/3x_1)…(1+1/3x_s') > 16 となって、(1+1/3x_1)…(1+1/3x_s') < 2^4 と矛盾する。 >>499 >t=saと置き、(1+3/t)^t < (1+1/3x_1)…(1+1/3x_s)が成り立つようにaを定める。 問題外。x_sの発散スピードが大きいとき、そのようなaは取れない。 コラッツの問題を舐めるな。 t=e^sとか、t=s!とかにしてもダメなんでしょうか? >>501 どうも君は不等式に対する感覚がイカれてるね。 パッと見てすぐに分かる間違いに全く気づいてない。 tが大きければ大きいほど、(1+3/t)^t は e^3 に近づくのだから、余計に (1+3/t)^t < (1+1/3x_1)…(1+1/3x_s) が成り立ちにくくなるだけだろ。 ていうか、x_1からx_sまでが物凄い勢いで大きければ、 (1+1/3x_1)…(1+1/3x_s) はほとんど 1 に等しいのだから、もはや (1+3/t)^t < (1+1/3x_1)…(1+1/3x_s) なんて成り立たないでしょ。 >>503 より詳しく説明しよう。 もし発散する初期値が存在するならば、次が成り立つことが証明できる。 ∀ε>0, ∃x_0 s.t. x_0は発散する初期値であり、かつ (1+1/3x_1)…(1+1/3x_s) < 1+ε (s∈N). このことから、(1+1/3x_1)…(1+1/3x_s) を統一的に下から押さえることができる定数は 「 1 」しかないことが分かる。つまり、x_0が発散する初期値ならば、 1 < (1+1/3x_1)…(1+1/3x_s) (s∈N) が成り立つということ。しかし、この不等式は自明なので、何の役にも立たない。 結局、この方針では原理的に不可能。 ん〜識者乱入か? 俺じゃよくわからんし勘違いを防ぐためにも なるべくCoqで証明を通してほしいよね。 もしちゃんとZs < Ys <= Xs < ysB * 2^(pys+2) < 8Zs が言えたら、 Zsと8Zsのずれは3で、これがずっと変わらない って無限大までいっても変わらないって事だから xsが発散してもずれは3以下なんだと、今気づかせてもらった。 という訳で、無限大に発散する方はあきらめます。 4-2-1以外のLoopがない方に注力します。 >>1 はいまどうしてるの? まだ頑張ってんの? それとも休憩中? >>489 の状態遷移図の穴が埋められないんです。 ちょっと休憩中です。 >>>489 の状態遷移図の穴が埋められないんです。 穴は埋まらないよ。この方針じゃ原理的に不可能。 なんで分からないのかなあ。>>506 のときみたいに 「これじゃ本質的にダメなんだ」って心の底から悟れよ。 ダメなんだよこれじゃ。ダメなの。このやり方じゃ解けないの。 本質的に解けないことちゃんと数学的に証明をしてあげないと。 頭ごなしに否定するだけじゃ納得するはずないでしょ。 >>511 数学的に証明するのはムリ。 しかし、ほぼ確実な状況証拠はある。 3n+1版ではなく、an+1版のコラッツ予想を考える(ただしaは7以上の奇数)。 この場合、ほとんどの初期値でコラッツの軌道が発散することが予想されている。 軌道上に出現する各々の値の偶奇を0,1で横一列に並べると、 どうもその列は、ほとんどの初期値で2進正規になっているように見える。 もし2進正規になってることが証明できたならば、コラッツ予想でおなじみの 「軌道上では偶数と奇数が1/2ずつの確率で出現しそう」というヒューリティクスが 実際に正しいことが分かり、「ほとんどの初期値で発散する」という予想も正しいことが確定する。 おそらく、コラッツの軌道は本質的にランダムになりたがってる。 もともとの3n+1版でも同じことで、やはりランダムになりたがってる。 しかし、こちらの場合は掛ける数が「3」であるがゆえに、十分大きな数になれず、 それゆえに自由度が低下し、途中で不完全燃焼を起こしてループに陥る。 が、それまでの間はランダム列に近づきたがっている。初期値を大きく取れば取るほど、 ランダム列に近づきたがる期間も長くなるので、その間で幾らでも抜け穴となるパターンが生じうる。 だから本質的にムリなのだ。(続く) (続き) ライトエッジの「抜け穴」と似たような現象は、以下の箇所にも見られる。 英語版のコラッツ予想の記事を見ると、 >In particular, Krasikov and Lagarias showed that the number of integers in the interval [1,x] >that eventually reach one is at least proportional to x^0.84.[19] という記述がある。区間[1,x]に属する自然数のうち、コラッツの変換によって1になる数の比率は、 少なくとも x^{0.84} はある、という驚くべき文章である。 文献[19]をかいつまんで説明すると、「コラッツの変換によって1になる自然数の集合」を、 ある種のパラメータで分割して、いくつかの集合に分けるところから始まる。 それらの集合の間に定まる漸化式を使って、x^{0.84}という評価を得ている。 この漸化式が完全に制御できれば、もっといい結果が出るわけだが、 漸化式がイジワルな形をしており、漸化式を展開するたびにランダム性が増してしまって制御できなくなる。 そこで、途中で評価を落として不等式の形にすることで、不等式の左辺と右辺に何とかパターン性を 出現させ、それによって問題を対処する。その結果、x^{0.84} という中途半端な数字になってしまう。 ライトエッジの抜け穴は、この「評価を落としてパターン性を出現させる」ところに どことなく対応しているように見える。ライトエッジを完全に解析すると、まず間違いなく、 そのパターンは有限通りには収まらず、複雑な形の漸化式で記述されることになる。 その漸化式を展開するたびにランダム性が増してしまい、結局は制御できなくなる。 逆に、もしライトエッジが有限通りに収まったら、文献[19]の漸化式も実際には 上手くパターンに落とし込めることになると予想される。が、今のところそういう話は見てないし、 [19]を読んで漸化式を触ってみても、もう本能的に「こりゃムリだわ」っていう感想しか出てこない。 そんなわけで、ライトエッジの方針もムリに決まってるのだ。 (補足) 結局、>>512 の話でも、>>513 の話でも、 コラッツの変換を深く深く弄れば弄るほど、 ランダム性が増していく感触が確かな手ごたえとして観測される。 どこまでいっても、パターンに収まってくれる気配が全く出てこない。 「本質的にランダムになりたがっている」としか思えないのだ。 また、コラッツ予想の難しさはまさにこの部分にあるはずだ。 >>488 にも書いたが、コラッツ予想に取り組むなら、 「ランダムになりたがってる」という感触を どうやって解析したらいいかを真正面から考えるしかないだろう。 そして、そのこと自体が既に難しく、だからこその未解決問題なのだろう。 コラッツ予想で毎回思うんだけど プログラムでいうif文を扱える数学って存在すんのかなあ ifを扱える数学というか、プログラムの停止問題は解けないでそ。 Coqでコラッツの予想を厳密に定義するとどんな感じになるの? 有限回繰り返したときってCoqでどうやって表現すりゃいいんだ? >>518-519 Coqでは止まらない再帰関数は書けないので、 >>373 では、再帰を有限回で0終了させる引数yを入れてあります。 で、どんなxに対してもlast collatz03が0にならないyが存在する、という事で、 Require Import List.して Theorem collatz_is_true: forall (x:nat), x<>0 -> (exists y:nat, 1=(last (collatz03 x y) 0)). ってとこじゃないでしょうか。 うーんyで適用回数制限してんの? 止まらない再帰かけないってのも不便だな。 本質的には問題に成らんのかな Coqの仕様なんでなんとも…… >>520 でコラッツの定義としては問題ないと思います。 http://koubeichizoku.ix-web.tk/collatz/ 修正いたしました。当板の諸兄におかれましては何卒よろしくご査収の上 ご批評賜りたく、よろしくお願い申し上げます。 まず、x0の範囲を8bit以上から15bit以上に変更します。 これで、Xsが1ステップ進むごとに約0.585プラスされます。 禁止パターンは以下です。 ・00 ・111 ・11011 ・0101010 ・11 01011 01011 01011 以下のシミュレーションをおこないます。 【シミュレーションA】 1.7ビットの初期値x0A=1111111を用意する。 2.x0Aを下位へ1ビットシフトして(末尾は捨てる)、x0Aに加える。 3.最下位ビットに1加える。(下位からの繰り上がりが常に有る事を想定) 4.n+1ビットになっていたら、最下位ビットを捨ててnビットにする。 5.2~4を繰り返す。 得られる値をxsAとする。 xsAのライトエッジパターンは17区切りで以下になりますが、 [0,#1,1,0,1,0,1,1,0,1,0,1,1,0,1,0,1,0] 1個左にずらして01101011010110101の繰り返しとします。 それに合わせて、X0のライトエッジパターンも0と定義して、0ステップ目から17区切りにします。 (もしX1が0なら従来通り1ステップ目から始めます。) https://drive.google.com/file/d/0B_FTpAj7C52FLWI5TWMtMi1tVms/view?usp=sharing xsAは17区切りで1が10個入ります。 17区切りで1が11個入るパターンは禁止パターンなので除外します。 17区切りで1が10個入るパターンは、全部で21個あるのですが、先のライトエッジパターンの操作により、 0始まりのもの8個だけを考えれば良いです。 A1からA8の状態遷移を考えます。どれも0につながるので、この8個で閉じています。 薄い灰色は禁止パターンになるので、遷移できない箇所です。 濃い灰色はXsに0.585を足していって脱落した所です。 これを元に樹形図を描くと、最長が A4-A2-A2-A3-A3-A1-A8-A8-A7-A7-A6-脱落 の17*12ステップですが、 A2-A2-A3-A3 と A8-A8-A7-A7は脱落するので、 A4-A2-A2-A3-A1-A8-A8-A7-A6-脱落 の17*10ステップが最長となります。 これは、170ステップ以内で、17区切りで1が9個入るパターンが現れる事を意味しています。 xsAのライトエッジパターンに手を加えます。 170ステップごとに0を挿入します。 これをおこなっても先の議論より、 Xs < xsA*2^pxs (2^pxsはXsより十分右へ離す定数)が言えます。 170ステップごとに0を挿入した事により、xsAの傾きが変わります。 挿入する前は10/17=0.58823… > log(3/2)ですが、 挿入後は100/171=0.58479… < log(3/2)です。 グラフでは、「左端を伸ばすパターン」<「コラッツパターン」<「xsA」と並んでいますが、 xsAの傾きがlog(3/2)より小さい為、順序が逆転し、矛盾します。 この矛盾を回避するには、順序が逆転する前に、コラッツ値が1になるしかありません。 書いてみて分かったんですが ちょっとダメみたいです。お騒がせしました。 状態遷移図を修正しました。 before:A1\after:A1で結果がA8になっているのは、 A1からA1に遷移させるつもりだったけど、実際に計算してみるとA8に遷移してた、ということです。 あと、A4-A2-A2の遷移はA4-A2-A3になってしまうので、 A4-A2-A3-A1-A8-A8-A7-A6-D1 の17*9ステップが最長となります。 実はもう一つ問題があるのですが、それは後で書きます。 A6-D1-A1-A8と遷移したとします。 D1の末尾は0なので、A1〜A8に繋げる事ができません。 そこで11を挿入します。(1じゃないのは0101010回避のため) 次にA1を普通にやって、A8の先頭で、コラッツパターンの右端を2つ左にずらします。 これで11と相殺されます。 このときのA8のライトエッジパターンは[-2,1,0,1,1,0,1,0,1,1,0,1,0,1,0,1,1] と書いても良いかもしれません。 これで「左端を伸ばすパターン」<「コラッツパターン」<「xsA」の関係も維持されます。 ■ このスレッドは過去ログ倉庫に格納されています
read.cgi ver 07.5.5 2024/06/08 Walang Kapalit ★ | Donguri System Team 5ちゃんねる