定理証明手習い (81) 帰納法の構成

前回は全域性の主張の構成
今回は帰納法の構成

後ろから読んでいく

(defun induction/claim (defs seed def)

seedが種、defが定理の定義

  (if (equal seed 'nil)
      (dethm.body def)

種が'nilなら定理の本体を返す

      (induction/defun (app.args seed)
                       (dethm.body def)
                       (lookup (app.name seed) defs))))

そうでなければinduction/defunの値を返す
induction/defunは「Defun帰納法」のことだな

(defun induction/defun (vars claim def)
  (induction/if vars claim (defun.name def)
                (sub-e (defun.formals def) vars (defun.body def))))

ここに相当してる感じ？

Cの帰納的な主張は、このように構成される bodyi 全体に対する主張である。

これも合わせて考えて、

主張 C、関数(defun namef (x1 ... xn) bodyf)、変数 y1 ... yn に対し、 bodyf の x1 を y1 に、...、 xn を yn に置き換えた bodyi の部分式についての主張を次のように構成する。

vars = (app.args seed) = x1 ... xn
claim = (dethm.body def) = C
def = (lookup (app.name seed) defs) = bodyf

ってことだな
で
bodyi は(sub-e (defun.formals def) vars (defun.body def))ってわけだ
お次は

(defun induction/if (vars claim f e)

fは f 、eは bodyi

  (if (if? e)

bodyi がifならば

      (implication
       (induction/prems vars claim (expr-recs f (if.Q e)))
       (if-c-when-necessary (if.Q e)
                            (induction/if vars claim f (if.A e))
                            (induction/if vars claim f (if.E e))))

• (if Q A E)については、 Aに対する主張を Ca、 Eに対する主張を Ceとして、「 Qの帰納法のための前提が Caeを含意する」を主張とする。ただし Caeは、 Caと Ceが等しい場合は Caで、それ以外の場合については(if Q Ca Ce)である。

induction/premsは帰納法のための前提(Premise)のことらしい
そのままっちゃあそのまま

そうでなければ

      (implication
       (induction/prems vars claim (expr-recs f e))
       claim)))

• その他の式 E については、「 E の帰納法のための前提は C を含意する」を主張とする。

これもそのまま

最後に帰納法のための前提

(defun induction/prems (vars claim apps)
  (if (atom apps)
      '()
      (cons (sub-e vars (app.args (car apps)) claim)
            (induction/prems vars claim (cdr apps)))))

主張 C、再帰的な関数適用(name e1 ... en)、変数 x1 ... xn について、この関数適用に対する帰納法のための前提は、 Cに出てくる x1 を e1 に、...、 xn を en に置き換えたものになる。

varsは変数 x1 ... xn、
claimが主張 C 、
appsが再帰的な関数適用(name e1 ... en)、ですね

ふう