定理証明手習い (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
も条件を満たす