6.  包括原理,ZF集合論,ラッセルのパラドックス

集合を表現するのに,{0, 1, 2, 3} ではなく,{ x | x ∈A } とか,{ x | φ(x) } と書く場合があります.というか,この方が一般的です.この書き方だと,非常に大きなサイズの集合や無限個の数の要素の集合を難なく表記することができます.{0, 1, 2, 3} みたいなのはその集合の要素を書き連ねるわけですから,外延的表記であり,{ x | φ(x) } みたいなのは,ある集合の要素が共通して持つ性質 φ(x) で表記するわけですから,内包的表記です.

我々の集合論においても,この内包的表記を可能にしてみましょう.まず決めなくてはいけないのは,内包的性質をどう実現したらいいのかということですが,今簡単に結論を言ってしまえば,それはメンバーの型であり,クラスです.ですから,ここでも集合の性質をCommon Lisp の型で表現しましょう.そうすれば,自前でシステム開発する労力が大幅に低減される.Common Lisp の型システムにのっかって,車輪の再発明はやめましょう,ということです.まあ,このやりかたでうまくいくかどうか,やってみないとわかりませんが.

できあがりの姿として,自然数の集合は,{ x | (and integer (>= x 0)) } みたいに書けたらうれしいな,ということです.そうすると,縦棒の次の部分は型指定子とすればいいのではないか.もちろん既存のCommon Lisp の型を使って,{ x | integer } と書けるし,将来はCLOS の型を使って { x | animal } とか { x | carnivore } とか書けるじゃないか,という話です.まあ,そうなると何が何だか分からなくなる可能性もありますが,逆になるほどクラスとはそういうことかとよく分かるようになる可能性もある.

そうすると,次に外延的表記と内包的表記をどう統一するかという議論が出てきます.今 { x | (and integer (>= x 0)) } と定義されている集合のメンバーにたまたま { 0, 1, 2, 3 } とあったとします.もちろんこれらのメンバーはこの自然数の型定義を満足しますが,これですべて尽くされているわけではないですよね.ほかにもメンバーとなるべき自然数は一杯ある.ですから,これ以上はメンバーの増加や交代はない,という状態でないと,外延的表記と内包的表記を同一とすることはできません.逆に,そうしてもいいという場合という意味で,ここに finalize という概念を持ち込みます.finalize するのは,一番よく分かっている人,あなたか,あるいはエージェントです.つまり,finalize はこれでメンバー確定という積極的な宣言です.finalize されない限り,メンバーはまだ増えるかもしれない.色々な仕事は,集合の性質を調べたり,などは finalize されて初めて安心して実行できます.一方,内包的表記では,これ以外のあれこれという可能性はありません.可能性は書かれたそれで尽くされていますから,いわば最初から finalize されている.

いままでの議論を踏まえて,以下のように集合の定義を拡張しました.

(defclass set ()
  ((type :initarg :type :accessor set-type)
   (elements :initarg :elements :accessor member-of)
   (rank :initarg :rank :accessor rank-of))
  )
(defmethod print-object ((object set) stream)
  (if (slot-boundp object 'type)
      (format stream "{x | ~S}" (set-type object))
    (if (slot-boundp object 'rank)
        (format stream "{~{~S~^,~}}" (member-of object))
      (call-next-method))))
(defun set-p (x)
  (typep x 'set))
(defun set-of (&rest members)
  (make-instance 'set :elements members))
(defun set-by (&key (type t))
  (make-instance 'set :type type))
(defun set (members)
  (make-instance 'set :type type))
;;; Finalize
(defun finalize (set &optional (rank (card set)))
  "Default option is appicable only for ordinal numbers by succesor."
  (setf (rank-of set) rank)
  set)
(defun finalized-p (set)
  (or (slot-boundp set 'type)
      (slot-boundp set 'rank)))

CLOSのクラス定義では構造体定義とは異なり,自動的に型判別のための述語が定義されません.ですからここで set-p を定義しました.クラス set のスロットに新しく type スロットを設けました.内包的表記における記述はここに保存されます.ここに保存されたフォームはCommon Lisp の型判別子として用いることができるものとします.新しく導入された type スロットに対応して,print-object を拡張しました. type スロットに値があればそれが優先的に印刷されます.クラス set のスロットにもう一つ rank スロットを設けました.竹内外史さんによれば rank(x) とは,ある集合 x の順序数のことです.今まで出てきた例でいえば,集合 =1 の rank は 1, 集合 =5 の rank は 5 です.successor による順序数では rank はカージナリティ(要素の数)と等しいのですが,冪集合による順序数では異なっていました.とにかくここでは,だれかが rank を設定してくれるとして,rank が設定されていれば,それは finalize されているものとしました.ですから,print-object でも rank のあるときだけ従来どおりの印刷をしています.そういう実装で足らないことがあるかも知れませんが,我々の順序数に関して言えば十分ですね.ここでちょっと注意.call-next-method をprint-object の中で呼び出しています.メソッド定義の中で呼ばれるとcall-next-method は上位クラスのメソッドを呼び出します.call-next-method に引数を与えることもできますが,もし引数なしの形式だと,このメソッドのパラメータに与えられた値がそのまま引き継がれるだけでなく,実行時に効率のよいコードを生み出します.ですから,通常引数の値を変更しない場合には(ほとんどの場合はそうのはず.around の場合だけ積極的に引数の値を変更したりする),引数なしの形式でcall-next-methodを呼び出すのが正しいコードです.

関数 finalize でもしrank を与えないときは,デフォールトとして与えられた引数 set は successor によるものだとしています.それに合わせて関数 suc を次のように修正します.ただし,+empty+ にもrank を与えておきます.

(defparameter +empty+ (set-of))
(setf (rank-of +empty+) 0)
 
(defun suc (ord)
  (finalize (union-of ord (set-of ord))))

これで,順序数については従来通りとなりました.

zf(11): (defparameter =5 (make-ord #'(lambda () +empty+) 5))
=5
zf(12): =5
{{{{}},{},{{},{{}}}},{{}},{},{{},{{}}},{{{},{{}}},{},{{}},{{{}},{},{{},{{}}}}}}

さていよいよ,内包定義です.もし,set-type の値が型指定子なら,メンバーの所属を判定する関数 in は次のように拡張できます.

(defun in (member set)
  (cond ((slot-boundp set 'type)
         (if (typep member (set-type set))
             (values t t)
           (values nil t)))
        ((slot-boundp set 'rank)   ; finalized
         (if (member member (member-of set) :test #'equals)
             (values t t)
           (values nil t)))
        ((member-of set)
         (if (member member (member-of set) :test #'equals)
             (values t t)
           (values nil nil)))
        (t (values nil nil))))

もし,set-type があるなら,それを取り出して普通に typep で調べます.真であれば <t, t> の2値を返し,偽であれば<nil, t> の2値を返します.これはCommon Lisp の subtypep のやり方に沿ったものです.分からなければ<nil, nil> を返します.今,typep で調べることは確定的に調べられるものとして,typep で nil が返ったときには<nil, t> を返しています.finalize されているときも同様に,member で調べて真なら <t, t> ,偽なら <nil, t> です.そしてset が finalize されていないときでも,そのメンバーが確かに set のメンバーになっているなら <t, t> ですが,そうでないとき,将来そういうこともあるかも知れないという意味で,<nil, nil> を返しています.type も member-of もないならもちろん返す値は <nil, nil> です.

同じような考えで,subset-p を次のように拡張します.

(defun subset-p (x y)
  (when (eq x y) (return-from subset-p (values t t)))
  (cond ((and (slot-boundp x 'type) (slot-boundp y 'type))
         (let ((x-type (set-type x))
               (y-type (set-type y)))
           (when (eql x-type y-type) (return-from subset-p (values t t)))
           (subtypep x-type y-type)))
        ((and (slot-boundp x 'rank) (slot-boundp y 'rank))    ; finalized
         (if (every #'(lambda (e) (member e (member-of y) :test #'equals))
                (member-of x))
(values t t)
(values nil t)))
        ((and (slot-boundp x 'rank) (slot-boundp y 'type))
         (if (every #'(lambda (e) (typep e (set-type y)))
                    (member-of x))
             (values t t)
           (values nil t)))
        ((and (member-of x) (slot-boundp y 'type))
         (if (notevery #'(lambda (e) (typep e (set-type y)))
                       (member-of x))
             (values nil t)
           (values nil nil)))
        ((and (member-of x) (slot-boundp y 'rank))
         (if (notevery #'(lambda (e) (member e (member-of y) :test #'equals))
                       (member-of x))
             (values nil t)
           (values nil nil)))
        (t (values nil nil))))

二つの集合の両方に type が定義してあるなら,それについて subtypep で比較します.両方がmember について finalize されているときは従来通りですが,ただし返す値は2値にしています.x が finalize されていないときは,もし偽であるなら,将来メンバーが減少することはないとして(これを単調増加という),確かに偽であるとして <values nil, t> を返していますが,それ以外なら <nil, nil> です.y は finalize されていなければなりません.さもなければ <nil, nil> を返します.(続く)