定理証明手習い (33) 全域性の主張の作り方

8章では全域性の主張の作り方をやるんでした

題材はこれ

(defun add-atoms (x ys)
  (if (atom x)
      (if (member? x ys)
          ys
          (cons x ys))
      (add-atoms (car x)
                 (add-atoms (cdr x) ys))))

再帰のところが少し変わった形になっていますが
尺度はいつもどおり(size x)で
J-Bob/proveに尺度を与えてやると普通に全域性の主張が出力されます

そこをあえて手作りしてやるのがこの章
証明自体は出てきませんし自分でやってもすぐ

まずこの再帰呼び出しについて考えます

(add-atoms (car x) (add-atoms (cdr x) ys))

この関数適用ではadd-atomsの定義におけるxを(car x)に
ysを(add-atoms (cdr x) ys)に置き換えています

これと同様な置き換えを、尺度である(size x)に対して行うと(size (car x))になります
これが(add-atoms (car x) (add-atoms (cdr x) ys))という関数適用に対する尺度だそうです

わかるようなわからないような？
じゃあ(size x)は何に対する尺度？

定義らしきものに戻ってみます

尺度というのは、関数の定義と一緒に提示される式です。尺度の式では、それまでに定義済みの全域関数と、関数の定義に出てくる仮引数だけを参照して良いことになっています。尺度の式は、定義している関数が再帰的に呼び出されるたびに減少する自然数を返さなければなりません。

関数適用に対する尺度がなんなのかはかいてありませんがなんとなくそういう感じのものということで進みます

関数適用のたびに尺度（これは元の関数に対する尺度でしょうね）が減るという主張は
すなわち(size (car x))が(size x)よりも小さい、
すなわち(< (size (car x)) (size x))という主張になります

さらに、(add-atoms (cdr x) ys)も再帰的な関数適用です
同様に考えると、(add-atoms (cdr x) ys)に対する尺度は(size (cdr x))となり
適用時に尺度が減少すると言う主張は(< (size (cdr x)) (size x))となります

というところから逆算すると前半は
(add-atoms (car x) (add-atoms (cdr x) ys))という形を見て
あ、なんか二重に再帰してる、なんかやばそう、とか思わないで
単に(add-atoms (cdr x) ys)を単なる引数と見て扱う、ってことでいいみたいですね

合わせるとこうなります

(if (< (size (car x)) (size x))
    (< (size (cdr x)) (size x))
    'nil)

これは(< (size (car x)) (size x))と(< (size (cdr x)) (size x))の
両方が真であるときのみ真になる式で、つまりふたつの式のANDをとっています
式がふたつ以上になってもifをつなげていけばANDが取れます
難しそうな説明が書いてありますがつまりそういうことです

ANDのことを連言といいますが、そうやってつながっていくイメージから来てるのかなあ？

さて順番が逆転してる気がしますが元の定義は(atom x)かどうかで処理が分かれています
(atom x)の場合はどうなんでしょうか
こちらは再帰呼び出しがないので全域、ということで即'tでいいようです

ということで(size x)は常に減っていきそうな感じになりましたので
(size x)は自然数だよ、と言ってあげれば関数がいつかは値を返すと
無限下降法ですね

でも定義で尺度は自然数、って決めてるのに「もし尺度が自然数ならば」っていうのは
ちょっと不自然な気がするなあ
いや自然数っていうのは定義に含まれてるわけじゃないのか？

それに(size x)の減少がいつかは行き止まりにたどりつくといっても
たどりついたときにちゃんと値を返してくれるって言えるのかな？
この関数の場合だと(size x)がゼロになる＝xがアトム＝'tを返す、でいいわけだけど
っていうのは暗黙でセットになってるのかな？
それともそういうのまで含めて実際には尺度が減る一方＆尺度は自然数、でかならず値が返るもの？
よく考えればそうなってる気もしないではない

ところで尺度が(size x)だというのはどうやって決めるんでしょうか？
再帰呼び出しの引数に出てくる変数ってのはいいとして
じゃあysはどうして出てこないんでしょうか？
まあ見ればいらなさそうなのはわかりますが厳密に言うとどういうルール？