定理証明手習い (69) implication
implicationも見ておこう
- 前提が0個の場合、含意は e0 によって表す。
ここに対応
(if (atom es)
e前提が es (式のリスト)、帰結が e なのでこうなります
> (implication '() '(equal x 'a))
(equal x 'a)コードではあとは全部まとめてこうなっててシンプル
(if-c (car es)
(implication (cdr es) e)
(quote-c 't)))これでいいんなら含意の定義もこの形にしてしまってもいいような気がするんですけど
前提が1個の場合とそれ以上の場合で分かれてますね
- 前提が1個の場合、その前提を e1 とすると、含意は
(if e1 e0 't)によって表す。
前提が1個の場合、(cdr es)は要素が0個になるので
(implication (cdr es) e)は単にeとなります
ということでコードを実行しても定義と同じ結果になります
> (implication '((equal x 'a)) '(equal y 'b))
(if (equal x 'a) (equal y 'b) 't)次
- 2個以上の前提がある場合には、それらを e1 e2 ... en とすると、 e1 が「 e2 ... en の連言が帰結 e0 を含意する」ということを含意する、と表す。
ちょっとややこしいですね
コードを直接解釈して同じような書き方をするとこうなります
同じなんでしょうか
- 2個以上の前提がある場合には、それらを e1 e2 ... en とすると、 e1 が「 e2 ... en が e0 を含意する」ということを含意する、と表す。
前提が2個の場合をまずはコードの流れで解釈すると
「 e2 が e0 を含意する」は(if e2 e0 't)、
e1 がこれを含意するから全体は (if e1 (if e2 e0 't) 't)となります
> (implication '((equal x 'a) (equal y 'a)) '(equal x y))
(if (equal x 'a) (if (equal y 'a) (equal x y) 't) 't)なってる
次に定義にしたがって考えてみると
『「 e2 ... en 」の連言』は単に e2 だから「 e2 ... en 」の連言が帰結 e0 を
含意する」は「 e2 が e0 を含意する」、つまり (if e2 e0 't) となります
e1 がこれを含意するから全体は (if e1 (if e2 e0 't) 't)ですね
同じです
さて本番
前提が3個の場合をコードの流れで解釈すると、
「 e2 e3 が e0 を含意する」はさっきの結果を使って (if e2 (if e3 e0 't) 't)、
e1 がこれを含意するから全体は (if e1 (if e2 (if e3 e0 't) 't) 't)となります
> (implication '((equal x 'a) (equal y 'a) (equal z 'a)) '(equal x y))
(if (equal x 'a) (if (equal y 'a) (if (equal z 'a) (equal x y) 't) 't) 't)おｋ
次に定義にしたがって考えてみると
『「 e2 e3 」の連言』は (if e2 e3 'nil) ですので「 e2 e3 の連言が帰結 e0 を
含意する」は (if (if e2 e3 'nil) e0 't) となります
e1 がこれを含意するから全体は (if e1 (if (if e2 e3 'nil) e0 't) 't)ですね
これでいいの？
(if e1 (if (if e2 e3 'nil) e0 't) 't)
= (if e1 (if e2 (if (if e2 e3 'nil) e0 't)
(if (if e2 e3 'nil) e0 't))
't)
= (if e1 (if e2 (if e3 e0 't)
(if 'nil e0 't))
't)
= (if e1 (if e2 (if e3 e0 't) 't) 't)いいんだな
でも腑に落ちない
- 2個以上の前提がある場合には、それらを e1 e2 ... en とすると、 e1 が「 e2 ... en が e0 を含意する」ということを含意する、と表す。
の方が定義もシンプルだし結果もシンプル、しかも連言の定義の
- 3個以上の式 e1 、 e2 、...、 en の連言は、 e1 と、 e2 から en までの連言との連言である
とも形がそろうのに
どういうことだろう
