定理証明手習い (78) sub-var 〜 sub-e
やっと形式チェックではない処理
(sub-var vars args var) 変数に対応する引数
vars 変数のリスト
args 引数のリスト
var 変数
(sub-es vars args es) （複数の）式の置き換え
(sub-e vars args e) （単独の）式の置き換え
ここも複数の式を置き換える関数を作ってからその特殊系として単独の式の置き換えを作ってる
どうして単独の式の置き換えを使ってからmapするようなやり方をしないんだろうか
できそうな気がするけど
ここでは置き換えた項をさらに再帰的に置き換える、といったことはしてないですね
1ステップ分だけの置き換え
J-Bobはもともとそれしかやってないですしね
定理証明手習い (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の定義が順次追加されていくので、先に出てきた関数を呼ぶことが可能
定理証明手習い (75) step-args? 〜 seed?
(step-args? defs def args) argsがdefの正しい引数かどうか
組み込み関数に渡す引数はクォートされたリテラルでなければなりません。
そういうものだったっけか
はっきり認識できてなかったな
なにかそれっぽいものがあるとは思ってた気がするけど
こんなシンプルな条件だとは思ってなかった
(step-app? defs app) 正しい関数適用の形をしているか
(step? defs step) ステップの形をしているか
ん、ステップは必ず関数適用だったか
ということはifで始まっちゃいけないんだな
これも認識してなかった気がする
今更ながら
(steps? defs steps) ステップの列かどうか
ここらへんから種
いったい何が書けるのか気になってたところ
seedから見ていったほうが理解しやすそう
(seed? defs def seed) seedがdefの種として正しいか
defsは関数・定理の定義のリスト
defは今定義しようとしている関数または定理
seedは種
種として許されるのは
'nilか、
関数の定義ならば、定義している関数の仮引数に含まれている変数のみを使った式、か
定理の定義ならば、帰納法の型であるもの
alignを定義するときの(wt x)とか他の関数の(size x)は条件を満たしてる
定理の定義についてはあとで
(induction-scheme? defs vars e) eが帰納法の型かどうか
defsは関数・定理の定義のリスト
varsは今定義しようとしている定理の仮引数
eは種（帰納法の型）
帰納法の型として許されるのは、
関数適用であって、induction-scheme-for?であるもの
(induction-scheme-for? def vars e)
defはeで呼んでいる関数の定義
varsは今定義しようとしている定理の仮引数
eが種になる式
この関数が真になるのは
eで呼んでいるものが関数であって、
eで呼んでる関数の仮引数の数とeの引数の数が一致していて、
eの仮引数に重複がなくて、
eの引数が定義しようとしている定理の仮引数に含まれているとき
つまり
定義済みの関数に相異なる変数の列を渡した関数適用
ってことだな
(list-induction xs)とかは大丈夫そうだし
align/alignのalignも条件を満たす
小さな習慣が小さい
小さな習慣は続いてたり増えてたりします
いいことなんですけど、小さいままなんですよね
大きくしたいんだけど何かやめない限り大きくするすきまがない
うーん
残業？やっぱそこ？
ここんとこ少し増えてるからなあ
それでももう今さら途切れさせるのはもったいないと思って続けるくらいには
習慣づいてるのはプラスな面
でも最低限の目標だけクリアしとこうみたいな日が増えるのはマイナスな面
とりあえずこんな風になんか書いとくだけとかね
うむ
