kb84tkhrのブログ

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

定理証明手習い (67) J-Bob/何

ひとことでどういうグループかは言い難い

(if-QAE e) if型からQ、A、Eのリストを作る
(QAE-if e) Q、A、Eのリストからif型を作る

こうやっても書けるけどlist3と`if-cで作ってる
その方がスジがいいんだろうか

(defun if-QAE (es) (untag es))
(defun QAE-if (es) (tag 'if es))

こうは書けないんだな

(defun if-QAE untag)

これなら通るけどJ-Bob的には非合法だろう

(define if-QAE untag)

ratorって何

(defun rator? (name)
  (member? name '(equal atom car cdr cons natp size + <)))

何かの略?
組み込み関数ってなんだっけ built-in function かな?
ぜんぜん違うな

こういう関数だと、'equal'atomなら'tを返すのは当然として
それ以外のときには絶対に'nilを返すってことを言わなきゃだな
どう書けばいいかな
こんな感じか('equal'atom以外は省略)

(dethm rator?/nil (x)
  (if (equal x 'equal)
      't
      (if (equal x 'atom)
          't
          (equal (rator? x) 'nil))))

rator? 組み込み関数かどうか
rator.formals 組み込み関数の仮引数のリスト

def.name defun型またはdethm型のname
def.formals defun型またはdethm型のformals

どうもこのへん、関数がどういう考え方でグループに分けられているのかよくわからない
後方参照ができない、ってのはあるとして
defun、dethmグループとifグループとかに分けられそうな気はするんだけど