定理証明見習い (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の法則が適用できませんね
残念

全域関数でも、矛盾した結果が証明されてしまうものがあるのではないでしょうか？
ありません。

無矛盾性？
どういう証明になるのかな
帰納法でやるんだろうけれども