kb84tkhrのブログ

何を書こうか考え中です あ、あと組織とは関係ないってやつです 個人的なやつ

定理証明手習い (80) 全域性の主張作り

littleprover 
(defun totality/< (meas formals app)
  (app-c '<
         (list2 (sub-e formals (app.args app) meas)
                meas)))

名前からすると全域性に関する何か
measは尺度のことかな
measの仮引数にappの引数をあてはめたものが
measよりも小さい、という式を作っている
尺度が減っていく、ってやつだな

appはなんだろう
そうか、exprs-recsで関数本体から抽出した再帰呼び出しが入るのかな

後ろから読んだほうがわかりやすそうだ

(defun totality/claim (meas def)

measは尺度、defは関数定義

  (if (equal meas 'nil)

尺度が'nilで

      (if (equal (expr-recs (defun.name def) (defun.body def))
                 '())
          (quote-c 't)
          (quote-c 'nil))

再帰呼び出しがなければ't
あれば'nil

そうでなければ

関数 name の全域性についての主張は、 (natp m) と body に対する主張の連言になる。

というのがこれ

      (if-c
       (app-c 'natp (list1 meas))
       (totality/if meas
                    (defun.name def)
                    (defun.formals def)
                    (defun.body def))
       (quote-c 'nil))))

「 body に対する主張」がtotality/ifの関数適用にあたる

(defun totality/if (meas f formals e)

measが尺度、fが名前、formalsが仮引数、eが関数本体

  (if (if? e)

まずはifだった場合

  • Q、A、Eに対する主張が Cq 、 Ca 、 Ce であるとき、(if Q A E)であれば、 Ca および Ce が同じなら Cq と Ca の連言を主張とし、そうでなければ Cq と (if Q Ca Ce)の連言とする。
      (conjunction
       (list-extend
         (totality/meas meas formals (expr-recs f (if.Q e)))
         (if-c-when-necessary
          (if.Q e)
          (totality/if meas f formals (if.A e))
          (totality/if meas f formals (if.E e)))))

「 Ca および Ce が同じなら」はif-c-when-necessaryが面倒を見てくれるからいいとして

Cq が (totality/meas meas formals (expr-recs f (if.Q e)))で
Ca が (totality/if meas f formals (if.A e))、
Ce が (totality/if meas f formals (if.E e))っていう対応っぽいけど
Cq だけ形が違うのはなんでだ
むしろ下の、ifじゃなかった場合の方に似ている ていうか同じ
Q部にifがこないなんて決まってるわけじゃないはずだしなあ
totality/ifから始めなくても同じだから？

ifじゃなかった場合

      (conjunction
       (totality/meas meas formals (expr-recs f e)))))
  • それ以外の式 E については、 E に出てくる再帰的な関数適用(name e1 ... en)を調べる。まず、尺度 m に出てくる x1 を e1 に、...、 xn を en に置き換えることで、再帰的な関数適用に対する尺度 mr を作る。 E についての主張は、 E に出てくる再帰的な関数適用のそれぞれについての(< mr m)の連言とする。

のうちの

E に出てくる再帰的な関数適用のそれぞれについての(< mr m)の連言とする。

をやってる感じ

「 E に出てくる再帰的な関数適用」 が (expr-recs f e)
「連言とする」がconjunctionにあたる
とすると

(defun totality/meas (meas formals apps)
  (if (atom apps)
      '()
      (cons (totality/< meas formals (car apps))
            (totality/meas meas formals (cdr apps)))))

がやってるのは「それぞれ」くらいか

E に出てくる再帰的な関数適用(name e1 ... en)を調べる。まず、尺度 m に出てくる x1 を e1 に、...、 xn を en に置き換えることで、再帰的な関数適用に対する尺度 mr を作る。

がこれ

(defun totality/< (meas formals app)
  (app-c '<
         (list2 (sub-e formals (app.args app) meas)
                meas)))

できてる

> (totality/claim '(size xs) '(defun len (xs) (if (atom xs) '0 (+ '1 (len (cdr xs))))))
(if (natp (size xs)) (if (atom xs) 't (< (size (cdr xs)) (size xs))) 'nil)