Most axioms are not computationally useful. Those that are can be explicitly expressed by what Axiom calls an attribute. The attribute commutative("*"), for example, is used to assert that a domain has commutative multiplication. Its definition is given by its documentation:
A domain has commutative("*") if it has an operation "*": (R,R)->R such that .
Just as you can test whether a domain has the category Ring, you can test that a domain has a given attribute.
Do polynomials over the integers have commutative multiplication?
Do matrices over the integers have commutative multiplication?
Attributes are used to conditionally export and define operations for a domain (see ugDomainsAssertions ). Attributes can also be asserted in a category definition.
After mentioning category Ring many times in this book, it is high time that we show you its definition: Ring
There are only two new things here. First, look at the $$ on the last line. This is not a typographic error! The first $ says that the is to come from some domain. The second $ says that the domain is ``this domain.'' If $ is Fraction(Integer), this line reads coerce(n) == n * 1$Fraction(Integer).
The second new thing is the presence of attribute `` ''. Axiom can always distinguish an attribute from an operation. An operation has a name and a type. An attribute has no type. The attribute unitsKnown asserts a rather subtle mathematical fact that is normally taken for granted when working with rings.With this axiom, the units of a domain are the set of elements that each have a multiplicative inverse in the domain. Thus and are units in domain Integer. Also, for Fraction Integer, the domain of rational numbers, all non-zero elements are units. Because programs can test for this attribute, Axiom can correctly handle rather more complicated mathematical structures (ones that are similar to rings but do not have this attribute).