定理証明手習い (37) 自然な再帰
スター型でダメならどうすればいいのでしょうか
ここではadd-atomsで使われている再帰について考えます
add-atomsで使われている再帰は「自然な再帰」でしょうか
carやcdrをたどっていく再帰に比べれば複雑ですが
不自然かというとそうでもない気もします
自然な再帰では、どの引数も、同じままか、与えられた引数の構造の一部分に置き換えられます。
これが「自然な再帰」の定義かと思いましたがそうではありませんでした
これまでに出てきた範囲では、ということかな
(add-atoms (cdr x) ys)の引数は、ysと同じままでもないし、ysの構造の一部分になっているわけでもありません。
「(add-atoms (cdr x) ys)の引数」っていうと(cdr x)とysのことのように思えますが
ysはysと同じままですね
何か違うことを言っているのかな
ふたつ合わせて、ってことでしょうか
(add-atoms (cdr x) ys)そのもののことを言っている？
ここはいつもどおりなんとなくそんな感じということでスルーしておきます
で、結論は
なんだそうです
自然な再帰よりも帰納法が先にある、って言いたいんでしょうか
先に進むしかないですね
ちょっと変わった？再帰でしたからね
ところで証明したいのはset?/atomsやset?/add-atomsなのに
add-atomsばっかり注目されててset?が登場してこないのはどうしてなんでしょう？
再帰的に呼ばれないから、ってことでいいのかな？
いやそれも違うか
内側で呼ばれてるから？
ctx?/subもそうでした
全域性の主張ではxとysがあってysは消えちゃうんだけれども
なぜかというとそもそも尺度にysが入ってないから、という理由がありました
ただなんで尺度にysが入らなくていいかってところまで遡るとまたわからなくなってきますが
結局、証明できるんだからいいだろ、って話なんでしょうか
なにかの理論だか手順だかに従うと勝手にset?やysは消えていくんでしょうか
コードの形だけから判断できるルールはありそうな感じではありますが
