定理証明手習い (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
が減ってることを言うんでしょうか