定理証明手習い (71) bound?, exprs?, expr?

(bound? var vars) varが束縛されているか

varsは束縛変数のリスト
varsが'anyならば束縛されていなくても't

(exprs? defs vars es) 式のリストが正しいか

今まで出てきた関数の中ではなかなかの大モノ

まず引数から
esは式のリスト、defsはdefunやdethmのリストだろう
varsは変数のリストだろうけど、文脈からして束縛変数のリストかな？
あとは読みながら確かめる

(defun exprs? (defs vars es)
  (if (atom es)
      't

esの要素にアトムはないとして、esが空っぽになったら成功
esに要素があれば、先頭の要素について

      (if (var? (car es))
          (if (bound? (car es) vars)
              (exprs? defs vars (cdr es))
              'nil)

変数ならばそれが束縛されているかどうかを確かめる
束縛されていれば、残りの式をチェック
束縛されていなければエラー

変数でなければ進む

          (if (quote? (car es))
              (exprs? defs vars (cdr es))

quoteならチェック不要で成功
残りの式をチェック

quoteでもなければ先へ進む

              (if (if? (car es))
                  (if (exprs? defs vars (if-QAE (car es)))
                      (exprs? defs vars (cdr es))
                      'nil)

ifならば、Q、A、Eが正しいかどうかを確認
Q、A、Eが正しければ残りの式をチェック
正しくなければエラー

ifでもなければ先へ進む

                  (if (app? (car es))
                      (if (app-arity? defs (car es))
                          (if (exprs? defs vars
                                      (app.args (car es)))
                              (exprs? defs vars (cdr es))
                              'nil)
                          'nil)
                      'nil))))))

関数適用ならばアリティを確かめてから関数適用の引数が正しいかどうかを確かめる
問題なければ残りの式を確認
正しくなければエラー
定理を使った式はapp?であると判定されますが
app-arity?からargs-arity?を呼んだところでdethmが無視されてエラー判定

関数適用でもなければエラー

図体が大きい割にはわかりにくいところはなかった
condがあれば図体が大きくも見えなかったかもね

expr? 式が正しいか

こっちは式がひとつ
式をリストに入れてexprs?に渡してるだけ

なんか
こっちに処理の本体をを入れて、exprs?はリストの要素に対してexpr?を呼び出すだけ、って
ほうが素直な気がするけど

(exprs? defs vars (if-QAE (car es)))とか
(exprs? defs vars (app.args (car es)))みたいな書き方ができなくて面倒ってことかな