下記にオレンジ色で示したif式のQuestion部は、どちらも同じ(set? (add-atoms (cdr a) bs))という意味です。 知ってた しかし、if-nest-Aやif-nest-Eで単純な形にはできません。 先に言ってくれ！

テキストに沿って証明を進めます ここ、自分で考えたらやっぱりけっこう大変なんだろうなあ

Defun帰納法はかなり適用範囲が広そうなやり方です Defun帰納法は、自分たちで書くどんな関数でも使えるのでしょうか？ 帰納的な主張を構成する方法にしろ、全域性の主張を構成する方法にしろ、どんな関数に対しても構成はできます。 ifの位置にもよるけど持…

リスト型帰納法やスター型帰納法はDefun帰納法に含まれるそうです リスト型帰納法はlist-inductionから作ります

Defun式帰納法、とか言ってまた難しく書いてあります ていうか前よりわからないので今回も定義にしたがって追ってみます

ということでadd-atoms用の帰納法が作れるのならどんなものでしょうか list-inductionのときは主張を読んでみたら普通に帰納法だねって感じだったので まず自分で普通に考えてみます

スター型でダメならどうすればいいのでしょうか ここではadd-atomsで使われている再帰について考えます add-atomsで使われている再帰は「自然な再帰」でしょうか carやcdrをたどっていく再帰に比べれば複雑ですが 不自然かというとそうでもない気もします

8章から続いて、atoms関連の関数・定理について考えていきます set?はmember?を呼び出しているのでだんだんこの世界も複雑になってきました set?、member?、add-atomsの全域性については8章で証明済みです

8章では関数の全域性の主張の作り方をやりました 9章では定理の帰納法の作り方をやります 具体的に言うと、list-inductionとかstar-inductionに当たるものを作るということです いやちょっと違うな

っていう話を 関数 (defun name (x1 ... xn) body) および尺度 m が与えられたら、 body の部分式に対して次のようにして主張を構成する。 とか言って難しく書いてあります 難しいのでadd-atomsを1字1句このとおりにやってみます

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

まずmember?とset?の定義が出てきますがこれは下準備 いままでどおりにやるだけです (if (natp (size ys)) ...)は定理にしておきますね

次のフォーカスでctx?/tを使えるでしょうか？ はい、オレンジ色で示したぜんていがあるので使えます。あとでctx?/tの証明はしないといけませんけどね。 あとでいいんだっけ？

これは以前行きづまった(if (equal x '()) 't 'nil)を(equal x '())に変形するにちょっと似てる？ 定理証明手習い (28) 補助定理 - kb84tkhrのブログ さて(if (equal a b) 't 'nil)はどうかな

前回の記事書いてみて思ったのは ((A A 1 1) (equal-if x '?))とかを並べて書いてあるコードを見るより 途中経過の式を並べたものを見るほうがわかりやすいなってこと

(ctx? x)という前提が真の場合、そのifのAnswer部にある(ctx? x)を'tに置き換えられるでしょうか？ む これは以前行きづまった (if (equal x '()) 't 'nil)を(equal x '())に変形する にちょっと似てる？ 置き換えてよいのではないでしょうか。真である前提…

こんな定理を証明します (dethm ctx?/sub (x y) (if (ctx? x) (if (ctx? y) (equal (ctx? (sub x y)) 't) 't) 't)) そういえばこの間 'tってなんだよ'tって、と思いましたがこれはたぶん定理は常に'tでないといけないので入れてあるってことでしょう 定理証…

第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…

本書の目標は、帰納法を使うことで再帰的な関数についての事実を明らかにする方法を読者に知ってもらうことです。 って話でしたがやっと帰納法です 証明にも再帰を使えるんですか？ はい、使えます。 証明における再帰のことを、帰納法と呼びます。 ここでは…

Ifの持ち上げを何回か書いてると面倒になってきます これがパターンであるのなら定理として証明してしまえばいいのでは、 と思ったのですがそもそもパターンがJ-Bobで表現できるのかなあ 書けるとしたらこんな感じなんでしょうか (J-Bob/prove (defun.remb) …

ここでは何をやってるって言ったらいいのかな 再帰する関数の全域性が証明できるようになったので 再帰する関数を使った定理を証明する（ための準備）、でいいのかな 0要素のリスト、1要素のリスト、2要素のリストについて 定理を証明していきます 証明にも…

このまえも出てきたpartialの証明 本に書いてあることをコードで書くとこうなります > (J-Bob/prove (my/prelude) '(((defun partial (x) (if (partial x) 'nil 't)) (size x) ((Q) (natp/size x)) (() (if-true (if (< (size x) (size x)) 't 'nil) 'nil)))…

2つめの引数に含まれる'?をすべて1つめの引数の値に置き換える、subという関数を考えましょう。 これはScheme手習いで言うところの「スター型」(*のついた)関数になります car側も再帰するやつです (cons (sub x (car y)) (sub x (cdr y)))の部分は証明だと …

全域性を証明するために尺度を導入します 関数が再帰的に呼び出されるたびに尺度が減少することを示すことによって いつかは再帰が終わることを証明します 無限下降法的な何か？ sizeはリストを作るために必要なconsの数でした 以下のような公理を使って全域…

前回のlist?シリーズでlist?のA部の(equal x '())(=list0?)が list1?やlist2?では'nilに置き換えられているのは 何か一般的な書き換え規則があるんでしょうか Scheme風に書いた方では#tが#fになってます 何かあるような気がしますが思いつきません 他の再帰…

対話的定理証明器という言葉を見かけました j-bobに1行足しては結果を見てまた1行足す、ってやってるのを思い出して ああこれは対話してたんだ、と思うなど さて (defun list0? (x) (equal x '())) (defun list1? (x) (if (atom x) 'nil (list0? (cdr x)))) …

部分関数の置き換えを認めると矛盾が発生する 部分関数の例はこれ (defun partial (x) (if (partial x) 'nil 't)) こうじゃないのはなぜか (defun partial (x) (partial x)) いちおう値を返しそうな雰囲気はかもし出しておきたい、くらいかな であれば、こう…

全域とは、どんな値を渡しても関数が値を持つということ この間pairは全域、って話が出てました 組み込み関数は、すべて全域です。 そうだったんですか！ そうだったんですか！ Scheme手習いでは lのcarは何ですか。 ここで lは'()です。 答えはありません。…

「4. これが完全なる朝食」のはじめに 関数list0?を定義してください。 (defun list0? (x) (if (equal x 'oatmeal) 'nil (if (equal x '()) 't (if (equal x '(toast)) 'nil 'nil))) はいはい、やり直しましょうね。 (defun list0? (x) (equal x '())) って…

この証明がもうちょっと短くできますねと書いてあります (J-Bob/prove (dethm.in-first-of-pair) '(((dethm in-second-of-pair (a) (equal (in-pair? (pair a '?)) 't)) nil ((1 1) (pair a '?)) ((1) (in-pair? (cons a (cons '? '())))) ((1 Q 1) (first-o…