余帰納法についての質問と回答
-
- いいね！0
Κeіsuke Νakanο
@ksknac
一年生向けの少人数授業でCoqを学習するテーマを提案したのですが， 他のほぼすべてのテーマで定員が埋まる中，このテーマだけが希望者が一人もいなかったそうです．😇 eng.tohoku.ac.jp/edu/ip/
2019-08-22 15:56:33
cutsea110
@cutsea110
@ksknac 資料のswap siteの形式化ですが、441の例で証明木がありますけど、これ停止しないということを余帰納法(cofix)で証明できるというふうに思って良いんでしょうか？ 行き着く先の公理ってこの場合は無いはずですよね？
2019-08-22 20:06:33
Κeіsuke Νakanο
@ksknac
@cutsea110 はい，こちらは余帰納法による証明の例で証明木は無限（正規木）になります．以前書いた論文が元ネタになっています． doi.org/10.1007/978-3-…
2019-08-22 20:12:50
cutsea110
@cutsea110
@ksknac 余帰納法による証明というのがピンときてないので的外れかもしれませんが… 例えば441列のように具体的であれば少し証明木を展開することで開始状態と同一になって無限に続くと言えそうですが、TPPMark2018のように一般的な列に対して証明出来るようなロジックだと思って良いですか？
2019-08-22 20:55:03
Κeіsuke Νakanο
@ksknac
@cutsea110 短い文字数でうまく伝わるかわかりませんが，「一般的な列に対して」というよりは「無限に続くという性質を」証明できる」というのが余帰納法の特徴です． 帰納法が「帰納的なものを仮定とする命題の証明法」であるのに対し， 余帰納法は「余帰納的なものを帰結とする命題の証明法」と言えます．
2019-08-22 21:06:21
cutsea110
@cutsea110
@ksknac 例えば数学的帰納法だと任意のnについてP(n)が成り立つことを証明したいけど、余帰納の場合はP(n)を証明したいのではなくて、その構造全体が無限に展開可能であることを証明するのが目的だってことですかね。 個々のP(n)はなんになるんでしょう？
2019-08-22 21:33:50
Κeіsuke Νakanο
@ksknac
@cutsea110 余帰納法によって証明する命題の典型例として，「二つのプログラムが等価であること」とか「二つの非決定性オートマトンが同じ文字列集合を生成すること」とかがあります． どちらも齟齬なく無限に続けられることを示している感じがしますね．
2019-08-22 21:47:24
cutsea110
@cutsea110
@ksknac 正直分かったとは言い難いですが、いくつかキーワードも頂けたので、もうしばらく色々調べまわってみます。 ありがとうございました。
2019-08-22 22:09:43
S (ﾂｲｰﾄはｽﾚｯﾄﾞ全体をご確認ください)
@esumii
@cutsea110 @ksknac 横からすみません。もしご参考になれば。sumii.hatenablog.com/entry/20110830…
2019-09-19 08:34:32
cutsea110
@cutsea110
@esumii @ksknac あ、それは初っ端に読まさせていただきました。 あと akitsu-sanae.hatenablog.com/entry/2017/12/… からのTaPL 21章。 でも、いざ証明に使われているのを見ると余帰納法による証明の論理というのが、どういう理屈でなにを証明しているのかやっぱり分からなかったので。。
2019-09-19 08:41:39
S (ﾂｲｰﾄはｽﾚｯﾄﾞ全体をご確認ください)
@esumii
@cutsea110 @ksknac ザックリですが例えば（適当な言語で）停止するプログラムについては、停止するまでのステップ数に関する帰納法で、Pに関する性質が証明でき（る場合があり）ます。（続
2019-09-19 08:51:38
S (ﾂｲｰﾄはｽﾚｯﾄﾞ全体をご確認ください)
@esumii
@cutsea110 @ksknac 一方、例えばプログラムPが「停止しない」ことを証明するには「P→Q（PがQに状態遷移する）かつQが停止しない」を証明すれば良いですが、Q=Pの場合も「あり」（余帰納法）になります
2019-09-19 08:51:57
cutsea110
@cutsea110
@esumii @ksknac この例の余帰納法では、Pから遷移する先はPしかない、ということを示すことで遷移は停止しないということを証明しようとしている。 と理解して良いですか？
2019-09-19 09:07:49
S (ﾂｲｰﾄはｽﾚｯﾄﾞ全体をご確認ください)
@esumii
@cutsea110 @ksknac あ、はい、簡単のために遷移は決定的と考えても良いですが、非決定的でも停止しない（無限に長い）遷移列が存在するという意味です
2019-09-19 09:22:05
S (ﾂｲｰﾄはｽﾚｯﾄﾞ全体をご確認ください)
@esumii
@cutsea110 @ksknac ちなみに循環していなくてもP→P1→P2→P3→…のように無限に続く場合も同様です
2019-09-19 09:23:14
cutsea110
@cutsea110
@esumii @ksknac 例えば、 X: 任意の状態からの遷移先が常にある という事実(示すべきこと)から Y: 遷移は停止しない、という余帰納的な帰結 を導出できるのは、これはもう公理だと思って良いのでしょうか？この論理自体が余帰納法というものだと理解して良いでしょうか？
2019-09-19 10:12:19
S (ﾂｲｰﾄはｽﾚｯﾄﾞ全体をご確認ください)
@esumii
@cutsea110 @ksknac （正確に書くとTAPLみたいな教科書的になってしまいますが大雑把には）帰納的定義から帰納法が従うのと同様に、余帰納法は余帰納的定義から従うので、公理というか定義より従うということで良いと思います。（続
2019-09-19 10:25:43
S (ﾂｲｰﾄはｽﾚｯﾄﾞ全体をご確認ください)
@esumii
@cutsea110 @ksknac ここでいう「停止しない」の（余帰納的）定義は、「Pが停止しないならば、P→QなるQが存在する」「P→QかつQが停止しないならば、Pも停止しない」を満たすようなプログラム（状態）Pの最大の集合を、停止しないプログラム（状態）の集合とする、という定義です。
2019-09-19 10:29:48
cutsea110
@cutsea110
@esumii @ksknac １つ目の言明ですが、Qが停止しないことは不要ですか？ 「Pが停止しないならば、P→QなるQが存在して停止しない」とはならない？ 一瞬 Pが停止しない iff P→QかつQが... という同値関係として理解すればいいのかと思ったのですが微妙に違いそうだったので確認ですけど。
2019-09-19 11:07:25
S (ﾂｲｰﾄはｽﾚｯﾄﾞ全体をご確認ください)
@esumii
@cutsea110 @ksknac あ、その２つの条件は「かつ」です。もう少しちゃんと書くと、(∀P∈S.∃Q.P→Q)∧(∀P.(∃Q∈S.P→Q)⇒P∈S)を満たす最大のSが「停止しないプログラム（状態）」の集合、という定義です
2019-09-19 11:18:50
cutsea110
@cutsea110
@esumii @ksknac 帰納法だと証明したい性質Pには色々ありえて利用例もたくさんあって分かりやすいのですが、余帰納法の場合このPに相当する性質が見えなくて困惑します。 登場する性質としては余帰納的な帰結「停止しないこと」しかなくて。
2019-09-19 11:50:36
S (ﾂｲｰﾄはｽﾚｯﾄﾞ全体をご確認ください)
@esumii
@cutsea110 @ksknac ksknac先生も挙げた、「２つのプログラム（状態）が等価である」も、無限ループし得るプログラム（状態）の組について余帰納的に定義・証明される性質の典型だと思います。（続
2019-09-19 12:03:58