定理証明手習い (68) J-Bob/if関連（てきとう

(defun if-c-when-necessary (Q A E)
  (if (equal A E) A (if-c Q A E))) 

お、これはアレだな
Defun帰納法の

Caeは、 Caと Ceが等しい場合は Caで、それ以外の場合については(if Q Ca Ce)である。

だなきっと

全域性の主張の方はすこし違った形だけど、部分的には同じところがあるからそっちでも使うかも？

Aを返したり（タグ付きの）(if-c Q A E)を返したりしてるってことは
Aもタグ付きの表現で渡されるってことだな
Q、Eもきっとそう

conjunctionは連言、implicationは含意の定義を反映したもののようです
が

conjunctionとimplicationは、適切に入れ子になったif式を変換して、式からなるリストにする関数です。

は反対じゃないかなあ
式からなるリストをif式に変換してませんか？

• 0個の式の連言は'tである。

はここに相当してそう

  (if (atom es)
      (quote-c 't)

ここのatomはアトムかどうかというよりも'()かどうかを判定してると見ます

リストが空っぽならば(quote-c 't)を返します
タグ付きの値を返すんですね

• 1個の式 e1 の連言はe1である。

      (if (atom (cdr es))
          (car es)

式が1個ならその式
ってことはesの要素もタグ付きの式だと思われます

• 2個の式 e1 と e2 の連言は、 e2 が tの場合は e1 、それ以外の場合は (if *e1* *e2* 'nil) である。
• 3個以上の式 e1 、 e2 、...、 en の連言は、 e1 と、 e2 から en までの連言との連言である

がまとめてこれになってるのかな

          (if-c (car es)
                (conjunction (cdr es))
                (quote-c 'nil)))))

e1 が (car es) 、 e2 から en までの連言が (conjunction (cdr es))で
そのふたつの連言を取れば上の形になります
ただし e2 が tの場合は e1 、っていう部分は反映されてませんね
結果的にはそうなる、ってことかな

やっぱり式のリストをif式に変換してますね

ところでテスト書いてて思ったんですが式の表現ってどうしたもんですかね
(if (equal x 'a) 'b 'c)はこうやって作るのがスジでしょうか

(if-c (app-c 'equal (list 'x (quote-c 'a))) (quote-c 'b) (quote-c 'c))

面倒ですね
評価すると元どおり

> (if-c (app-c 'equal (list 'x (quote-c 'a))) (quote-c 'b) (quote-c 'c))
(if (equal x 'a) 'b 'c)

少し前に出てきた

クォートされた式は、J-Bobの定義と同じ構文を利用してJ-Bobに渡せます。

っていうのはあんまりピンときてなかったんですが
(if-c (app-c 'equal (list 'x (quote-c 'a))) (quote-c 'b) (quote-c 'c))の代わりに
(if (equal x 'a) 'b 'c)を渡していいですよ、って言ってくれてたのかな
そうだなきっとそうしよう

こうやって書いてたテストが

(my/test "conjunction/3exp"
         (conjunction (list (app-c 'equal (list 'x (quote-c 'a)))
                            (app-c 'equal (list 'x (quote-c 'b)))
                            (app-c 'equal (list 'x (quote-c 'c)))))
         (if-c (app-c 'equal (list 'x (quote-c 'a)))
               (if-c (app-c 'equal (list 'x (quote-c 'b)))
                     (app-c 'equal (list 'x (quote-c 'c)))
                     (quote-c 'nil))
               (quote-c 'nil)))

これで済むのは大きすぎる

(my/test "conjunction/3exp"
         (conjunction '((equal x 'a) (equal x 'b) (equal x 'c)))
         '(if (equal x 'a) (if (equal x 'b) (equal x 'c) 'nil) 'nil))

ところで

ただし e2 が tの場合は e1 、っていう部分は反映されてませんね
結果的にはそうなる、ってことかな

> (conjunction '((equal x 'a) 't))
(if (equal x 'a) 't 'nil)

そうなりませんね
意味は同じですが

この形、よく出てくるな