kb84tkhrのブログ

何を書こうか考え中です あ、あと組織とは関係ないってやつです 個人的なやつ

定理証明手習い (75) step-args? 〜 seed?

(step-args? defs def args) argsdefの正しい引数かどうか

組み込み関数に渡す引数はクォートされたリテラルでなければなりません。

そういうものだったっけか
はっきり認識できてなかったな
なにかそれっぽいものがあるとは思ってた気がするけど
こんなシンプルな条件だとは思ってなかった

(step-app? defs app) 正しい関数適用の形をしているか
(step? defs step) ステップの形をしているか

ん、ステップは必ず関数適用だったか
ということはifで始まっちゃいけないんだな
これも認識してなかった気がする
今更ながら

(steps? defs steps) ステップの列かどうか

ここらへんから種
いったい何が書けるのか気になってたところ
seedから見ていったほうが理解しやすそう

(seed? defs def seed) seeddefの種として正しいか

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)

defeで呼んでいる関数の定義
varsは今定義しようとしている定理の仮引数
eが種になる式

この関数が真になるのは
eで呼んでいるものが関数であって、
eで呼んでる関数の仮引数の数とeの引数の数が一致していて、
eの仮引数に重複がなくて、
eの引数が定義しようとしている定理の仮引数に含まれているとき

つまり

定義済みの関数に相異なる変数の列を渡した関数適用

ってことだな
(list-induction xs)とかは大丈夫そうだし
align/alignalignも条件を満たす