kb84tkhrのブログ

何を書こうか考え中です あ、あと組織とは関係ないってやつです 個人的なやつ

定理証明手習い (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)

どんなしくみで式を作ってるんでしょうか

  • 尺度は自然数である
  • ifのQ部はそのまま
  • 再帰は引数の尺度が現在の尺度よりも減っているという式に変換
  • それら以外の式(全域と分かってる式ってことかな)は'tに変換

みたいな感じでしょうか
例をひとつ見ただけなのでまだなんとも言えません
第8章で説明されるそうです
最終的には付録CがJ-Bob自身の解説なので、そこを読めば完璧?

で、あとは主張の式を公理や関数適用で置き換えていって'tであることを示します
ここは今までと同じ

  • 再帰しない関数については全域性は自明

なので証明も不要だったわけですね
そのためにも組み込み関数はすべて全域である必要があると