コラッツ予想がとけたらいいな　その2

コラッツ予想がとけた ..

232:１３２人目の素数さん
18/06/10 09:11:07.49 gH+TEyZw.net
>>204
> 「それぞれの項目が重なり合わないように敷き詰められている」ように思えてなりません。
コラッツ予想は、言い方を変えると「４で割って３余るすべての奇数は、
『３倍して１を足す』『２で割る』という二つの操作によって、
１を根とした二分木上に一意に配置される」ということだから、
その認識は正しいと思います。
> 素人なんではっきり証明できる力はないのですがorz
まぁまぁ、そうおっしゃらずに。数学者は数学的な道具の取り扱いに長けているので、
つい自分の使い慣れた道具で扱おうとして、結果的に灯下探索症候群に
陥ることもあるようですから、素人目線も重要ですよ。
行列を使って永らく未解決だった問題が、連分数や図的解法（古代メソポタミアでは
普通に使われていましたが、二十一世紀に再評価されるまで、ほとんど博物館の
展示物扱いでした）であっさり解けちゃった例もありますし。
ヘヴィサイドの演算子法みたいに、「とにかく解けるんだからいいじゃないか」と
いうのに後から数学的なリクツがついてきた、という例もあるので。

233:１３２人目の素数さん
18/06/10 09:27:08.31 gH+TEyZw.net
>>220 の指摘は、「二分木上に一意に配置される」という観点からいうと、
ある「４で割って1 余る奇数」を d （odd の d です。o だとゼロと紛らわしい
ので）としたとき、「d が d≡0(mod 3)のときには、そこより先に（次の数 d' が
出てくるような）枝はない」「d が d≡1(mod 3)のときには、奇数枝が出ないので、
あるとすれば偶数枝の先に d' がある」「d が d≡2(mod 3)のときには奇数枝も
出るので、奇数枝と偶数枝の両方の先に d' （とか d'' とか）がある可能性がある」という
話になるんじゃないか、と思います。ですから、非常に納得のゆく視点です。
等差級数うんぬんの話というのは、そこから自然に導かれる帰結なのでは
ないでしょうか。

234:１３２人目の素数さん
18/06/10 09:38:45.60 gH+TEyZw.net
>>226
ごめんなさい。「奇数枝」というのは、「(3n + 1) / 2 操作によって
奇数に至るルート」なので、途中で偶数を経由しています。したがって、
「3n + 1 操作」ベースで考えると、「それは偶数枝として一般的に
扱ったほうが適切なんじゃねぇんの？」という批判は（たぶん）
あるかと思います。

235:１３２人目の素数さん
18/06/10 11:33:20.33 GkYmcQpB.net
1
2
4←1
8
16←5
32
64←21
128
256←85
512
…
5
10←3
20
40←13
80
160←53
320
640←213
1280
…

236:１３２人目の素数さん
18/06/10 11:48:45.88 GkYmcQpB.net
一般化するとこんな感じで枝分かれを繰り返してくわけだが
6n+1
12n+2
24n+4←8n+1
48n+8
96n+16←16n+5
192n+32
384n+64←128n+13
…
6n+5
12n+10←4n+3 「奇数枝」はここかな？
24n+20
48n+40←16n+13
96n+80
192n+160←64n+53
…

237:１３２人目の素数さん
18/06/10 13:29:24.03 gH+TEyZw.net
>>229
> 12n+10←4n+3 「奇数枝」はここかな？
よく分からんが、たぶんそうだと思う。
>>116 の再録になるが、
> 242:242 -> 161 -> 107 -> 71 -> 47 -> 31
> 728:728 -> 485 -> 323 -> 215 -> 143 -> 95 -> ☆63
> 1214:1214 -> 809 -> 539 -> 359 -> 239 -> ☆159
> 1700:1700 -> 1133 -> 755 -> 503 -> 335 -> 223
> 2186:2186 -> 1457 -> 971 -> 647 -> 431 -> 287 -> 191 -> 127
> 2672:2672 -> 1781 -> 1187 -> 791 -> 527 -> ☆351
> 3158:3158 -> 2105 -> 1403 -> 935 -> 623 -> 415
> 3644:3644 -> 2429 -> 1619 -> 1079 -> 719 -> 479 -> 319
> 4130:4130 -> 2753 -> 1835 -> 1223 -> 815 -> ☆543
> 4616:4616 -> 3077 -> 2051 -> 1367 -> 911 -> 607
> 5102:5102 -> 3401 -> 2267 -> 1511 -> 1007 -> 671 -> ☆447
> 5588:5588 -> 3725 -> 2483 -> 1655 -> 1103 -> ☆735
> 6074:6074 -> 4049 -> 2699 -> 1799 -> 1199 -> 799
> 6560:6560 -> 4373 -> 2915 -> 1943 -> 1295 -> 863 -> 575 -> 383 -> ☆255
> 7046:7046 -> 4697 -> 3131 -> 2087 -> 1391 -> ☆927
> 7532:7532 -> 5021 -> 3347 -> 2231 -> 1487 -> 991
> 8018:8018 -> 5345 -> 3563 -> 2375 -> 1583 -> 1055 -> 703
> 8504:8504 -> 5669 -> 3779 -> 2519 -> 1679 -> ☆1119
> 8990:8990 -> 5993 -> 3995 -> 2663 -> 1775 -> 1183
> 9476:9476 -> 6317 -> 4211 -> 2807 -> 1871 -> 1247 -> ☆831
> 9962:9962 -> 6641 -> 4427 -> 2951 -> 1967 -> ☆1311
みたいな系列だ。

238:１３２人目の素数さん
18/06/10 13:37:00.64 gH+TEyZw.net
あ、念のため。
このスレに集っている方々にとっては常識だろうけれど、
‘☆’

239:がついてるのは、三の倍数（n ≡ 0 (mod 3)）の場合な？「偉そうに」とか「上から目線」とか、そう思われるのは不本意なので。

240:righ1113
18/06/10 15:13:02.69 FdIQbMom.net
>>220
自分も昔似たような事を考えていました。
URLﾘﾝｸ(d.hatena.ne.jp)
でも後が続かないのですよね……
同じ事を考えた方がいたのは嬉しいです。

241:１３２人目の素数さん
18/06/10 16:52:17.37 gH+TEyZw.net
>>232
> 同じ事を考えた方がいたのは嬉しいです。
つーか、似たようなことを考えてる輩（やから）が
このスレに集まってるんだろうがよ（笑）。

242:218
18/06/11 07:22:40.87 l+PAssIA.net
>224
>222を初項の小さい順に並べ直してみると、
1.9.17.25.33.41…a
3.7.11.15.19.23…b
5.37.69.101.133.165…c
13.29.45.61.77.93…d
21.149.277.405.533.661…e
53.117.181.245.309.373…f
a___a___a___a___a___a___a___a___a
_b_b_b_b_b_b_b_b_b_b_b_b_b_b_b_b_
__c_______________c______________
______d_______d_______d_______d__
__________e______________________
__________________________f______
と、フラクタル的な配置が出現しているように思います。
言い換えれば、全ての奇数がこの配置のどこかに格納される事が証明できれば、「とんでもなく大きな数で例外が現れる」可能性を除去できるのではないかと考えたんですが、いかがでしょうか？
あとは、この数列が例外なくコラッツ操作後1に繋がる(1.5.21.85.341.1365…)の数列に帰結する事が証明できれば、コラッツ予想を証明したと言えるのではないかと。
(「そんなんできねーよw」と自分では思ってたんですが、>223が糸口になりそう？)
頓珍漢な事を言ってたら申し訳ないです。

243:１３２人目の素数さん
18/06/11 08:14:51.55 CCISXKIi.net
>>234
いや、発想としては順当だろうと思う。>>207 も発想としては同じだろう。
下向きの三角形というのは、一次元セルオートマトンではしょっちゅう
出てくるパターンだし、タガヤサンミナシ（イモガイの一種）の模様にも
あるような普遍的なパターンなので、シェルピンスキーの三角形みたいに
大きな三角形が「ずどん」と出るケースをうまく避けられれば
証明に結びつくと思う。
…… つーか、そのネタはウラムも思いついていて、ノイマンあたりと一緒に
追いかけてたかもしれない。それでコラッツ→ウラム→ノイマン→角谷と
伝わって、ここでこうして議論されているという話はありうる。

244:１３２人目の素数さん
18/06/11 08:16:22.58 CCISXKIi.net
×シェルピンスキーの三角形
〇シェルピンスキーのギャスケット

245:１３２人目の素数さん
18/06/11 08:42:28.48 CCISXKIi.net
あと、厳密な（解析的な）解決には結びつきそうもないが、
セルオートマトン → チューリング → 二重勾配 → 形態形成
→ フィボナッチ螺旋 → 互除法 → 連分数みたいなルートは
なんとなく臭い、と思う。「二重勾配」あたりに位置するのが、
「ビットシフト」と「算術演算」（2n + n + 1 ＝ 3n + 1）
であり（こっちが速い過程）、結果的に起きるキャリー（繰上り）の
連鎖とビットパターンの分布の相互作用（こっちが遅い過程）
ではないかと。そのあたりが話をややこしくしているように思う。

246:１３２人目の素数さん
18/06/12 07:21:50.27 /TgiGIzK.net
オートマトンといえば昔考えた、
×3+1を計算する有限オートマトン
文字: 0,1,空白
先頭が下位の2進数、後は空白のテープを考える
状態: 0(×3+0), 1(×3+1, 初期状態), 2(×3+2), 3(停止).
遷移表:(移動は常に右)
遷移|0　|1　|空
s0|0/s0|1/s1|空/s3|
s1|1/s0|0/s2|1/s3|
s2|0/s1|1/s2|0/s1|

247: 例:7×3+1=22 s1: [1]11空空空 s2: 0[1]1空空空 s2: 01[1]空空空 s2: 011[空]空空 s1: 0110[空]空 s3: 01101[空] 停止せずに折り返して先頭の0を空白に置き換えるように改造すればコラッツ問題を再現するけど、停止しなくなる 1…10と0…01が状態s1を保つので、これでうまく分類できないかなぁ、まで考えた

248:１３２人目の素数さん
18/06/12 13:08:59.15 B3CrVbdR.net
>>238
> まで考えた
Java の開発環境があるなら、前にも「それなりに頑張ってるんだけど」
的な話をしたので、 Java のソース貼るけど？
ただ、ム板（プログラム技術板）でも「ソース貼られると
読んでて邪魔だ」と言われて嫌われて、
「どっかいけ」みたいな感じで追い出されたのだが。
『★★ Java の宿題ここで答えます Part 74 ★★』とかに
“出題”してくれれば、名目が立つんだが。

249:１３２人目の素数さん
18/06/12 19:25:58.43 psqSBNTM.net
>>1みたいにgithub使えばよろし
まあ、無理にとは言わんが

250:１３２人目の素数さん
18/06/12 21:30:52.62 B3CrVbdR.net
>>240
> github使えばよろし
> まあ、無理にとは言わんが
WikiPedia によれば、GitHub は
> 2018年にマイクロソフトによる買収が発表されている
そうだ。
ゲイツが死んで三十年くらい経ったら考えてみてもいい。

251:１３２人目の素数さん
18/06/12 21:33:17.05 psqSBNTM.net
もしかして言語がJavaなのもアンチゲイツのせいなのか？ｗ

252:１３２人目の素数さん
18/06/13 09:31:54.51 86YPnV22.net
>>242
Eclipse を使ってるのもアンチゲイツのせいだw
Eclipse の原型は OS/2 で動いてた VisualAge C/C++ なんだぜ。

253:１３２人目の素数さん
18/06/13 19:07:29.31 86YPnV22.net
ところで、このスレはコンピュータ使いが多いと思うんだが、
・計算器で限界に挑戦するなら C 言語
・プログラマが本業だったら、仕事にも使える Java
・研究とかも含めて、ロジックとかそっちの方にも視野を
向けてるんだったら Lisp 系
・教育のほうに向いているんなら N-BASIC とか Mathematica とか
みたいな言語ごとの棲み分けみたいなのがありそうに思うんだが、
お前ら何（＝どんな言語）使ってる？

254:１３２人目の素数さん
18/06/13 20:27:07.06 9eZXXRM3.net
そういやコラッツてプッシュダウンオートマトンとかで実装できるの？

255:１３２人目の素数さん
18/06/13 21:21:20.83 86YPnV22.net
>>245
なんかしら Wolfram がチューリングマシンをどうこうして、
どっかの学生が証明したのなんだの、という話が
二三日前の新聞にあったような。
　　　　　　　　　　　　　　　　　　　ggrks 、とセルフつっこみ。

256:righ1113
18/06/13 21:27:55.75 RdFyYz3+.net
>>245
チューリングマシンなら、あるんだがなあ。
URLﾘﾝｸ(m.youtube.com)

257:１３２人目の素数さん
18/06/13 21:33:44.48 9eZXXRM3.net
そりゃチューリングマシンはあるだろうさ

258:１３２人目の素数さん
18/06/13 22:05:18.39 6aITicNF.net
JavaScript で実装してみた
たぶん新しめのブラウザでないと動かない
最上位の1は暗黙の存在とし、内部的には全部'_'になって止まる
第1引数は下位を先頭とする2進数の文字列
(※最上位の1は入力からは除外する)
第2引数は途中で止めたい時用に処理する最大桁数
出力は途中経過の配列(最上位の1は補完)
function collatz(a,m){
const STT=[
['___','___','___'], // 停止
['10L','11L','6_R'], // 最下位まで戻る
['___','___','10L'], // 繰り上がり処理
['30R','41R','11L'], // ×3+0
['31R','50R','20R'], // ×3+1
['40R','51R','21R'], // ×3+2
['6_R','5_R','0_R'], // 割る2
];
let s=6, i=0, r=[a+1];
a=[...a];
while(s>0&&i<m){
let c='01'[a[i]]||'2';
let n=STT[s][c];
s=n[0]; // 状態
a[i]=n[1]; // 文字
i+=(n[2]=='R')?1:-1; // 移動
if(s==6)r.push(a.join('')+1);
}
return r;
}

259:１３２人目の素数さん
18/06/13 22:08:23.72 xW9095UW.net
>>249
ん、これコラッツのプッシュダウンオートマトンなの？

260:１３２人目の素数さん
18/06/13 22:12:54.50 6aITicNF.net
なお出力の途中経過は×3+1,÷2のいずれかが完了したところだけ出してる

261:１３２人目の素数さん
18/06/13 22:13:28.53 6aITicNF.net
あ、プッシュダウンではないね
ただのオートマトン

262:１３２人目の素数さん
18/06/13 22:14:59.61 xW9095UW.net
有限オートマトンのこと？
コラッツってそんな弱いの？

263:１３２人目の素数さん
18/06/13 22:25:22.86 6aITicNF.net
弱い強いはよくわからんが
「ある整数からコラッツ問題の通りに計算を続けて1に到達する」と
「ある整数に対応する初期状態から開始すると止まる」が同値になるオートマトンは作れるかな？
というわけで作ってみたのだが

264:１３２人目の素数さん
18/06/13 23:07:39.84 xW9095UW.net
うーん、プログラムが正しくオートマトンの制限を守ってるかどうか判断できない orz
パッと見、チューリングマシンのようにも見える。LとかRとかあるし。

265:１３２人目の素数さん
18/06/13 23:23:40.12 6aITicNF.net
オートマトンは進む一方か……
チューリングマシンだったねこれ

266:１３２人目の素数さん
18/06/13 23:34:57.10 6aITicNF.net
とりあえずwikipediaで定義を見直してきましたが、チューリングマシンと呼ぶべきですね
チューリングマシンをオートマトンの一種とするならオートマトンといえなくもないかもですが……
有限オートマトンではありません
なんかごっちゃになってましたねー

267:１３２人目の素数さん
18/06/15 19:53:54.10 uqoBws9V.net
まあ、プッシュダウンオートマトンでコラッツを実装で来たらそれはそれで一定の成果なのかな？
コラッツ予想が真なら究極的には1状態有限オートマトンでもおｋなわけだから無い話ではないはず。

268:１３２人目の素数さん
18/06/15 21:09:22.84 uqoBws9V.net
プッシュダウンオートマトンで実装で来たら無限に発散しないことが言えてしまう？

269:１３２人目の素数さん
18/06/15 21:10:02.85 uqoBws9V.net
いや、そうともかぎらんか。スマソ

270:前786
18/06/18 00:49:33.21 R9ITlpR3.net
すっかり別の話が進んでいるようですし、
私の方はなかなか次の話ができる見込みがないので、
私から剰余コラッツ予想についての話題を出すのは一旦休みたいと思います。
ここまでお付き合い下さった皆様、ありがとうございました。

271:righ1113
18/06/18 03:15:08.94 WdqZRIIM.net
残念ですぅ

272:１３２人目の素数さん
18/06/18 08:13:14.97 M5JNYBjP.net
解決に結びつくような話ではないのでスレ違いなんだが、
アラン・チューリングがチューリング・マシンの論文を
発表したのが一九三六年で、ローター・コラッツが
コラッツ予想を提出したのが一九三七年だろ？
なんかしらの関係はあったんだろうかね？

273:１３２人目の素数さん
18/06/18 08:44:33.72 M5JNYBjP.net
やべぇ。コラッツ予想は連続体仮説や選択公理みたいに、
証明不能であるかもしれないという疑惑が出てきた。
>>246 >>247
で話題になってたのは Wolfram が提出した問題なんだが
コラッツ過程を実行するチューリングマシン
（テープ上に、1, 0, -（データなし）の三状態が記録できる。
で、二往復すると、コラッツ過程が１ステップ進む）が、
万能チューリングマシンであることが示されたらしい
（>>247 の動画は、その実行例のデモ）。
そうなると、コラッツ予想は万能チューリングマシンの
停止性問題に帰着しそうな気がする

274:んだが、どうだろう。それとも「遷移規則をうまく構成する」ことで万能チューリングマシンを実現することができるだけなので、「コラッツ予想を説くための具体的な遷移規則」を与えたときに停止性が謂えるかどうかは、まったくの別問題なのかな？

275:righ1113
18/06/18 10:36:46.36 qNaPdH2s.net
>>264
Wolframが提示して学生が解いたチューリングマシンは2状態3色で、8状態3色のコラッツとは別物ですね。
URLﾘﾝｸ(ja.osdn.net)
またおっしゃる通り、万能チューリングマシンに具体的な遷移規則を与えると、ある1つのチューリングマシンと等価になるので、万能性は消失すると思います。

276:１３２人目の素数さん
18/06/18 13:50:07.33 M5JNYBjP.net
>>265
ありがとう。安心した。

277:１３２人目の素数さん
18/06/18 21:39:43.70 mGDl57cN.net
コラッツ過程を実行するチューリングマシン
（テープ上に、1, 0, -（データなし）の三状態が記録できる。
で、二往復すると、コラッツ過程が１ステップ進む）が、
万能チューリングマシンであることが示されたらしい
これソースあるなら教えてくれる？
ひょっとしたら万能性が消失してないという話なのかもしれないので。
可能性は低いと思うけど。

278:１３２人目の素数さん
18/06/19 06:40:39.47 EReiwMfo.net
>>128
論文はこちら
URLﾘﾝｸ(www.wolframscience.com)
あとはこことか
URLﾘﾝｸ(reference.wolfram.com)
動画はガイシュツだけどこれ
URLﾘﾝｸ(m.youtube.com)

279:１３２人目の素数さん
18/06/19 06:46:57.18 EReiwMfo.net
あとはこれも
URLﾘﾝｸ(www.wolframscience.com)

280:１３２人目の素数さん
18/06/19 06:53:13.41 EReiwMfo.net
オートマトン関係ないけど、本筋的にはこんなのも
URLﾘﾝｸ(mathworld.wolfram.com)

281:１３２人目の素数さん
18/06/19 22:10:02.87 3mIZP/N3.net
>>268
コラッツがチューリング完全とは書いてないっぽい

282:１３２人目の素数さん
18/06/21 13:52:02.84 qX+RK+7d.net
「何か進展はあるか？」みたいな話だとスレが進まないだろうけど、
「こういうアプローチはどうだろう？」みたいな
雑談っぽい話はあってもいいように思う。
このスレの住民は、悪戦苦闘したあげくに
このスレにいるわけだから、
たぶんバカにしたりとはしないぞ？
中学生とかが「こんな感じなんですけど、どうでしょうか？」
みたいな話をしたら、たぶん懇切丁寧に説明してくれるはずだ
（逆に、そういう初心者をバカにしたりしたら、総がかりで
ボコられると思う）。
このスレは数学板の中では、かなり優しいスレのうちに
入ると思う。

283:１３２人目の素数さん
18/06/21 19:09:13.28 3VWwsuqs.net
この手の問題は何をしたら証明したことになるのかが難しい
すぐに思いつくのは反例を見つけることだけど見つかる気がしない
この予想が正しかったら証明する方法なくね？って思ってしまう

284:１３２人目の素数さん
18/06/21 20:42:50.94 qX+RK+7d.net
>>273
とりあえず、ルートを逆に辿ることはできるんだから、
一意性は成り立っているわけだ。
だから、「任意の『４で割って１余る数』について、
なんかしらの順序的な保存量が定義できる」というのが表せれば、
証明になるんじゃないか？
現状、コラッツ操作によって値が上がったり下がったりするから、
「順序的な保存量」というのが定義できないわけだから。

285:１３２人目の素数さん
18/06/21 20:46:10.50 qX+RK+7d.net
>>273
あ、保存量として「何ステップで１に到達するか」を取るってのは
ナシだぞ？（笑）　「有限のステップで、必ず１に到達する」って
いうのが証明されてないわけだから。

286:１３２人目の素数さん
18/06/22 09:22:26.66 fZs8skv2.net
>>273
問題構造としては、「原始ピタゴラス数が三分木で表される」って
いうのと、ほぼ逆なんだよな。あっちは「最小の元から初めて、
三つの操作によってすべての元が一意に表せる」ことが解ってて、
「任意の元から最小の元へのルートが求められない」つーのが

287:問題だった。コラッツ問題の場合は、「任意の元から最小の元へのルートが求められることは、かなり確からしい（ただし、本当に最小の元へのルートがあるかは、不明）」。で、「最小の元に二種類の操作を行なうことによって、すべての元（任意の自然数）が一意に表される」かどうかは、いまのところ不明であると。なんか、自然数域から何か別の空間への写像を考えて、その別空間のなかで、ある量に対する半順序構造が成り立つ、みたいなアプローチになるのかな？たとえば f(128) < f(31) とか。

288:１３２人目の素数さん
18/06/22 09:46:11.31 fZs8skv2.net
わかりきったことを雑多に書くので落書きみたいなことに
なってしまうが、いちおう書いてみる。すまぬ。
2^∞＝∞で、「２で割る」操作が無限回必要だから、これは考えない。
したがって、[1, ∞) という自然数の開集合の中で考える。
n が偶数の場合は、n/2 に帰着するので、
「[1, ∞)の中の奇数」（{n|n は奇数かつ n∊[1, ∞)}）について考えれば足りる。
で、たしか
n が n≡3(mod 4) のときは、そこから先に奇数が出てこないので、
「{n|n ≡ 1(mod 4) ∧ n∊[1, ∞)}」について考えれば足りる。
みたいな話になってたような気がするんだけど、これで議論は
足りてるかな？

289:１３２人目の素数さん
18/06/22 17:03:30.74 fZs8skv2.net
>>277
あ、ぜんぜん足りてねぇな。
n ≡ 0 (mod 3) のケースについての話がなんにもない。
そのあたり、真面目に（高校生にも解るように）書いてると、
なんかしらスレを消費するだけなんだよな。
誰か（スレ主とか）が「やれ」って言ってくれりゃあ、
やるけど。

290:１３２人目の素数さん
18/06/22 20:03:26.94 iMFpB+6q.net
ごめん保存量とか知らない単語が出てきて自分には理解できなかった
自分で考えてて思いついたのは数学的帰納法くらいで
1～kの自然数が1に収束するならk+1も1に収束する、ということが言えれば証明できるのかなと
k+1が偶数なら次が(k+1)/2 < kだから1に収束する
k+1が4で割って1余るならkは4の倍数で次の3k+4も4の倍数
次の次が(3/4)k+1 < kだから1に収束する
あとはk+1が4で割って3余る場合を考えればいい
でもその先はパターンが無限の組み合わせになりそうだからこの方法では解けなさそう

291:righ1113
18/06/22 20:38:25.49 8OiWJMk5.net
>>277
ここってどういう意味?
> n が n≡3(mod 4) のときは、そこから先に奇数が出てこないので、

292:１３２人目の素数さん
18/06/22 21:02:12.79 fZs8skv2.net
>>279
> ごめん保存量とか知らない単語が出てきて自分には理解できなかった
いや、数学的には正確になんというか知らんのだが、
全部の要素が順番に並んでて、
「最初のものについて成り立つ」
「あるものについて成り立つならば、“その次のもの”について成り立つ」
「だったら、全部のものについて成り立つ」
っていうのが、数学的帰納法だろ？
現代数学って、「次の数」ベースで成立してる（ペアノの公準。「数え主義」
あるいは「順序数による」定義）で成り立っているので、「加法が成立する」っていう「量に基づく
考え方」（基数による定義）とは、ちょっと相性が悪いんだ。
「１は自然数である」「自然数＋自然数は自然数である」みたいなやりかたは、
現代数学じゃなくって、むしろ「算数」の考え方なんだよ。

293:１３２人目の素数さん
18/06/22 21:11:12.96 fZs8skv2.net
>>280
すまん。言葉が足りなかった。
そのあたりは、いちおう前のほうのエントリで議論は尽くされて
いると思うので、あらためて整理してからまた書く。
しばらく待っててくれ。

294:１３２人目の素数さん
18/06/23 07:13:55.05 if8U6rKp.net
話はかなり基礎的な話になる。
コラッツ予想は、“すべての有限な自然数”は、「偶数だったら２で割る」
「奇数だったら三倍して１を足す」という操作を繰り返してゆくと、
“有限回で” “必ず”１に到達する（そして１→４→２→１という
ループに落ちる）という話だ。
コラッツ予想の対偶は、逆操作である「２倍する」「１を引いて３で割る」という
操作を、１に対して有限回おこなうことで、“すべての数”に到達することができる、
というものだ。つまり、有限な自然数は、「２倍する」「１を引いて３で割る」
という二つの操作によって、１を根とした（有限の高さの）二分木構造を
なす、ということだ。
ここまでは、変なことは言ってないと思う。
２^∞を除く2の冪乗数は、プリミティブだから考えなくていい。
すべての偶数は、根のほうから見ると、奇数に2の冪乗数を
乗じたもので表されるから、「奇数の先にある」し
「奇数と奇数の間に出てくる」わけだから、考えなくていい。
このとき、 n が奇数のとき、3n + 1 は必ず偶数になるので、
コラッツ操作 3n + 1 は (3n + 1)/2 とし、逆問題が
「すべての有限な自然数」ではなくて「少なくともすべての有限な
基数（途中に出てくる偶数は、勘定に入れなくていい）」について
証明すれば足りる。

295:１３２人目の素数さん
18/06/23 07:21:29.24 if8U6rKp.net
ある奇数が 3 の倍数のとき、「×２」の操作を何度行なっても、
3 の倍数になる。そうすると、(3n + 1)/2 の逆操作が行なえない
（結果が自然数でなく分数になってしまう）ので、
「（n ではなく d（odd の d）と表記するとして）3 の剰余群
{0, 1, 2} のうち、d ≡ 1 または 2 のすべての有限な奇数が、1 を
根とした木の上にあることが示されれば、コラッツ予想は肯定的に
証明されることになる」と謂える。

296:１３２人目の素数さん
18/06/23 07:31:26.76 if8U6rKp.net
これをもう一段絞りこんで、4 の剰余群 {0, 1, 2, 3} のうち、d ≡ 1 (mod 4) の
場合にだけ注目すればいい、という話にならないか？ということ。
d ≡ 0 (mod 4) と d ≡ 2 (mod 4) は偶数なので、（逆操作の途中には
出てくるけれども）、証明の本質にはかかわってこない。
d ≡ 3 (mod 4) ということは、「下位ビットが 2 個以上の連続した
オンビット」なので、途中には出てくるけれど、d ≡ 1 (mod 4) の場合に
帰着する（つまり、d ≡ 1 (mod 4) の場合に吸収される）はずだ。
その結果、コラッツ予想は 3 と 4 の剰余群の直積集合上で考えていいわけで、
mod 12 で考えても一般性を失わないはず。
ただし、それで証明ができるかは別問題なんだが (-_-!)

297:１３２人目の素数さん
18/06/23 07:48:51.66 if8U6rKp.net
>>280
× > n が n≡3(mod 4) のときは、そこから先に奇数が出てこないので、
〇 > n が n≡0(mod 3) のときは、そこから先に奇数の枝が出てこないので、

298:１３２人目の素数さん
18/06/23 21:10:19.57 kMgEMQAn.net
以下、左が下位の2進表現とする
x→3x+1
10→00 10
01→11 10
10 01→00 11 10
10 01 01→00 11 11 10
10 01 01 01→00 11 11 11 10
…
27みたいなのはこういうパターンを踏んで大きくなるのか

299:１３２人目の素数さん
18/06/24 06:22:55.46 JZQSNXZT.net
最下位に 1 が連続して出てくると、そこからが
厄介なんですよ。
11 11 11 0### みたいなパターンを
[11 11 1 ]+[10###] と分けたとするでしょう？
そうすると、全体に五回 3x+1 操作を加えることは、
[10###] に５回 3x+2 操作を行なうのと等価になる。
それで 1 への収束が遅れるらしい。
だから、コラッツ予想を (m, n) という２変数に対する操作と
考えて、有限回で (0, 1) に到達するかどうか、と
言い換えるのはどうだろうか、と考えたことがある。

300:１３２人目の素数さん
18/06/24 06:32:53.97 JZQSNXZT.net
31 だと、
11111
*111101
**1110001
***1101011
****10000101
（中略）
*****/*/1101101
*****/*/*10010001
*****/*/**/1110011
*****/*/**/*11011001
*****/*/**/**10010111
*****/*/**/***/11110101
*****/*/**/***/*111000001
*****/*/**/***/**110100011
*****/*/**/***/***1000101001
（中略）
*****/*/**/***/****/*//***/**/111111001
*****/*/**/***/****/*//***/**/*111110111
*****/*/**/***/****/*//***/**/**1111001101
*****/*/**/***/****/*//***/**/***11101100001
*****/*/**/***/****/*//***/**/****11001010011
*****/*/**/***/****/*//***/**/*****101111101001
*****/*/**/***/****/*//***/**/******//1111000111
*****/*/**/***/****/*//***/**/******//*11101010101
*****/*/**/***/****/*//***/**/******//**110000000001
*****/*/**/***/****/*//***/**/******//***101000000011
と、途中で何度も 1 の連続が出てくるんで、なかなか収束しない。

301:１３２人目の素数さん
18/06/24 09:49:32.99 Ke8Ud7bS.net
f(x):=(3x+1)/2
b_k:=2^k-1 (k>1)
とおくと
f(2^(k+1)x+b_k)
=3 2^(k+1)x+3 2^k-2
=2^(k+1)×(3x+1) + (2^k-1) -1
=2^(k+1)f(x)+b_k-1
k>1の場合は

302: f(2^(k+1)x+b_k)=2×(2^(k)f(x)+b_(k-1)) 2で割って以下繰り返すと最後(k=1)は 2f^k(x)になる、と。なんというか……振り出しに戻された感が。

303:１３２人目の素数さん
18/06/24 10:36:18.55 JZQSNXZT.net
>>290
> なんというか……振り出しに戻された感が。
あるある（笑）
連分数とかやってると、なんだかんだで
また φ に戻ってくるとかな。
とはいえ数学って、「既存のアイディアの世界から
出る」つーのがエポックメーキングな仕事になる場合が
多いみたいな気がするから、そのあたりは宿命だと
思って諦めるしかないと思う。

304:１３２人目の素数さん
18/06/24 10:45:37.45 JZQSNXZT.net
>>290
ひょっとして、けっこう昔からプログラマやってる方？
「:=」って、Pascal とかでしょ。
数学屋さんだったら、
b_k:=2^k-1 (k>1)
より
Me(n) = 2^n - 1 (n = 0 のとき偶数。0 < n のとき奇数)
とか書きそうな気がした。私も元がプログラミング畑だから、
数学の分野の言い回しに慣れるのに時間がかかったな。

305:１３２人目の素数さん
18/06/24 13:11:45.44 Ke8Ud7bS.net
プログラマでもあるけど、
数学でも定義で:=表記を使うことはあるよ
卒論はどうだったかなー、とレジュメ見たら使ってたし

306:１３２人目の素数さん
18/06/24 14:11:36.72 JZQSNXZT.net
>>293
そうか。深読みしすぎてゴメン。
なんにせよ数学畑の人が、
このスレに興味を持ってくれているのが
嬉しい（個人的な感想だから、そのあたりは
スレ主との合意が必要なんだが）。

307:１３２人目の素数さん
18/06/24 14:38:08.41 JZQSNXZT.net
スレ主の 78righ1113 氏と相談なんだが、
コテハン（＝固定ハンドル）のほうが、たぶん分かりやすいので、
使っちゃっていいかな？
（別板から変なのが来て、荒れると不本意なので）

308:righ1113
18/06/24 14:40:49.97 prj5qOCW.net
>>295
使っても良いですよ

309:M.B.
18/06/24 15:06:01.07 JZQSNXZT.net
>>296
ありがとうございます。
お婆ちゃんだけど、よろしこ。
前のエントリを明らかにしようと思ったら、
「レスアンカーが多すぎます！」とか言われてハネられちゃったわ。
　　　　　　　　　　　　　　　　　　「梅干し婆」と呼ばれるけれど
　　　　　　　　　　　　　　　　　　鶯泣かせた春もある

310:M.B.
18/06/24 19:41:54.78 JZQSNXZT.net
n を普通の二進数で表すときに「(2)」と表記し、
たとえば 10 = 0101(2)と表すことにする。
これを左右ひっくり返したものを「(r2)」と
表記することにすると、10 = 0101(2) = 1010(r2) と
なる。
Me(k) = 2^k - 1
とおいて、
X(n) = {Me(p) + 2^p × q}
を、
(p, q)
と表記することにする。
q ≡ 3 (mod 4) のとき、q は (r2) で表したときに、
q は 11### … #(r2) で表される。このとき、
操作 A について、A(p, q) は (p + 1, (q - 1)/2) であるとする。
また、q が偶数であるとき、
操作 B について B(p, q) は (p, q / 2) であるとする。
さらに、1 < p のとき、
操作 C について、C(p, q) は (p - 1, (q × 3) + 2) であるとする。
n = 1 のとき、n = (p, q) = (0, 1) である。これをかりに e とおく。
コラッツ予想は、すべての有限の自然数である n について、
n = BBABCAB……e が有限長の記号列である、という主張と
同義である。
― みたいなコトを考えたんだけど、これって方向性として、
どう思います？

311:M.B.
18/06/24 20:12:12.78 JZQSNXZT.net
>>298
あ、ごめんなさい。
q = 0 かつ q ≡ 1 (mod 4)のとき、
D(p, q) = (p, q) = (p, 3×q + 1) = (0, 3×q + 1) っていうのが
抜けてた。

312:M.B.
18/06/24 20:15:43.15 JZQSNXZT.net
>>299
× q = 0 かつ q ≡ 1 (mod 4)のとき、
〇 p = 0 かつ q ≡ 1 (mod 4)のとき、

313:righ1113
18/06/24 20:30:52.33 DiBEd+/F.net
>>298
う～ん、今の時点では何とも……
剰余コラッツ予想の時みたいに、何か部分的な成果があると良いのですが……

314:M.B.
18/06/24 20:49:40.29 JZQSNXZT.net
>>300
肝心なことを書き忘れていました。
A・B・C・D は、演算子あるいは作用素みたいなものなんです。
これに対して、ノルム（絶対値みたいなものです）を (p, q) に
対して与える関数 N((p, q)) を考えます。
このとき、操作 A・B・C・D に対してノルムが単調減少し、
すべての有限な量 (p, q) に対して N() が有限であるということが
証明されれば、コラッツ予想は肯定的に証明された、と
謂えるように思います。
もっとも、N が実数に対して写像されちゃうと、
「１／２を何回掛けても 0 にはならない」みたいに
底抜けになってしまうので、N() はあくまで
整数域に対する関数でないと困るわけですが。

315:M.B.
18/06/24 21:00:26.22 JZQSNXZT.net
> 剰余コラッツ予想の時みたいに、
> 何か部分的な成果があると良いのですが……
p は上下しながら 0 に向かっているというのは
数値実験上は傾向として掴んでいるのですが、
メルセンヌ数を与えたときに、初期値の p を超えちゃう
場合があるんですよね。
>>289 における p = 5 から p = 6 とか。
ただ、>>289 を見てもらえればお分かりになると
思うんですけど、この逆転が起きるのは、q に
(3n + 1) / 2 操作を施した場合に限られていそうに
思うんですよ。
そうなると、「p が増加しない」が謂えて、
「無限ループが存在しない」が謂えれば、
なんとか抑えこめそうな気がしています。
剰余コラッツ予想の場合でも、
「かりに無限ループが存在しても、
その周期は 5×2^60 より長い」みたいな
下限は与えられそうに思うんですが。

316:M.B.
18/06/24 21:11:52.43 JZQSNXZT.net
>>302
なお、仮に N() が具体的に求められたとしても、μ再帰関数である
アッカーマン関数のように、とんでもなく大きい値を与える
関数になってしまい、具体的な上限値が計算できるようなシロモノ
ではなかろう、と予想しています。
だけど有限は有限なので、「少なくとも無限ではない」という意味で、
証明に結びつきうるのではないかと考えています。

317:righ1113
18/06/24 21:18:08.31 DiBEd+/F.net
>>302-304
(上から目線でｽﾏﾅｲ)
いくつかの「思う」を『定理』『補題』として言えれば、もっと素晴らしくなると思います。

318:１３２人目の素数さん
18/06/24 22:21:29.01 fzgyO7V1.net
M.B.さんトリップもつけとけば？
念のため。

319:M.B.
18/06/25 05:43:48.60 i3V6MyI3.net
>>305
じつは、このアイデアは「原始ピタゴラス数は三分木をなす」という
Barning と Hall の定理（小林吹代『ピタゴラス数を生み出す
行列のはなし』参照）が元ネタです。e = {3, 4, 5} に行列
U・D・A を順次掛けてゆくと、すべての原始ピタゴラス数が
一意に表されます。
原始ピタゴラス数は、「互いに素で偶奇が異なる自然数 (m, n)
（0 < m < n）」、または「互いに素な奇数 (p, q)（0 < p < q）」
で表されます。ここで、m × n または p × q が単調減少し、
その減少のしかたが三通りあって、それぞれが U・D・A を掛ける
操作と対応することを示しました。
この定理の “泣きどころ” は、任意の原始ピタゴラス数を与えたときに、
それを e と U・D・A の列の積の形に分解できない（逆問題が解決
されていない）点だったのですが、このアプローチで解決できました。

320:M.B.
18/06/25 05:49:55.64 i3V6MyI3.net
>>307
コラッツ問題は、問題の設定としてはこの逆で、任意の n から
e へのルートがあるのは確からしいのに、それが e に収束するか
どうかが（途中の値が一見カオティックに上下するために）、
「（Barning = Hall 問題のような m × n や p × q のような）
単調減少するノルムに対応させることができていない」という
ところに難関があると考えています。

321:M.B.
18/06/25 05:58:56.50 i3V6MyI3.net
>>307
なお、「泣きどころ」うんぬんの話は、細矢治夫『トポロジカル・インデックスー
フィボナッチ数からピタゴラスの三角形までをつなぐ新しい数学』
にありました。同書には細矢先生が Barning = Hall 問題
にどのようにアプローチしたかが丁寧に書かれていて、興味ぶかく
読ませていただきました。

322:M.B.
18/06/25 06:11:49.38 i3V6MyI3.net
スレ違いですが、{x, y, z} が原始ピタゴラス数、すなわち
x^2 + y^2 = z^2 のとき、
{x, y, z} = {n^2 - m^2, 2× m × n, m^2 + n^2}
がいえて、
{m, ABS(n - 2m)} が新しい m, n の値（順不同。小さいほうが m）に
なります。
なお、e = {3, 4, 5} = (1, 2) です。2 - 1×2 が 0 になっちゃうので、
行きどまりになり、ここが三分木の根になります。

323:M.B.
18/06/25 06:43:11.89 i3V6MyI3.net
あまり見込みはありませんが、「二つの逆コラッツ操作
（「２倍する」と「２倍して１を引いてから３で割る」）が
実質的に同じものと見なせる」ことを示す、というアプローチも
考えられます。
(m, ABS(n - 2m)) → (m, n)
がなぜ三分木に対応するかというと、この操作の逆操作が
・m に n の二倍を足す
・n に m の二倍を足す
・n の二倍から m を引く
という三つの操作に対応するからです（m × n の長方形を
考えるとわかりやすいです。互除法の変形です。互除法
なので、連分数とかかわってきます）。
ただ、このアプローチはせめて「コラッツ操作によって、
任意の n についての中間値が最大どこまで大きくなるか」の
上限値を n の関数として表せないと無理筋なので、
攻めるとすればここかな？と思っています。つまり、「最下位の
オンビット列の連鎖が、どう現れるのか」です。
連投ごめんなさい。m(_ _)m

324:M.B.
18/06/25 17:53:09.88 i3V6MyI3.net
ついでながら、なんでこのスレでのたくっているかというと、
佐藤郁郎先生（URLﾘﾝｸ(www.geocities.jp)）に
「コラッツ予想も、Barning = Hall 問題のノリで
解けるかもしれない」みたいな話をしちゃったのが
きっかけなんですよ。
みなさん、期待されてます。

325:１３２人目の素数さん
18/06/25 20:22:13.67 /XT/YqNK.net
俺予想
xから始まってコラッツの操作で到達できる数のうち最大のものをcollatz_max(x)とする
あるnとcが存在しn<xならばlog(collatz_max(x))/log(x)<=cが言える。

326:M.B.
18/06/25 20:46:18.33 i3V6MyI3.net
>>313
それって、かなり確からしいけど、
リーマン予想みたいに「例外がない」ことを示すのが
難しいっていうのが泣きどころなのよねぇ ……

327:１３２人目の素数さん
18/06/25 21:05:06.15 /XT/YqNK.net
>>314
コテ名乗るならトリつけたほうがよくない？
ひょっとしたらこのスレから世紀の発見ってこともかんがえられるしｗ

328:M.B.
18/06/25 21:17:21.66 i3V6MyI3.net
すでに「コラッツむし」という名前で話題に出ているのですが、
蒸し返しです。
オートマトンに関連する話題なんだけど、
「一斉射撃の問題」というのがあって、これはいろいろ研究されてて
コラッツ問題の解決のヒントになるかもしれないな、と思っています。
「オートマトンが 0 番から m 番まで (m + 1) 個並んでいる。左端の
A0 から、時刻 0 で、ある信号が発せられた。一定の時間後に (m + 1)個が
すべてのオートマトンが同時に特別の状態（「射撃」状態）にはいるように、
オートマトンの動作表を設計せよ。」

329: これを変形すると、「0 から、ある状態にセットされたオートマトンがあったときに、その状態は無限遠（m が無限）まで到達できない」ことが示されるかどうかという話に持ってゆけます。これだと、「２で割る」という操作は「先頭位置がズレてゆく」ことになりますので、また違った面から議論できそうに思います。「歴史的な背景などについては、後藤英一：一斉射撃の問題。数理科学１１－１０、４２－４６（１９７３）を参照のこと。また、小林考次郎：オートマトン理論のパズル、数理科学１９７６年１１月増刊「パズルＩ」にも解説がある。」とのこと。出典は有澤誠『プログラミングレクリエーションーソフトウェア実習のガイド』（近代科学社）、p.132。

330:M.B.
18/06/25 21:20:40.37 i3V6MyI3.net
>>315
べつにいいじゃない。このスレがきっかけになるんなら。
だいたい、独立に発見された定理なんか、山ほどあるでしょうに。

331:１３２人目の素数さん
18/06/25 21:30:29.74 /XT/YqNK.net
ふむ？コテ名乗るような奴はトリもつけたがるものだとおもってたが。
まあ無理強いはしませんがね。

332:M.B.
18/06/25 21:36:29.09 i3V6MyI3.net
「コラッツ予想の解決」、つまり「コラッツ予想が正しい／間違って
いる」とはおそらく関係しないけど、「先頭位置が、必ずしも
「一回一回の操作が終了する」まで待たなくてよくて、先頭から
次々とシグナルが送られてゆく、と考えてもいいわけですよね？
だったら、テープワームみたいな形でネットに放して、
空いてるコンピュータ・リソースを総動員して「どこまで正しいか」を
検証するという手はあるかと思います（犯罪っぽいけど）。

333:M.B.
18/06/25 21:39:48.99 i3V6MyI3.net
>>318
数学板だと、誰が喋ってんのかわかんないと文脈っつーか
脈絡っつーか、そういうのが分かりにくいんじゃないかなー、という
配慮です。
だいたい、あたしの騙りとかって、難しいと思うよ？

334:１３２人目の素数さん
18/06/25 22:22:25.93 /XT/YqNK.net
xから始まってコラッツの操作で到達できる数のうち最大のものをcollatz_max(x)とする。
n以下の自然数の中にlog(collatz_max(x))/log(x)>=3を満たすようなxが存在するか？
という問いはNP問題になると思う。
これをSATとしてあらわしてSATソルバに食わせて一気にデカいnについて解くというのはどうだろうか？

335:１３２人目の素数さん
18/06/25 22:25:29.22 /XT/YqNK.net
いやにNPならないか。
コラッツの過程を計算するのに指数リソース食うかも

336:１３２人目の素数さん
18/06/25 23:08:39.50 /XT/YqNK.net
xからコラッツ逆操作で到達できる数のうち最小のものをcollatz_inverse_min(x)とする。
xを入力としてxとcollatz_inverse_min(x)が等しいかどうかは多項式時間で判定できるか？

337:M.B.
18/06/26 08:03:44.37 0z6GeZu4.net
縦軸に (3n+1)/2、横軸に /2 の回数を取って、
Me(k) についてプロットしてみる、とかいうのも
面白そう。

338:１３２人目の素数さん
18/06/27 20:13:28.48 JI1+mB/E.net
M.Bさんはjava使いなの？

339:M.B.
18/06/27 20:36:49.75 dy3jMf1T.net
>>325
『【好調】Java の宿題ここで答えます【三巡目】』
（ｽﾚﾘﾝｸ(tech板)）
＞＞38 以降とか。
兄者は件のサーバーアプリを再興しようと、
マ板でのさばっておりますわん。

340:righ1113
18/06/29 00:06:15.82 iQFgCDGa.net
剰余コラッツ予想の例のプログラムですが、
Coqに移植できました。
Coqの関数は全て停止するので、例のプログラムも停止する事になって、
『剰余コラッツ予想は真！』
……と言いたいところですが、怪しさ満載ですので、今しばらく調査します。

341:前786
18/06/29 01:00:09.65 CMkNZo9B.net
わくわく
Coq については名前を聞いたことがあるぐらいで詳しくは知りませんが、
なにか手伝えることがあればおっしゃってください。

342:righ1113
18/06/29 01:15:11.78 iQFgCDGa.net
おーお久しぶりです。
Coqというプログラミング言語(定理証明支援系)では、再帰関数を作る際に、停止性をチェックされて、それをパスした関数だけが定義されます。
手伝って欲しいことは後々出てくると思うので、よろしくお願いします。

343:１３２人目の素数さん
18/06/29 03:51:44.66 iREabCnd.net
>>329
> Coqというプログラミング言語(定理証明支援系)では、再帰関数を作る際に、停止性をチェックされて、それをパスした関数だけが定義されます。
最近のCoqの現状は全く知らないのですが、そもそもCoqの文法に従って（チェックされなければ）停止しない関数を書けるような構文になってましたっけ？
Coqは構成的型理論と呼ばれるものに属する形式的体系の１つに基づいているので、その基づいている型理論に即して素直に項の構文（関数はこの構文を使って定義することになるので
この構文がその構成的型理論の体系が与えるプログラミング言語に相当する）を作ると、そもそも停止するか否かがわからないような関数を定義することは構文的に不可能だと理解しているのですが
それとも最近のCoqは書きやすさとかのためにgeneral recursionのような書き方を許す構文も導入しているのかなあ

344:M.B.
18/06/29 06:56:09.36 bG5MqPr9.net
>>327 >>328
おかえりなさ～い！

345:righ1113
18/06/29 07:10:56.55 iQFgCDGa.net
>>330
質問の答えになっているか分からないですが、
今回の方法だと、再帰関数を書き終えた時点で証明モードに入って、そこでの証明を終えると、関数が定義されます。
具体的には、Coq.Program.Wfをインポートして、減少する引数をmeasureで指定して、Program Fixpointで関数を書きます。
URLﾘﾝｸ(www.google.com)URLﾘﾝｸ(d.hatena.ne.jp)

346:１３２人目の素数さん
18/06/29 19:22:32.47 PBV1h0j5.net
もし本当なら相当な成果？

347:righ1113
18/06/29 19:58:55.32 IWPhIwZs.net
いや、待って下さい。なんかダメっぽいんです。詳細はこの後書きます。

348:１３２人目の素数さん
18/06/29 21:27:05.32 KSe/m9fx.net
それにしてもCoq使えるのは凄いな。
あれは高度な数学力とプログラミング力を要するからな。

349:righ1113
18/06/29 21:29:41.42 R9VAP49J.net
>>335
前スレで教えてもらいました。

350:１３２人目の素数さん
18/06/29 22:20:51.29 iREabCnd.net
>>332
レスありがとうございます。
> 今回の方法だと、再帰関数を書き終えた時点で証明モードに入って、そこでの証明を終えると、関数が定義されます。
> 具体的には、Coq.Program.Wfをインポートして、減少する引数をmeasureで指定して、Program Fixpointで関数を書きます。
例を拝見しました。なるほど、関数そのものは構文としては文字通りのfixpointつまりgeneral recursionで定義するのを許す代わりに
停止性を保証するmeasureを自分で与えて停止性証明を正しく構成しなければ関数定義として認めないということですか。
構造帰納法で上手く定義できない関数を扱う上では強引な印象もありますが、実用的にはとても役に立ちそうなアプローチですね。
御教示どうもありがとうございました。

351:１３２人目の素数さん
18/06/29 23:49:39.74 KSe/m9fx.net
はよはよｗ

352:righ1113
18/06/30 00:17:51.21 ePd1LYGC.net
>>334
問題点は、19x+1版にしても、Coqは「停止する」って言っているのです。
19x+1版は、>>94で反例が出ています。
以下が考えられます。
・Coqの

353:停止性の証明が間違っている・オールNothingが出ても無限走行するとは限らないこれらを調査しないといけないのですが、すみませんがマイペースでやらせて下さいf(^_^;

354:１３２人目の素数さん
18/06/30 00:31:00.91 P0VnQOuD.net
つか、Coqが間違ってないとすれば計算が進むたびに減少するなにがしかの量を>>1が見つけたってことだよね？
>>274が言ってたことだよね？
ホントならかなりすごいよね？

355:righ1113
18/06/30 00:44:28.49 ePd1LYGC.net
>>328
>>786氏に見て欲しいことがあるのです。
・オールNothingが出ても無限走行するとは限らない
オールNothingが出た後、本当に無限走行するのか、アルゴリズムで見ていただけないでしょうか。

356:前786
18/06/30 08:42:24.23 f79gd0NI.net
>>341
なるほど了解です。考えてみます。
>>340
これは剰余コラッツ予想(>>2)についての話なので>>274は関係ないかと…

357:前786
18/06/30 10:23:33.09 f79gd0NI.net
って、これはほとんど明らかのように思います。
例えば
「C の元を 3 倍して 1 を加えて C' のどのグループに属するか調べる」
のときにオールNothingが出たとします。
この後に「上の作業で得られた C' のグループ」を用いて組を探すことになりますが、
これは空集合なので再びオールNothingとなります。
以下同様に繰り返し、延々とオールNothingが繰り返さることになります。

358:righ1113
18/06/30 13:47:05.15 LW37VaWU.net
>>343
ありがとうございます。
ということは、僕のCoqの証明がどこか間違っているのですね。お騒がせしました。

次ページ