定理証明手習い (20) 尺度
全域性を証明するために尺度を導入します
関数が再帰的に呼び出されるたびに尺度が減少することを示すことによって
いつかは再帰が終わることを証明します
無限下降法的な何か?
size
はリストを作るために必要なcons
の数でした
以下のような公理を使って全域性を証明します
(size x)
は自然数である(size (car x))
は(size x)
より小さい(size (cdr x))
は(size x)
より小さい
関数の場合は「種」に尺度を入れてやるようです
すると、全域性を主張する式が返されます
> (J-Bob/prove (defun.list2?)
'(((defun list? (x)
(if (atom x)
(equal x '())
(list? (cdr x))))
(size x))))
(if (natp (size x)) (if (atom x) 't (< (size (cdr x)) (size x))) 'nil)
どんなしくみで式を作ってるんでしょうか
みたいな感じでしょうか
例をひとつ見ただけなのでまだなんとも言えません
第8章で説明されるそうです
最終的には付録CがJ-Bob自身の解説なので、そこを読めば完璧?
で、あとは主張の式を公理や関数適用で置き換えていって't
であることを示します
ここは今までと同じ
- 再帰しない関数については全域性は自明
なので証明も不要だったわけですね
そのためにも組み込み関数はすべて全域である必要があると