kb84tkhrのブログ

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

定理証明手習い (26) 7. びっくりスター!

第7章はスター型関数に関する定理の証明
題材となるスター型関数はこれ

(defun ctx? (x)
  (if (atom x)
      (equal x '?)
      (if (ctx? (car x))
          't
          (ctx? (cdr x)))))

まずは全域性の証明
種は(size x)
証明すべき式はこれ

(if (natp (size x))
  (if (atom x)
      't
      (if (< (size (car x)) (size x))
          (if (ctx? (car x))
              't
              (< (size (cdr x)) (size x)))
          'nil))
  'nil)

この関数が全域であるという主張は、本書の中でも特に複雑なものです。

そうですか
でも証明は特に難しくはありません

全域性の主張をどうやって構成するのかは、第8章で詳しく説明します。

おおざっぱに考えると
(if (natp (size x)) ... 'nil)はオマジナイで
あとは関数の形をもとにしつつ
(car x)(cdr x)を見かけたらsizeが小さくなっていくことを
確かめるって感じでしょうか
(equal x '?)は全域だってわかってるから'tに変換するってことかな
でも全域だからって(atom x)'tに置き換えちゃうとこれは変
明確なルールにするとすればどうなるんでしょう?
Q部はそのままとか?
もうちょっと何かありそう
Q部が再帰することもあるでしょうし
その時は1段ifを増やしてsizeが減ってることを言うんでしょうか