Parametric Properties for the Assume Facility
Description
A parametric property is a property, defined by the user, which cannot be expressed as a single name. This corresponds to cases where we are defining classes of properties, and the arguments to the parametric property are the values which identify the particular property within the class. A parametric property is represented as an unevaluated function call. The name of this unevaluated function call is the name of the property, its arguments are the parameters. For example,
RealRange(...)
ComplexRange(...)
BlockDiagonal(...)
Ring(...)
are all parametric properties, as they determine a class of properties, which can be specialized in each case.
A RealRange is a segment of the real line specified by the values of its two extremes (two real numbers); similarly a ComplexRange is a rectangle in the complex plane specified by two complex numbers.
BlockDiagonal would be determined by the number and type of the diagonal components and Ring could be determined by the set and basic operations. (RealRange, due to its importance, is already included in assume; the other three examples are not).
We will explain the definition of parametric properties through the example of BlockDiagonal. In this example, the property of being BlockDiagonal(n, b) is satisfied by square matrices which contain n objects with property b on their diagonal.
The definition of a parametric type requires at least the function:
`property/included/BlockDiagonal`(a,b)
for example:
`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:
and the type definition:
`type/BlockDiagonal`
`type/BlockDiagonal` := 'BlockDiagonal'(integer,property);
In words, the above definition performs the following checks:
Isolate the trivial cases, inclusion of the bottom or inclusion in the top.
If both arguments are BlockDiagonal, then the number of blocks should coincide, and the property of the first components should be included in the property of the second.
Testing for an inclusion in a BlockDiagonal, the only possibility is that the first argument is a diagonal matrix, and that the BlockDiagonal is of type diagonal (that is, its components are either diagonal or scalars)
Same as (3), but when we want to test the inclusion of a BlockDiagonal in property b
If a is BlockDiagonal and b is not even a SquareMatrix then there is no possible inclusion.
With these two definitions we can do some computation, for example:
p3 := BlockDiagonal(3,NonSingular);
assume( M1, p3 );
isgiven( M1, p3 );
is( M1, BlockDiagonal(3,SquareMatrix) );
Other functions contribute more to the usefulness of the property; these are:
BlockDiagonal(....)
`property/exclusive/BlockDiagonal`(a,b)
`property/foo/BlockDiagonal`( a, [b, ...] )
`property/included/BlockDiagonal`(a,b) determines whether property a is included in property b. This function should return true, FAIL or false only. This function will only be invoked when one of a or b is a BlockDiagonal parametric type.
The function BlockDiagonal is the simplifier of the data structure. As such it receives as arguments the parameters of the property and has to check their validity, simplify them if necessary and return the simplified property. For example,
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
BlockDiagonal(1,SquareMatrix);
BlockDiagonal(3,BlockDiagonal(5,UpperTriangular));
The function `property/exclusive/BlockDiagonal`(a,b) returns true if the two properties "a" and "b" are mutually exclusive (that is, no possible object could be both an "a" and a "b"). It returns false when the two properties have a non-empty intersection and FAIL otherwise. For example:
`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
AreExcl( BlockDiagonal(10,prime), BlockDiagonal(10,composite) );
AreExcl( BlockDiagonal(5,complex), real );
AreExcl( BlockDiagonal(3,complex), p3 );
The last one is due to the fact that assume does not know that complex are mutually exclusive with NonSingular matrices.
See Also
assume
ComplexRange
RealRange
Download Help Document
