satisfies - Maple Help

type/satisfies

embed a predicate as a structured type

 Calling Sequence type(expr, 'satisfies'(P1, P2, ... ))

Parameters

 expr - Maple expression P1, P2, ... - predicates

Description

 • The type satisfies provides a mechanism for embedding arbitrary predicates in Maple's type system. It enables you to define a structured type corresponding to an arbitrary predicate without having to pollute the type namespace. This is helpful when used in conjunction with the few Maple facilities (such as the two-argument form of indets) that accept types, but not arbitrary predicates.
 • An expression expr is of type satisfies(P1, P2, ...) if all Pk(expr) evaluate to true, or to And, Or, Xor, Implies, Not constructions that, when converted to their corresponding boolean operators (and, or, xor, implies, not; see convert/boolean_operator), evaluate to true. Also all Pk(expr) are expected to evaluate to either true or false, or to And, Or, Xor, Implies, Not constructions with those meanings.
 • Type satisfies is always used as a structured type with at least one parameter. The function type(expr, 'satisfies'(P)) evaluates to true if the expression expr satisfies the predicate P. More than one predicate P1, P2, ... can be supplied, in which case the expression expr must satisfy all of the predicates P1, P2, ....
 • Type satisfies evaluates the Pk(expr) in the order supplied until an expression evaluates to false. Then the type(expr, 'satisfies'(P1, P2, ...) call returns false. If no predicate returns false, then the value true is returned.
 • Predicates are expected to return normally, without raising exceptions. You can use the ordered evaluation of the predicates to test that any preconditions for error-free evaluations are met. See Example 3.

Examples

Example 1

 Use this type to filter conditions when computing objects of certain type:
 All the functions
 > $\mathrm{indets}\left(F\left(G\left(x,y\right),z\right)H\left(x\right),'\mathrm{function}'\right)$
 $\left\{{F}{}\left({G}{}\left({x}{,}{y}\right){,}{z}\right){,}{G}{}\left({x}{,}{y}\right){,}{H}{}\left({x}\right)\right\}$ (1)
 Only the functions having y
 > $\mathrm{indets}\left(F\left(G\left(x,y\right),z\right)H\left(x\right),'\mathrm{And}\left(\mathrm{function},\mathrm{satisfies}\left(f↦\mathrm{has}\left(f,y\right)\right)\right)'\right)$
 $\left\{{F}{}\left({G}{}\left({x}{,}{y}\right){,}{z}\right){,}{G}{}\left({x}{,}{y}\right)\right\}$ (2)
 Only the functions having y and not having z
 > $\mathrm{indets}\left(F\left(G\left(x,y\right),z\right)H\left(x\right),'\mathrm{And}\left(\mathrm{function},\mathrm{satisfies}\left(f↦\mathrm{has}\left(f,y\right)\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\mathbf{and}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\mathbf{not}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\mathrm{has}\left(f,z\right)\right)\right)'\right)$
 $\left\{{G}{}\left({x}{,}{y}\right)\right\}$ (3)

Example 2

 Use this mechanism to introduce local types within module or procedure bodies. Note that NumberTheory[IsSquareFree] returns true or false when applied to some arguments
 > $m≔\mathbf{module}\left(\right)\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}\mathrm{_export}\left(\mathrm{sqrfree}\right);\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}\mathrm{sqrfree}≔'\mathrm{satisfies}'\left(x→\mathrm{type}\left(x,'\mathrm{odd}'\right),\mathrm{NumberTheory}['\mathrm{IsSquareFree}']\right)\phantom{\rule[-0.0ex]{0.5em}{0.0ex}}\mathbf{end module}:$
 Observe that, unlike global type names, which should always be quoted to protect against unwanted evaluation, a local type defined in this way must not be quoted.
 For example, the following example cannot have quotes, that is, $'m:-\mathrm{sqrfree}'$.
 > $\mathrm{type}\left(7,m:-\mathrm{sqrfree}\right)$
 ${\mathrm{true}}$ (4)
 The global space of names (including the global name sqrfree) remains distinct and so the definition of type m:-sqrfree does not imply the existence of a sqrfree type
 > $\mathrm{type}\left(7,\mathrm{sqrfree}\right)$

Example 3

 Giving predicates in certain order, they are evaluated in that order
 > $\mathrm{map}\left(\mathrm{type},\left[0,1,2\right],'\mathrm{And}'\left('\mathrm{integer}','\mathrm{satisfies}'\left(s↦\mathrm{evalb}\left(s\ne 0\right),s↦\mathrm{type}\left(\frac{1}{s},'\mathrm{integer}'\right)\right)\right)\right)$
 $\left[{\mathrm{false}}{,}{\mathrm{true}}{,}{\mathrm{false}}\right]$ (5)
 While constructing predicates (the procedures testing whether a condition is satisfied), the condition being tester may lead to an error, for example, because the test produces a division by zero.
 > $\mathrm{map}\left(\mathrm{type},\left[0,1,2\right],'\mathrm{And}'\left('\mathrm{integer}','\mathrm{satisfies}'\left(s↦\mathrm{type}\left(\frac{1}{s},'\mathrm{integer}'\right)\right)\right)\right)$
 You can prevent these situations adding more predicates, taking care of the exceptional cases before the predicate which returns an error is considered
 > $\mathrm{map}\left(\mathrm{type},\left[0,1,2\right],'\mathrm{And}'\left('\mathrm{integer}','\mathrm{satisfies}'\left(s↦\mathrm{is}\left(s\ne 0\right),s↦\mathrm{type}\left(\frac{1}{s},'\mathrm{integer}'\right)\right)\right)\right)$
 $\left[{\mathrm{false}}{,}{\mathrm{true}}{,}{\mathrm{false}}\right]$ (6)
 You can use And, Or, Xor, Implies, Not constructions to make them more readable or to have full control of the evaluation rules when constructing your types - these constructions do not automatically evaluate to true or false.
 > $\mathrm{condition}≔f↦\mathrm{And}\left(\mathrm{type}\left(f,\mathrm{function}\right),\mathrm{Not}\left(\mathrm{hastype}\left(\frac{f}{\mathrm{exp}\left(1\right)},\mathrm{function}\right)\right)\right)$
 ${\mathrm{condition}}{≔}{f}{↦}{\mathrm{type}}{}\left({f}{,}{\mathrm{function}}\right){\wedge }{¬}{\mathrm{hastype}}{}\left(\frac{{f}}{{ⅇ}}{,}{\mathrm{function}}\right)$ (7)
 > $\mathrm{type}\left(\mathrm{exp}\left(2\right),\mathrm{satisfies}\left(\mathrm{condition}\right)\right)$
 ${\mathrm{false}}$ (8)
 > $\mathrm{type}\left(\mathrm{exp}\left(1\right),\mathrm{satisfies}\left(\mathrm{condition}\right)\right)$
 ${\mathrm{true}}$ (9)