定理証明手習い (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)
そうなりませんね
意味は同じですが
この形、よく出てくるな