定理証明手習い (85) 演算子の適用

(rands args) argsのクォートをはがす
(eval-op app) 組み込み演算子を適用する

apply-opはタグなしの値を受け取るようになっているので、randsではがしてから
渡します

逆に言うと、組み込み演算子を適用できるのはクォートされた値のみ
変数には適用できない

ってことでいい？

定理証明手習い (84) 演算子

(unary-op rator rand) （組み込みの）単項演算子の演算を行う
(binary-op rator rand1 rand2) （組み込みの）二項演算子の演算を行う
(apply-op rator rands) （組み込みの）演算子の演算を行う

rator、なんだかわかった・・・
opeが省略されてたのか
そりゃ辞書引いても載ってないわ
まあ自分の察しの悪さもたいがいだが
randもランダムとか関係なし

難しいところは特になし

randにはタグがついてないことには注意かな

定理証明手習い (83) Dethmの法則？

具体的な形になった定理をつかう前に、follow-premsで延滞をチェックする必要があります。このチェックにより、等しいことが証明可能な2つの式を表す具体的な帰結が、等式として得られます。

わかったようなわからないような
(equal (car (cons 'a 'b)) 'a)みたいな式が得られる、ってことですかね

follow-premsから見てみます

定理証明手習い (82) 式の置き換え

(find-focus-at-direction dir e) 式eの、dirで指定された部分式

dirがeの適切な位置を示しているかはまったく気にしてない模様
'Qって指定されたけどそもそもeはifじゃないとか
'3って指定されたけど引数が2個しかないとか
そういうの

定理証明手習い (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帰納法」のことだな

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

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

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

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

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

定理証明手習い (79) exprs-recsとそういえば

exprs-recs 式のリストから再帰的な関数適用を抽出する
expr-recs 式から再帰的な関数適用を抽出する

変数なら数えない
クォートなら数えない
ifならQ、A、E部の関数適用を抽出
関数適用で名前が一致したらそれ自身＋引数に含まれる関数適用を抽出
名前が一致しなければ引数に含まれる関数適用を抽出