定理証明手習い (76) extend-rec 〜 defs?

(extend-rec defs def) ???

定義済みのリストに関数の新しい定義を追加してるんだけれども
ただ自分を呼ぶだけの関数を追加している
なんだこれ

(def-contents? known-defs formals body) 仮引数と本体が正しい形か

known-defsは定義済みの関数・定理のリスト
いつもdefsと言ってるのになぜここだけことさらにknownと言っているんだろう
チェックしてるのは仮引数に重複がないことと、本体が正しい式かということ
名前は渡されてもいない

(def? defs def) 正しい定義か

defsが定義済みの関数・定理でdefはこれから定義しようとしている関数・定理

まず、定理を定義している場合
まだ定義されていない名前で、仮引数と本体が正しい形であること

関数を定義している場合も
まだ定義されていない名前で、仮引数と本体が正しい形であること

ただし、定義済みリストに自分自身を追加している・・・
これかextend-recのやっていることは
関数・定理のリストに自分自身を追加しているというのは
再帰呼び出しを認めるっていうことだな
recはrecordかと思ってたけどrecursiveか
勘が悪かった

ここまで形のチェックばっかりやってきたけど
考えてみたら関数が全域だから形さえ合っていれば必ず値があるんだな
なにかが腑に落ちた

(defs? known-defs defs) 正しい定義の列か

known-defsにdefsの定義が順次追加されていくので、先に出てきた関数を呼ぶことが可能