定理証明見習い (17) 部分関数
- 部分関数の置き換えを認めると矛盾が発生する
部分関数の例はこれ
(defun partial (x) (if (partial x) 'nil 't))
こうじゃないのはなぜか
(defun partial (x) (partial x))
いちおう値を返しそうな雰囲気はかもし出しておきたい、くらいかな
であれば、こうじゃないのはなぜか
(defun partial (x) (if (partial x) 't 'nil))
評価してみて返ってくるかどうかで部分関数かどうかを判定するっていう意味合い?
いやちょっと無理があるか
さてpartial
は部分関数なのでこういうの書いても't
になることはないでしょうから
証明なしで定義する必要があります
(J-Bob/prove (my/prelude)
'(((defun partial (x)
(if (partial x) 'nil 't))
...
この間は無理やり公理のリストに付け足してやりましたが
J-Bobのお作法ではlist-extend
というのを使うようです
list-extend
はそんなに特別な処理をしてるわけではなくて、
項目を追加したリストを返す関数ですが、リスト内にすでに同じ項目がある場合は
何もせず元のリストを返します なるほど
(J-Bob/prove (my/prelude) ...)
の代わりに
(J-Bob/prove (list-extend (my/prelude) A) ...)
としてやれば
一時的にmy/prelude
に定義Aを付け加えて証明を記述することができます
いまさら気が付きましたが(J-Bob/define (prelude) ...)
の
prelude
を囲んでるカッコは構文上のカッコじゃなくて
単に関数適用のカッコですね
マクロかと思ってました
で部分関数の置き換えが可能だとどんなことになっていくかやっていきます
以下の...
に置き換えを書いていきます
付録Bだとdethm
の行のインデントがずれてて構造が見にくくなってます
カッコの数は数えないので!
(J-Bob/prove
(list-extend (my/prelude)
'(defun partial (x)
(if (partial x) 'nil 't)))
'(((dethm contradiction () 'nil)
nil
...)))
(略)ということでpartial
が適用できてしまうと'nil
が't
になってしまいます
どういうカラクリかと見てみると
(partial x)
を(if (partial x) 'nil 't)
に置き換えたときに
真偽が反転してます
なので
(defun partial (x) (if (partial x) 't 'nil))
ではそういうことは起こりません そういうことか
これも部分関数ではありますが
部分関数が全部悪いわけじゃないけど念のため全部ダメなことにする、ってことでしょうか
矛盾は引き起こさないとしても値を返さないことがあるんだからやっぱダメかな
部分関数を置き換えるのはまずいとして
じゃあ公理を使って例えば'nil
を(if (partial x) 'nil 'nil)
に
書き換えるのは問題ないんでしょうか
'nil
の値は'nil
ですが(if (partial x) 'nil 'nil)
は値を返さないので
もうすでにこの時点でおかしくなってるはず
いや、それを言うならmy/prelude
にpartial
を追加した時点でおかしいのか
追加できたということは全域であると宣言してるようなものだから
さらにこれは部分関数かどうか
(defun partial (x) (if (partial x) 't 't))
普通に動かしたら無限ループですがif-same
の公理が使えれば't
になります
if-same
を使ってはいけない条件というのがあるんでしょうか
単に関数定義の中では公理による置き換えは使えないというだけかな
同じ形の定理なら証明できますけどだからといって関数が全域であるとは言えなさそう
(J-Bob/prove
(list-extend (my/prelude)
'(defun partial (x)
(if (partial x) 't 'nil)))
'(((dethm partial-theorem (x)
(if (partial x)
't
't))
nil
(() (if-same (partial x) 't)))))
せっかく矛盾を導けたので、矛盾を使って任意の命題を証明する、っていうのが
できないかと思いましたが
「帰結」がないのでDethmの法則が適用できませんね
残念
全域関数でも、矛盾した結果が証明されてしまうものがあるのではないでしょうか?
ありません。
無矛盾性?
どういう証明になるのかな
帰納法でやるんだろうけれども