あみだくじが無限ループしないことを証明した - にわとり小屋でのプログラミング

どんなあみだくじでも答えにたどり着くことを証明した。 ここでいうあみだくじとは 有限本のくじ(縦棒)がある 縦棒上の点と点を結ぶ横道が有限本ある 横道は水平線だけじゃなく、遠くのくじへ行ったり自身を上に行ったりできる ダメなこと 「ふりだしへもどる」はない 同じ点と点を結ぶことはできない 一方通行はない 一度通ると崩れるマリオのブロックみたいな道はない どちらに行くか選べる分岐みたいなのはない なぜ証明したか PPLで話題になって証明しようかなと思った。 ざっくりとしたアイディア あみだくじを形式的に定義するアイディア くじ(縦棒)の集合があったとき、横道の集まりで一つのあみだくじのデータを表現した。 例えばこのあみだくじは A0--B2, A1--B0, B1--C0 という3本の横道として表現する。横道は端点のペアであり、端点の添字は点の高さで上から順に一つづつ大きい数字になる。各くじ

[ikaironic]

確かに「誰が」は言っていないから嘘ではない

[petite_blue]

coqがrocqという名前になったのは知らなかった

[nmcli]

横棒は2回通るパターンはあるが、縦だけ見れば大丈夫ということか

[hnw]

ハイハイよくあるやつね、と読み進めたらcoq登場してワロタ

[WorldWanderer]

That's a fascinating proof! Never thought about it that way.