math

Type Members

1. trait AffineSpace extends AnyRef

   

   An abstract principal homogeneous space over the additive group of a linear space.

   An abstract principal homogeneous space over the additive group of a linear space. Vector addition acts freely and transitively over the point set. To the extent practicable, the following axioms should hold.

   Axioms:

   • 𝓅 + zero == 𝓅 for every point 𝓅 in this.
   • (𝓅 + 𝐮) + 𝐯 == 𝓅 + (𝐮 + 𝐯) for every point 𝓅 and all vectors 𝐮, 𝐯 in this.
   • (𝐯: Vector) => 𝓅 + 𝐯 is a bijection for every point 𝓅 in this.

   Example:

   1. // You can abstract over affine spaces by parameterizing a class or
      // function with a subtype of AffineSpace with Singleton. Type elements
      // with the #Point, #Vector and #Scalar type projections of your
      // AffineSpace type parameter.
      def testAffineSpaceOperations[A <: AffineSpace with Singleton](
          p: A#Point, q: A#Point, u: A#Vector, v: A#Vector): Unit = {
        assert((p + u) + v == p + (u + v), "associativity of point-vector addition")
        assert(p + (-v) == p - v, "existence of point-vector subtraction")
        assert((p + v) - (q + v) == p - q, "existence of point-point subtraction")
      }
      
      // Alternatively, functions can use path-dependent types of an AffineSpace parameter.
      def testAffineSpaceIdentities(A: AffineSpace)(p: A.Point, q: A.Point, v: A.Vector): Unit = {
        import A._
        assert(p + zero == p, "existence of additive identity vector")
        if (p + v == q + v) assert(p == v, "uniqueness of points")
      }

   Version

   0.1

   Since

   0.0

2. trait CompleteField extends Field

   

   A complete abstract field structure.

   A complete abstract field structure. Addition associates and commutes, and multiplication associates, commutes, and distributes over addition. Addition and multiplication both have an identity element, every element has an additive inverse, and every element except zero has a multiplicative inverse. Completeness implies that every Cauchy sequence of elements converges. To the extent practicable, the following axioms should hold.

   Axioms for addition:

   • if 𝑎 and 𝑏 are elements in this, then their sum 𝑎 + 𝑏 is also an element in this.
   • 𝑎 + 𝑏 == 𝑏 + 𝑎 for all elements 𝑎, 𝑏 in this.
   • (𝑎 + 𝑏) + 𝑐 == 𝑎 + (𝑏 + 𝑐) for all elements 𝑎, 𝑏, 𝑐 in this.
   • this has an element zero such that zero + 𝑎 == 𝑎 for every element 𝑎 in this.
   • to every element 𝑎 in this corresponds an element -𝑎 in this such that 𝑎 + (-𝑎) == zero.

   Axioms for multiplication:

   • if 𝑎 and 𝑏 are elements in this, then their product 𝑎 * 𝑏 is also an element in this.
   • 𝑎 * 𝑏 == 𝑏 * 𝑎 for all elements 𝑎, 𝑏 in this.
   • (𝑎 * 𝑏) * 𝑐 == 𝑎 * (𝑏 * 𝑐) for all elements 𝑎, 𝑏, 𝑐 in this.
   • this has an element unit != zero such that unit * 𝑎 == 𝑎 for every element 𝑎 in this.
   • if 𝑎 is in this and 𝑎 != zero then there exists an element 𝑎.inverse such that 𝑎 * 𝑎.inverse == unit.

   The distributive law:

   • 𝑎 * (𝑏 + 𝑐) == (𝑎 * 𝑏) + (𝑎 * 𝑐) for all elements 𝑎, 𝑏, 𝑐 in this.

   Completeness axiom:

   • every non-empty subset of this with an upper bound has a least upper bound.

   Example:

   1. // You can abstract over complete fields by parameterizing a class or
      // function with a subtype of CompleteField with Singleton. Type elements
      // with the #Element type projection of your CompleteField type parameter.
      def testCompleteFieldOperations[F <: CompleteField with Singleton](a: F#Element, b: F#Element, c: F#Element): Unit = {
        assert(a + b == b + a, "commutativity of addition")
        assert((a + b) + c == a + (b + c), "associativity of addition")
        assert(a * b == b * a, "commutativity of multiplication")
        assert((a * b) * c == a * (b * c), "associativity of multiplication")
        assert(a * (b + c) == (a * b) + (a * c), "distributivity of multiplication over addition")
      }
      
      // Alternatively, functions can use path-dependent types of a CompleteField parameter.
      def testCompleteFieldIdentities(F: CompleteField)(a: F.Element): Unit = {
        import F._
        assert(zero + a == a, "existence of additive identity")
        assert(a + (-a) == zero, "existence of additive inverse")
        assert(unit != zero && unit * a == a, "existence of multiplicative identity")
        assert(a * a.inverse == unit, "existence of multiplicative inverse")
      }

   Version

   0.1

   Since

   0.0

3. class DimensionException extends RuntimeException

   

   Indicates a dimensional mismatch.

   Indicates a dimensional mismatch.

   Version

   0.0

   Since

   0.0

4. trait F2 extends FN

   

   An abstract 2-dimensional vector space over a ring.

   An abstract 2-dimensional vector space over a ring.

   Version

   0.1

   Since

   0.0

5. trait F2x2 extends Ring with FMxN

   

   An asbtract 2 by 2 matrix space over a field.

   An asbtract 2 by 2 matrix space over a field.

   Version

   0.1

   Since

   0.0

6. trait F3 extends FN

   

   An abstract 3-dimensional vector space over a ring.

   An abstract 3-dimensional vector space over a ring.

   Version

   0.1

   Since

   0.0

7. trait F3x3 extends Ring with FMxN

   

   An asbtract 3 by 3 matrix space over a field.

   An asbtract 3 by 3 matrix space over a field.

   Version

   0.1

   Since

   0.0

8. trait F4 extends FN

   

   An abstract 4-dimensional vector space over a ring.

   An abstract 4-dimensional vector space over a ring.

   Version

   0.1

   Since

   0.0

9. trait F4x4 extends Ring with FMxN

   

   An asbtract 4 by 4 matrix space over a field.

   An asbtract 4 by 4 matrix space over a field.

   Version

   0.1

   Since

   0.0

10. trait FMxN extends VectorSpace

    

    An abstract M by N matrix space over a ring.

    An abstract M by N matrix space over a ring. Matrix spaces describe linear maps between vector spaces relative to the vector spaces' assumed bases. Matrix addition associates and commutes, and scalar multiplication associates, commutes, and distributes over matrix addition and scalar addition. Matrix and vector multiplication also both associate and distribute over matrix addition. Vectors in the row space multiply as columns on the right, and vectors in the column space multiply as rows on the left. Addition and scalar multiplication both have an identity element, and every matrix has an additive inverse. To the extent practicable, the following axioms should hold.

    Axioms for matrix addition:

    • if 𝐀 and 𝐁 are matrices in this, then their sum 𝐀 + 𝐁 is also a matrix in this.
    • 𝐀 + 𝐁 == 𝐁 + 𝐀 for all matrices 𝐀, 𝐁 in this.
    • (𝐀 + 𝐁) + 𝐂 == 𝐀 + (𝐁 + 𝐂) for all matrices 𝐀, 𝐁, 𝐂 in this.
    • this has a matrix zero such that zero + 𝐀 == 𝐀 for every matrix 𝐀 in this.
    • to every matrix 𝐀 in this corresponds a matrix -𝐀 in this such that 𝐀 + (-𝐀) == zero.

    Axioms for scalar multiplication:

    • if 𝑥 is a scalar in this and 𝐀 is a matrix in this, then their product 𝑥 *: 𝐀 is also a matrix in this.
    • (𝑥 * 𝑦) *: 𝐀 == 𝑥 *: (𝑦 *: 𝐀) for all scalars 𝑥, 𝑦 and every matrix 𝐀 in this.
    • Scalar has an element unit such that unit *: 𝐀 == 𝐀 for every matrix 𝐀 in this.

    Axioms for vector multiplication:

    • If 𝐀 is a matrix in this and 𝐯 is a vector in the row space of 𝐀, then their product 𝐀 :⋅ 𝐯 is a vector in the column space of 𝐀.
    • (𝐀 ⋅ 𝐁) :⋅ 𝐯 == 𝐀 :⋅ (𝐁 :⋅ 𝐯) for all matrices 𝐀, 𝐁 and every vector 𝐯 in the row space of 𝐁, where the row space of 𝐀 equals the column space of 𝐁.
    • 𝐀 :⋅ 𝐯 == 𝐯 ⋅: 𝐀.T for every matrix 𝐀 and every vector 𝐯 in the row space of 𝐀.

    Axioms for matrix multiplication:

    • if 𝐀 and 𝐁 are matrices and the row space of 𝐀 equals the column space of 𝐁, then the matrix product 𝐀 ⋅ 𝐁 exists.
    • (𝐀 ⋅ 𝐁) ⋅ 𝐂 == 𝐀 ⋅ (𝐁 ⋅ 𝐂) for all matrices 𝐀, 𝐁, 𝐂 where the row space of 𝐀 equals the column space of 𝐁, and the row space of 𝐁 equals the column space of 𝐂.
    • (𝐀 ⋅ 𝐁).T == 𝐁.T ⋅ 𝐀.T for all matrices 𝐀, 𝐁 where the row space of 𝐀 equals the column space of 𝐁.

    Distributive laws:

    • 𝑥 *: (𝐀 + 𝐁) == (𝑥 *: 𝐀) + (𝑥 *: 𝐁) for every scalar 𝑥 and all matrices 𝐀, 𝐁 in this.
    • (𝑥 + 𝑦) *: 𝐀 == (𝑥 *: 𝐀) + (𝑦 *: 𝐀) for all scalars 𝑥, 𝑦 and every matrix 𝐀 in this.
    • 𝐯 ⋅: (𝐀 + 𝐁) == (𝐯 ⋅: 𝐀) + (𝐯 ⋅: 𝐁) for all matrices 𝐀, 𝐁 in the same matrix space, and every vector 𝐯 in the column space of 𝐀 and 𝐁.
    • (𝐀 + 𝐁) :⋅ 𝐯 == (𝐀 :⋅ 𝐯) + (𝐁 :⋅ 𝐯) for all matrices 𝐀, 𝐁 in the same matrix space, and every vector 𝐯 in the row space of 𝐀 and 𝐁.
    • 𝐀 ⋅ (𝐁 + 𝐂) == (𝐀 ⋅ 𝐁) + (𝐀 ⋅ 𝐂) for all matrices 𝐁, 𝐂 in the same matrix space, and every matrix 𝐀 whose row space equals the colum space of 𝐁 and 𝐂.
    • (𝐀 + 𝐁) ⋅ 𝐂 == (𝐀 ⋅ 𝐂) + (𝐁 ⋅ 𝐂) for all matrices 𝐀, 𝐁 in the same matrix space, and every matrix 𝐂 whose column space equals the row space of 𝐀 and 𝐁.

    Version

    0.1

    Since

    0.0

11. trait FN extends VectorSpace

    

    An abstract N-dimensional vector space over a ring.

    An abstract N-dimensional vector space over a ring. Vector addition associates and commutes, and scalar multiplication associates, commutes, and distributes over vector addition and scalar addition. Vector addition and scalar multiplication both have an identity element, and every vector has an additive inverse. Every vector space is an affine space over itself. To the extent practicable, the following axioms should hold.

    Axioms for vector addition:

    • if 𝐮 and 𝐯 are vectors in this, then their sum 𝐮 + 𝐯 is also a vector in this.
    • 𝐮 + 𝐯 == 𝐯 + 𝐮 for all vectors 𝐮, 𝐯 in this.
    • (𝐮 + 𝐯) + 𝐰 == 𝐮 + (𝐯 + 𝐰) for all vectors 𝐮, 𝐯, 𝐰 in this.
    • this has a vector zero such that zero + 𝐯 == 𝐯 for every vector 𝐯 in this.
    • to every vector 𝐯 in this corresponds a vector -𝐯 in this such that 𝐯 + (-𝐯) == zero.

    Axioms for scalar multiplication:

    • if 𝑎 is a scalar in this and 𝐯 is a vector in this, then their product 𝑎 *: 𝐯 is also a vector in this.
    • (𝑎 * 𝑏) *: 𝐯 == 𝑎 *: (𝑏 *: 𝐯) for all scalars 𝑎, 𝑏 and every vector 𝐯 in this.
    • Scalar has an element unit such that unit *: 𝐯 == 𝐯 for every vector 𝐯 in this.

    Distributive laws:

    • 𝑎 *: (𝐮 + 𝐯) == (𝑎 *: 𝐮) + (𝑎 *: 𝐯) for every scalar 𝑎 and all vectors 𝐮, 𝐯 in this.
    • (𝑎 + 𝑏) *: 𝐯 == (𝑎 *: 𝐯) + (𝑏 *: 𝐯) for all scalars 𝑎, 𝑏 and every vector 𝐯 in this.

    Example:

    1. // You can abstract over vector spaces by parameterizing a class or
       // function with a subtype of FN with Singleton. Type elements with
       // the #Vector and #Scalar type projections of your FN type parameter.
       def testVectorSpaceOperations[V <: FN[S] with Singleton, S <: Ring with Singleton]
           (a: V#Scalar, b: V#Scalar, u: V#Vector, v: V#Vector, w: V#Vector): Unit = {
         assert(u + v == v + u, "commutativity of vector addition")
         assert((u + v) + w == u + (v + w), "associativity of vector addition")
         assert((a * b) *: v == a *: (b *: v), "associativity of scalar multiplication with ring multiplication")
         assert(a *: (u + v) == (a *: u) + (a *: v), "distributivity of scalar multiplication over vector addition")
         assert((a + b) *: v == (a *: v) + (b *: v), "distributivity of scalar multiplication over ring addition")
       }
       
       // Alternatively, functions can use path-dependent types of a FN parameter.
       def testVectorSpaceIdentities(V: FN[_])(a: V.Scalar, v: V.Vector): Unit = {
         import V._
         assert(zero + v == v, "existence of additive identity vector")
         assert(v + (-v) == zero, "existence of additive inverse vector")
         assert(Scalar.unit *: v == v, "existence of multiplicative identity scalar")
       }

    Version

    0.1

    Since

    0.0

12. trait Field extends Ring

    

    An abstract field structure.

    An abstract field structure. Addition associates and commutes, and multiplication associates, commutes, and distributes over addition. Addition and multiplication both have an identity element, every element has an additive inverse, and every element except zero has a multiplicative inverse. To the extent practicable, the following axioms should hold.

    Axioms for addition:

    • if 𝑎 and 𝑏 are elements in this, then their sum 𝑎 + 𝑏 is also an element in this.
    • 𝑎 + 𝑏 == 𝑏 + 𝑎 for all elements 𝑎, 𝑏 in this.
    • (𝑎 + 𝑏) + 𝑐 == 𝑎 + (𝑏 + 𝑐) for all elements 𝑎, 𝑏, 𝑐 in this.
    • this has an element zero such that zero + 𝑎 == 𝑎 for every element 𝑎 in this.
    • to every element 𝑎 in this corresponds an element -𝑎 in this such that 𝑎 + (-𝑎) == zero.

    Axioms for multiplication:

    • if 𝑎 and 𝑏 are elements in this, then their product 𝑎 * 𝑏 is also an element in this.
    • 𝑎 * 𝑏 == 𝑏 * 𝑎 for all 𝑎, 𝑏 elements in this.
    • (𝑎 * 𝑏) * 𝑐 == 𝑎 * (𝑏 * 𝑐) for all elements 𝑎, 𝑏, 𝑐 in this.
    • this has an element unit != zero such that unit * 𝑎 == 𝑎 for every element 𝑎 in this.
    • if 𝑎 is in this and 𝑎 != zero then there exists an element 𝑎.inverse such that 𝑎 * 𝑎.inverse == unit.

    The distributive law:

    • 𝑎 * (𝑏 + 𝑐) == (𝑎 * 𝑏) + (𝑎 * 𝑐) for all elements 𝑎, 𝑏, 𝑐 in this.

    Example:

    1. // You can abstract over fields by parameterizing a class or
       // function with a subtype of Field with Singleton. Type elements
       // with the #Element type projection of your Field type parameter.
       def testFieldOperations[F <: Field with Singleton](a: F#Element, b: F#Element, c: F#Element): Unit = {
         assert(a + b == b + a, "commutativity of addition")
         assert((a + b) + c == a + (b + c), "associativity of addition")
         assert(a * b == b * a, "commutativity of multiplication")
         assert((a * b) * c == a * (b * c), "associativity of multiplication")
         assert(a * (b + c) == (a * b) + (a * c), "distributivity of multiplication over addition")
       }
       
       // Alternatively, functions can use path-dependent types of a Field parameter.
       def testFieldIdentities(F: Field)(a: F.Element): Unit = {
         import F._
         assert(zero + a == a, "existence of additive identity")
         assert(a + (-a) == zero, "existence of additive inverse")
         assert(unit != zero && unit * a == a, "existence of multiplicative identity")
         assert(a * a.inverse == unit, "existence of multiplicative inverse")
       }

    Version

    0.1

    Since

    0.0

13. trait IntervalField extends IntervalRing with Field

    

    A field of closed sets between two elements of an ordered field.

    A field of closed sets between two elements of an ordered field.

    Version

    0.1

    Since

    0.1

14. trait IntervalRing extends Ring

    

    A ring of closed sets between two elenents of an ordered ring.

    A ring of closed sets between two elenents of an ordered ring.

    Version

    0.1

    Since

    0.1

15. trait OrderedField extends OrderedRing with Field

    

    A totally ordered abstract field structure.

    A totally ordered abstract field structure. Addition associates and commutes, and multiplication associates, commutes, and distributes over addition. Addition and multiplication both have an identity element, every every element has an additive inverse, and every element except zero has a multiplicative inverse. To the extent practicable, the following axioms should hold.

    Axioms for addition:

    • if 𝑎 and 𝑏 are elements in this, then their sum 𝑎 + 𝑏 is also an element in this.
    • 𝑎 + 𝑏 == 𝑏 + 𝑎 for all elements 𝑎, 𝑏 in this.
    • (𝑎 + 𝑏) + 𝑐 == 𝑎 + (𝑏 + 𝑐) for all elements 𝑎, 𝑏, 𝑐 in this.
    • this has an element zero such that zero + 𝑎 == 𝑎 for every element 𝑎 in this.
    • to every element 𝑎 in this corresponds an element -𝑎 in this such that 𝑎 + (-𝑎) == zero.

    Axioms for multiplication:

    • if 𝑎 and 𝑏 are elements in this, then their product 𝑎 * 𝑏 is also an element in this.
    • 𝑎 * 𝑏 == 𝑏 * 𝑎 for all elements 𝑎, 𝑏 in this.
    • (𝑎 * 𝑏) * 𝑐 == 𝑎 * (𝑏 * 𝑐) for all elements 𝑎, 𝑏, 𝑐 in this.
    • this has an element unit != zero such that unit * 𝑎 == 𝑎 for every element 𝑎 in this.
    • if 𝑎 is in this and 𝑎 != zero then there exists an element 𝑎.inverse such that 𝑎 * 𝑎.inverse == unit.

    The distributive law:

    • 𝑎 * (𝑏 + 𝑐) == (𝑎 * 𝑏) + (𝑎 * 𝑐) for all elements 𝑎, 𝑏, 𝑐 in this.

    Order axioms:

    • if 𝑎 <= 𝑏 and 𝑏 <= 𝑎 then 𝑎 == 𝑏 for all elements 𝑎, 𝑏 in this.
    • if 𝑎 <= 𝑏 and 𝑏 <= 𝑐 then 𝑎 <= 𝑐 for all elements 𝑎, 𝑏, 𝑐 in this.
    • 𝑎 <= 𝑏 or 𝑏 <= 𝑎 for all elements 𝑎, 𝑏 in this.

    Example:

    1. // You can abstract over ordered fields by parameterizing a class or
       // function with a subtype of OrderedField with Singleton. Type elements
       // with the #Element type projection of your OrderedField type parameter.
       def testOrderedFieldOperations[F <: OrderedField with Singleton](a: F#Element, b: F#Element, c: F#Element): Unit = {
         assert(a + b == b + a, "commutativity of addition")
         assert((a + b) + c == a + (b + c), "associativity of addition")
         assert(a * b == b * a, "commutativity of multiplication")
         assert((a * b) * c == a * (b * c), "associativity of multiplication")
         assert(a * (b + c) == (a * b) + (a * c), "distributivity of multiplication over addition")
         if (a <= b) assert((a min b) == a, "existence of minima")
         if (a <= b) assert((a max b) == b, "existence of maxima")
       }
       
       // Alternatively, functions can use path-dependent types of an OrderedField parameter.
       def testOrderedFieldIdentities(F: OrderedField)(a: F.Element, b: F.Element): Unit = {
         import F._
         assert(zero + a == a, "existence of additive identity")
         assert(a + (-a) == zero, "existence of additive inverse")
         assert(unit != zero && unit * a == a, "existence of multiplicative identity")
         assert(a * a.inverse == unit, "existence of multiplicative inverse")
         if (a <= b && b <= a) assert(a == b, "antisymmetry of ordering")
         if (a <= b && b <= c) assert(a <= c, "transitivity of ordering")
         assert(a <= b || b <= a, "totality of ordering")
       }

    Version

    0.1

    Since

    0.0

16. trait OrderedRing extends Ring

    

    A totally ordered abstract ring structure.

    A totally ordered abstract ring structure. Addition associates and commutes, and multiplication associates and distributes over addition. Addition and multiplication both have an identity element, and every element has an additive inverse. To the extent practicable, the following axioms should hold.

    Axioms for addition:

    • if 𝑎 and 𝑏 are elements in this, then their sum 𝑎 + 𝑏 is also an element in this.
    • 𝑎 + 𝑏 == 𝑏 + 𝑎 for all elements 𝑎, 𝑏 in this.
    • (𝑎 + 𝑏) + 𝑐 == 𝑎 + (𝑏 + 𝑐) for all elements 𝑎, 𝑏, 𝑐 in this.
    • this has an element zero such that zero + 𝑎 == 𝑎 for every element 𝑎 in this.
    • to every element 𝑎 in this corresponds an element -𝑎 in this such that 𝑎 + (-𝑎) == zero.

    Axioms for multiplication:

    • if 𝑎 and 𝑏 are elements in this, then their product 𝑎 * 𝑏 is also an element in this.
    • (𝑎 * 𝑏) * 𝑐 == 𝑎 * (𝑏 * 𝑐) for all elements 𝑎, 𝑏, 𝑐 in this.
    • this has an element unit != zero such that unit * 𝑎 == 𝑎 for every element 𝑎 in this.

    The distributive law:

    • 𝑎 * (𝑏 + 𝑐) == (𝑎 * 𝑏) + (𝑎 * 𝑐) for all elements 𝑎, 𝑏, 𝑐 in this.

    Order axioms:

    • if 𝑎 <= 𝑏 and 𝑏 <= 𝑎 then 𝑎 == 𝑏 for all elements 𝑎, 𝑏 in this.
    • if 𝑎 <= 𝑏 and 𝑏 <= 𝑐 then 𝑎 <= 𝑐 for all elements 𝑎, 𝑏, 𝑐 in this.
    • 𝑎 <= 𝑏 or 𝑏 <= 𝑎 for all elements 𝑎, 𝑏 in this.

    Example:

    1. // You can abstract over ordered rings by parameterizing a class or
       // function with a subtype of OrderedRing with Singleton. Type elements
       // with the #Element type projection of your OrderedRing type parameter.
       def testOrderedRingOperations[R <: OrderedRing with Singleton](a: R#Element, b: R#Element, c: R#Element): Unit = {
         assert(a + b == b + a, "commutativity of addition")
         assert((a + b) + c == a + (b + c), "associativity of addition")
         assert((a * b) * c == a * (b * c), "associativity of multiplication")
         assert(a * (b + c) == (a * b) + (a * c), "distributivity of multiplication over addition")
         if (a <= b) assert((a min b) == a, "existence of minima")
         if (a <= b) assert((a max b) == b, "existence of maxima")
       }
       
       // Alternatively, functions can use path-dependent types of an OrderedRing parameter.
       def testOrderedRingIdentities(R: OrderedRing)(a: R.Element, b: R.Element): Unit = {
         import R._
         assert(zero + a == a, "existence of additive identity")
         assert(a + (-a) == zero, "existence of additive inverse")
         assert(unit != zero && unit * a == a, "existence of multiplicative identity")
         if (a <= b && b <= a) assert(a == b, "antisymmetry of ordering")
         if (a <= b && b <= c) assert(a <= c, "transitivity of ordering")
         assert(a <= b || b <= a, "totality of ordering")
       }

    Version

    0.1

    Since

    0.0

17. trait RealField extends OrderedField with CompleteField

    

    A complete, totally ordered abstract field structure.

    A complete, totally ordered abstract field structure. Addition associates and commutes, and multiplication associates, commutes, and distributes over addition. Addition and multiplication both have an identity element, every element has an additive inverse, and every element except zero has a multiplicative inverse. Also, every Cauchy sequence of elements converges. To the extent practicable, the following axioms should hold.

    Axioms for addition:

    • if 𝑎 and 𝑏 are elements in this, then their sum 𝑎 + 𝑏 is also an element in this.
    • 𝑎 + 𝑏 == 𝑏 + 𝑎 for all elements 𝑎, 𝑏 in this.
    • (𝑎 + 𝑏) + 𝑐 == 𝑎 + (𝑏 + 𝑐) for all elements 𝑎, 𝑏, 𝑐 in this.
    • this has an element zero such that zero + 𝑎 == 𝑎 for every element 𝑎 in this.
    • to every element 𝑎 in this corresponds an element -𝑎 in this such that 𝑎 + (-𝑎) == zero.

    Axioms for multiplication:

    • if 𝑎 and 𝑏 are elements in this, then their product 𝑎 * 𝑏 is also an element in this.
    • 𝑎 * 𝑏 == 𝑏 * 𝑎 for all 𝑎, 𝑏 elements in this.
    • (𝑎 * 𝑏) * 𝑐 == 𝑎 * (𝑏 * 𝑐) for all elements 𝑎, 𝑏, 𝑐 in this.
    • this has an element unit != zero such that unit * 𝑎 == 𝑎 for every element 𝑎 in this.
    • if 𝑎 is in this and 𝑎 != zero then there exists an element 𝑎.inverse such that 𝑎 * 𝑎.inverse == unit.

    The distributive law:

    • 𝑎 * (𝑏 + 𝑐) == (𝑎 * 𝑏) + (𝑎 * 𝑐) for all elements 𝑎, 𝑏, 𝑐 in this.

    Order axioms:

    • if 𝑎 <= 𝑏 and 𝑏 <= 𝑎 then 𝑎 == 𝑏 for all elements 𝑎, 𝑏 in this.
    • if 𝑎 <= 𝑏 and 𝑏 <= 𝑐 then 𝑎 <= 𝑐 for all elements 𝑎, 𝑏, 𝑐 in this.
    • 𝑎 <= 𝑏 or 𝑏 <= 𝑎 for all elements 𝑎, 𝑏 in this.

    Completeness axiom:

    • every non-empty subset of this with an upper bound has a least upper bound.

    Example:

    1. // You can abstract over real fields by parameterizing a class or
       // function with a subtype of RealField with Singleton. Type elements
       // with the #Element type projection of your RealField type parameter.
       def testRealFieldOperations[R <: RealField with Singleton](a: R#Element, b: R#Element, c: R#Element): Unit = {
         assert(a + b == b + a, "commutativity of addition")
         assert((a + b) + c == a + (b + c), "associativity of addition")
         assert(a * b == b * a, "commutativity of multiplication")
         assert((a * b) * c == a * (b * c), "associativity of multiplication")
         assert(a * (b + c) == (a * b) + (a * c), "distributivity of multiplication over addition")
         if (a <= b) assert((a min b) == a, "existence of minima")
         if (a <= b) assert((a max b) == b, "existence of maxima")
       }
       
       // Alternatively, functions can use path-dependent types of a RealField parameter.
       def testRealFieldIdentities(R: RealField)(a: R.Element, b: R.Element): Unit = {
         import R._
         assert(zero + a == a, "existence of additive identity")
         assert(a + (-a) == zero, "existence of additive inverse")
         assert(unit != zero && unit * a == a, "existence of multiplicative identity")
         assert(a * a.inverse == unit, "existence of multiplicative inverse")
         if (a <= b && b <= a) assert(a == b, "antisymmetry of ordering")
         if (a <= b && b <= c) assert(a <= c, "transitivity of ordering")
         assert(a <= b || b <= a, "totality of ordering")
       }

    Version

    0.1

    Since

    0.0

18. trait Ring extends AnyRef

    

    An abstract ring structure.

    An abstract ring structure. Addition associates and commutes, and multiplication associates and distributes over addition. Addition and multiplication both have an identity element, and every element has an additive inverse. To the extent practicable, the following axioms should hold.

    Axioms for addition:

    • if 𝑎 and 𝑏 are elements in this, then their sum 𝑎 + 𝑏 is also an element in this.
    • 𝑎 + 𝑏 == 𝑏 + 𝑎 for all elements 𝑎, 𝑏 in this.
    • (𝑎 + 𝑏) + 𝑐 == 𝑎 + (𝑏 + 𝑐) for all elements 𝑎, 𝑏, 𝑐 in this.
    • this has an element zero such that zero + 𝑎 == 𝑎 for every element 𝑎 in this.
    • to every element 𝑎 in this corresponds an element -𝑎 in this such that 𝑎 + (-𝑎) == zero.

    Axioms for multiplication:

    • if 𝑎 and 𝑏 are elements in this, then their product 𝑎 * 𝑏 is also an element in this.
    • (𝑎 * 𝑏) * 𝑐 == 𝑎 * (𝑏 * 𝑐) for all elements 𝑎, 𝑏, 𝑐 in this.
    • this has an element unit != zero such that unit * 𝑎 == 𝑎 for every element 𝑎 in this.

    The distributive law:

    • 𝑎 * (𝑏 + 𝑐) == (𝑎 * 𝑏) + (𝑎 * 𝑐) for all elements 𝑎, 𝑏, 𝑐 in this.

    Example:

    1. // You can abstract over rings by parameterizing a class or
       // function with a subtype of Ring with Singleton. Type elements
       // with the #Element type projection of your Ring type parameter.
       def testRingOperations[R <: Ring with Singleton](a: R#Element, b: R#Element, c: R#Element): Unit = {
         assert(a + b == b + a, "commutativity of addition")
         assert((a + b) + c == a + (b + c), "associativity of addition")
         assert((a * b) * c == a * (b * c), "associativity of multiplication")
         assert(a * (b + c) == (a * b) + (a * c), "distributivity of multiplication over addition")
       }
       
       // Alternatively, functions can use path-dependent types of a Ring parameter.
       def testRingIdentities(R: Ring)(a: R.Element): Unit = {
         import R._
         assert(zero + a == a, "existence of additive identity")
         assert(a + (-a) == zero, "existence of additive inverse")
         assert(unit != zero && unit * a == a, "existence of multiplicative identity")
       }

    Version

    0.1

    Since

    0.0

19. trait VectorSpace extends AnyRef

    

    An abstract vector space over a ring.

    An abstract vector space over a ring. Vector addition associates and commutes, and scalar multiplication associates and distributes over vector addition and scalar addition. Vector addition and scalar multiplication both have an identity element, and every vector has an additive inverse. To the extent practicable, the following axioms should hold.

    Axioms for vector addition:

    • if 𝐮 and 𝐯 are vectors in this, then their sum 𝐮 + 𝐯 is also a vector in this.
    • 𝐮 + 𝐯 == 𝐯 + 𝐮 for all vectors 𝐮, 𝐯 in this.
    • (𝐮 + 𝐯) + 𝐰 == 𝐮 + (𝐯 + 𝐰) for all vectors 𝐮, 𝐯, 𝐰 in this.
    • this has a vector zero such that zero + 𝐯 == 𝐯 for every vector 𝐯 in this.
    • to every vector 𝐯 in this corresponds a vector -𝐯 in this such that 𝐯 + (-𝐯) == zero.

    Axioms for scalar multiplication:

    • if 𝑎 is a scalar in this and 𝐯 is a vector in this, then their product 𝑎 *: 𝐯 is also a vector in this.
    • (𝑎 * 𝑏) *: 𝐯 == 𝑎 *: (𝑏 *: 𝐯) for all scalars 𝑎, 𝑏 and every vector 𝐯 in this.
    • Scalar has an element unit such that unit *: 𝐯 == 𝐯 for every vector 𝐯 in this.

    Distributive laws:

    • 𝑎 *: (𝐮 + 𝐯) == (𝑎 *: 𝐮) + (𝑎 *: 𝐯) for every scalar 𝑎 and all vectors 𝐮, 𝐯 in this.
    • (𝑎 + 𝑏) *: 𝐯 == (𝑎 *: 𝐯) + (𝑏 *: 𝐯) for all scalars 𝑎, 𝑏 and every vector 𝐯 in this.

    Example:

    1. // You can abstract over vector spaces by parameterizing a class or
       // function with a subtype of VectorSpace with Singleton. Type elements
       // with the #Vector and #Scalar type projections of your VectorSpace
       // type parameter.
       def testVectorSpaceOperations[V <: VectorSpace with Singleton]
           (a: V#Scalar, b: V#Scalar, u: V#Vector, v: V#Vector, w: V#Vector) {
         assert(u + v == v + u, "commutativity of vector addition")
         assert((u + v) + w == u + (v + w), "associativity of vector addition")
         assert((a * b) *: v == a *: (b *: v), "associativity of scalar multiplication with ring multiplication")
         assert(a *: (u + v) == (a *: u) + (a *: v), "distributivity of scalar multiplication over vector addition")
         assert((a + b) *: v == (a *: v) + (b *: v), "distributivity of scalar multiplication over ring addition")
       }
       
       // Alternatively, functions can use path-dependent types of a VectorSpace parameter.
       def testVectorSpaceIdentities(V: VectorSpace)(a: V.Scalar, v: V.Vector): Unit = {
         import V._
         assert(zero + v == v, "existence of additive identity vector")
         assert(v + (-v) == zero, "existence of additive inverse vector")
         assert(Scalar.unit *: v == v, "existence of multiplicative identity scalar")
       }

    Version

    0.1

    Since

    0.0