This page is a guide to an archive of mathematical traits. The traits are written in the Larch Shared Language (LSL). The traits do not duplicate the traits in Guttag and Horning's handbook, but add to them.
The traits are freely available, both through this page, an alphabetical index, and by anonymous ftp from ftp.cs.iastate.edu in file pub/larch/Math/Math-traits.tar.gz. (The README file contains similar information to this page.)
This collection of traits constitutes a small LSL handbook. (Other handbooks are also available.) Contributions are welcome for correcting, extending, and enhancing it.
Many of the traits in this directory are concerned with the definition of the real numbers.
The trait Real defines the sort R which is the real numbers. It is based on the trait RealClosedField, and also uses a trait FieldSugars; its implications use the traits DenseOrder and UnboundedOrder.
The trait RealClosedField defines the notion of a real closed field, with the help of the trait PolynomialFunctions.
The trait RealConversions includes the trait Real, and the traits Rational and Float (from Guttag and Horning's book). It defines several conversion functions to and from the Reals. It also uses the rounding traits described below.
The trait PolynomialFunctions treats polynomials as functions. It uses the trait Polynomial to specify polynomials (in one variable) over a ring. the trait Polynomial uses the trait PolynomialRing, but also uses the trait Coefficients as an auxiliary data structure.
A less well-developed set of traits for the construction of the real numbers is based on mathematical sequences. The construction itself is found in the trait RealConstruction, and it uses the trait MathSequence.
More interesting, probably, are the traits for mathematical sequences. the trait MathSequence defines an ordering on the primitive notion of a mathematical sequence described in the trait MathSequenceBasics.
The trait VectorSpace defines vector spaces over a field. The trait VectorSpace is defined with the help of a trait DistributiveRingAction.
The trait VectorSpace is used by the trait Vector, which defines vectors with an inner product and length over a real closed field.
An action of a monoid on a set is a way of producing a new element of the set from an element of a monoid and an element of the set. (Examples are scaling of vectors, transitions in finite state machines, etc.) The trait M_Set describes such actions.
The trait LinearMonoidAction describes the action of a monoid on an abelian group. It uses the trait M_Set.
The trait DistributiveRingAction describes the action of a ring on an abelian group; this is similar to a vector space, but less restrictive. This trait uses the trait LinearMonoidAction.
The trait FieldSugars defines an operator (__/__) for division in totally-ordered fields; it includes the trait RingSugars. The trait RingSugars defines the infix __-__ operator for subtraction.
Note that the trait RealClosedField defines the sqrt operator which gives the positive square root of a number.
The trait Between defines operators for three and four-way comparisons on a partial order.
The trait Abs defines the absolute-value operator for a totally-ordered group.
The traits MonotonicallyIncreasing, MonotonicallyDecreasing, StrictlyDecreasing, and StrictlyIncreasing can be used to state various implications about the monotonicity of a function.
The trait Round describes various ways to round a rational into an integer. It uses the traits Floor and the trait Ceiling to define the floor and ceiling operators.
Thanks to Steve Garland, Don Pigozzi, and especially to Pierre Lescanne for help with these traits. Thanks to John Penix for his lsl2html tool.
This work was supported in part by NSF grant CCR-9593168.
Permission is granted for you to use the traits in the ftp directory for educational and scholarly purposes, and for commercial use in specifying software, but the copies may not be sold or otherwise used for direct commercial advantage; this premission is granted provided that this copyright and permission notice is preserved on all copies. All other rights reserved.