|
|
•
|
パラメータ付き性質はユーザが定義する性質で、単独の名前だけでは表現できないものです。それは、いくつかの性質を 1 つのクラスにまとめたようなもので、そのクラスの中の特定の性質を識別するために、パラメータ付き性質の引数としていくつかの値を与えます。パラメータ付き性質は未評価の関数呼び出しとして表現されます。この関数呼び出しの名前がその性質の名前で、その引数がパラメータです。たとえば、
|
RealRange(...)
ComplexRange(...)
BlockDiagonal(...)
Ring(...)
|
|
はいずれもパラメータ付き性質で、それぞれ特別な意味を持つ性質のクラスを作っています。RealRange を指定するにはパラメータとしてその両端の値と型が必要です。同様に、ComplexRange を指定するには、その 4 つの角の値と型が必要でしょう。また、BlockDiagonal は対角成分の個数と型によって決定され、Ring は集合と基本演算によって決定されるでしょう。(RealRange は重要なので、あらかじめ assume に含まれています。他の 3 つの例は含まれていません。)
|
|
•
|
ここでは、BlockDiagonal の例を通してパラメータ付き性質の定義について説明します。この例では、BlockDiagonal(n,b) であるという性質は、対角線に性質 b を持つ n 個の要素が並ぶ正方行列により満たされます。
|
|
•
|
パラメータ付き性質の定義には、まず次の関数が必要です：
|
`property/included/BlockDiagonal`(a,b)
|
|
たとえば： `property/included/BlockDiagonal` := proc( a:property, b:property )
option remember;
if b=TopProp or a=BottomProp then true
elif type([a,b],[BlockDiagonal,BlockDiagonal]) then
op(1,a) = op(1,b) and Incl( op(2,a), op(2,b) )
elif type(b,BlockDiagonal) then
a=diagonal and Incl(op(2,b),OrProp(complex,diagonal))
# a must be of type BlockDiagonal
elif b=diagonal then Incl( op(2,a), OrProp(complex,diagonal) )
elif Incl( b, SquareMatrix ) = false then false
else FAIL end if
end proc:
|
|
|
さらに、次の型定義が必要です： `type/BlockDiagonal`
|
`type/BlockDiagonal` := 'BlockDiagonal'(integer,property);
|
•
|
言葉で述べると、上の定義では次の項目を実行しています：
|
|
|
(1) 自明な場合に個別対応します。つまり、何にでも含まれる性質か、何でも含む性質が与えられた場合です。
|
|
|
(2) 2 つの引数がともに BlockDiagonal ならば、そのブロック数は一致して、最初の成分の性質はもう一方の成分の性質に含まれるべきです。
|
|
|
(3) BlockDiagonal に含まれるかを調べます。この場合の唯一の可能性は第一引数が対角行列であり、その BlockDiagonal の型が diagonal (すなわち、その成分が diagonal または scalar) のときだけです。
|
|
|
(4) (3) と同様ですが、BlockDiagonal が性質 b に含まれるかを調べる必要があります。
|
|
|
(5) a が BlockDiagonal なのに b が SquareMatrix でなければ、包含関係はありません。
|
|
•
|
この2つの定義を使って、たとえば、次のような計算ができます：
|
p3 := BlockDiagonal(3,NonSingular);
assume( M1, p3 );
isgiven( M1, p3 );
is( M1, BlockDiagonal(3,SquareMatrix) );
|
•
|
他にもその性質を使い易くするのに役立つ関数があります。それは次の2つの関数です：
|
BlockDiagonal(....)
`property/exclusive/BlockDiagonal`(a,b)
`property/foo/BlockDiagonal`( a, [b, ...] )
|
|
`property/included/BlockDiagonal`(a,b) は性質 a が性質 b に含まれるかどうかを決定するものです。この関数は true, FAIL または false のいずれかを返さなければなりません。この関数は a または b の一方が BlockDiagonal というパラメータ付き性質のときだけ呼び出されることになります。
|
|
•
|
関数 BlockDiagonal はデータ構造を簡単にするためのものです。実際、それがその性質のパラメータを引数として受け取ると、その正当性を調べて、もし必要ならばそれを簡単にして、その簡単になった性質を返します。たとえば、次のようになります：
|
BlockDiagonal := proc( n:integer, component:property )
option remember, system;
if n <= 0 then error "invalid arguments"
elif n=1 then component
elif type(component,BlockDiagonal) then
BlockDiagonal( n*op(1,component), op(2,component) )
else 'BlockDiagonal'(args) end if
end proc:
BlockDiagonal(1,SquareMatrix);
BlockDiagonal(3,BlockDiagonal(5,UpperTriangular));
|
•
|
関数 `property/exclusive/BlockDiagonal`(a,b) は 2 つの性質 "a" と "b" が互いに排他的のとき (つまり、"a" と "b" の両方になりえるオブジェクトが存在しないとき)、true を返します。それはその 2 つの性質が空でない交わりを持つとき false を返し、そうでないとき FAIL を返します。たとえば、次のようになります：
|
`property/exclusive/BlockDiagonal` := proc( a:property, b:property )
if type([args],[BlockDiagonal,BlockDiagonal]) then
op(1,a) <> op(1,b) or AreExcl( op(2,a), op(2,b) )
elif type(b,BlockDiagonal) then procname(b,a)
elif Incl(b,SquareMatrix) = false then true
elif Incl(op(2,a),diagonal) and AreExcl(diagonal,b) then true
else FAIL end if
end proc:
AreExcl( BlockDiagonal(10,prime), BlockDiagonal(10,composite) );
AreExcl( BlockDiagonal(5,complex), real );
AreExcl( BlockDiagonal(3,complex), p3 );
|
•
|
最後のものは複素数 と NonSingular な行列が互いに排他的であるということを assume が知らないという事実によります。
|
|
