内包的表記の集合の性質を Common Lisp の型で表記することにして,typep を利用した in や,subtypep を利用した subset-p を定義しました.これらは次のように一見調子よさそうに見えますが,実は型指定子に satisfies を使った場合にはうまく動きません.

zf(2): (defparameter +NNN+ (set-by :type '(integer 0 *)))
+NNN+
zf(3): (defparameter +INT+ (set-by :type 'integer))
+INT+
zf(4): (subset-p +NNN+ +INT+)
t
t
zf(5): (subset-p +INT+ +NNN+)
nil
t
zf(6): (subset-p (finalize (set-of 0 1 2)) +INT+)
t
t
zf(7): (subset-p (finalize (set-of 0 1 2)) +NNN+)
t
t
zf(8): (subset-p (finalize (set-of -1 0 1)) +INT+)
t
t
zf(9): (subset-p (finalize (set-of -1 0 1)) +NNN+)
nil
t

ここで (integer 0 *) という型指定子は,CLtL2 にある第4.6節の「簡略化を行う型指定子」というものです.上記を見るとうまくいっています.ところが同じことを型指定子の satisfies を用いてしようとするとこうなります.

zf(13): (defun natural-number-p (x)
          (and (typep x 'integer) (>= x 0)))
natural-number-p
zf(14): (deftype natural-number () '(satisfies natural-number-p))
natural-number
zf(15): (typep 1 'natural-number)
t
zf(16): (typep 0 'natural-number)
t
zf(17): (typep -1 'natural-number)
nil
zf(18): (subtypep 'natural-number 'integer)
nil
nil

CLtL2 第4.3節「述語を持つ型指定子」にあるように,1変数の述語を用意しておいて,それを (satisfies 述語) として型指定子にすることができます.確かにここにあるように,typep についてはうまく動くのですが,subtypep になると,意味的には先の (integer 0 *) と同じであるにもかかわらず,<nil, nil> が返ってきました.これは一体どうしたことでしょう.実は subtypep の説明にこんなことがかいてあります.

処理系は多くの場合,実際は与えられた型の間の関係を決定できるかも知れないのに,簡単に「諦めて」2つの nil の値を返している.・・・ subtypep は,引数のうちの一つか両方に satisfies,and,or,not,member を含まない限り,第2の値として nil を返すことは許されない.

おいおい,satisfies があったら,分からないと簡単に「諦めて」もいいのかよ,といいたくなりますね.not は前々から言っているように大変なんで,まあしかたがないとして,and と or は何とかしてほしい.集合のベン図を考えていただければすぐ分かりますが,and は共通集合(intersection),or は和集合(union) に相当します.巨人の肩の上に乗ろうと思ったら,巨人がそれほどでもなかったということでしょうか.

実はsubtypep のやることはあらかじめ決まっているCommon Lisp のデータ型については,コード内で両者を見て真偽を判定しています.まあ,効率化のために色々細工はあるにせよ.ところがユーザが新しく定義するデータ型については,たとえば integer (実は (integer * *) と同じこと)を (integer 0 *) と比較することは,まあ何とかできるわけです.これも subtypep の中でコード化されている.ところが (satisfies natural-number-p) になると,これを比較するには natural-number-p のコードを理解しなければならない,というわけで「諦めて」しまうわけです.

プログラムコードを理解しているわけではないですが,このへんのことを論理的にきちんとやっているのが述語論理(description logic)という分野で,それはセマンティックウェブのOWL の理論的基礎にもなっています.述語論理において行う主要なタスクは二つあって,いわば typep と subtypep の質問にきちんと答えることなんですよ.ですから,述語論理の成果をCommon Lisp に取り入れると,もうちょっとましになることは確かなのですが,まあちょっとこのブログの範囲をこえることになるのは,確かなことですね.

ここでは,まあ適当に進めさせていただきます.えーっと,and と or だけについては,きちんと押さえておきたいですね.でもそうすると,結局論理システムを少し導入せざるを得なくなるのですけどね.