OpenMath Content Dictionary: linalg7

Canonical URL:

http://www.openmath.org/cd/linalg7.ocd

CD File:

linalg7.ocd

CD as XML Encoded OpenMath:

linalg7.omcd

Defines:

constant, sparse, zero

Date:

2003-03-22

Version:

1

Review Date:

2005-00-00

Status:

experimental

Uses CD:

alg1, arith1, interval1, linalg1, linalg4, list1, logic1, mathmltypes, quant1, relation1, set1

A CD of structured vectors

zero

Description:

The zero symbol represents the zero vector, it takes one parameter which should be the length (dimension in some terminology) of the vector.

Commented Mathematical property (CMP):

If M is an n*m matrix and V is a zero vector of length m then V*M = V2 where V2 is a zero vector of length n

Formal Mathematical property (FMP):

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
<OMBIND>
  <OMS cd="quant1" name="forall"/>
  <OMBVAR>
    <OMATTR>
      <OMATP>
        <OMS cd="mathmltypes" name="type"/>
        <OMS cd="mathmltypes" name="matrix_type"/>
      </OMATP>
      <OMV name="M"/>
    </OMATTR>
  </OMBVAR>
  <OMA>
    <OMS cd="logic1" name="implies"/>
    <OMA>
      <OMS cd="logic1" name="and"/>
      <OMA>
        <OMS cd="relation1" name="eq"/>
        <OMA>
          <OMS cd="linalg4" name="columncount"/>
          <OMV name="M"/>
        </OMA>
        <OMV name="m"/>
      </OMA>
      <OMA>
        <OMS cd="relation1" name="eq"/>
        <OMA>
          <OMS cd="linalg4" name="rowcount"/>
          <OMV name="M"/>
        </OMA>
        <OMV name="n"/>
      </OMA>
    </OMA>
    <OMA><OMS cd="relation1" name="eq"/>
      <OMA>
        <OMS cd="arith1" name="times"/>
        <OMA>
          <OMS cd="linalg7" name="zero"/>
          <OMV name="m"/>
        </OMA>
        <OMV name="M"/>
      </OMA>
      <OMA>
        <OMS cd="linalg7" name="zero"/>
        <OMV name="n"/>
      </OMA>
    </OMA>
  </OMA>
</OMBIND>
</OMOBJ>

forall [ Attrib([ type matrix_type ], M) ] . (implies (and (eq (columncount ( M) , m) , eq (rowcount ( M) , n) ) , eq (times (zero ( m) , M) , zero ( n) ) ) )

$$\forall \hspace{0.17em}M.\mathrm{columncount}\left(M\right)=m\wedge \mathrm{rowcount}\left(M\right)=n\Rightarrow \mathrm{zero}\left(m\right)M=\mathrm{zero}\left(n\right)$$

Commented Mathematical property (CMP):

If M is an n*m matrix and V is a zero vector of length n then M*V = V2 where V2 is a zero vector of length m

Formal Mathematical property (FMP):

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
<OMBIND>
  <OMS cd="quant1" name="forall"/>
  <OMBVAR>
    <OMATTR>
      <OMATP>
        <OMS cd="mathmltypes" name="type"/>
        <OMS cd="mathmltypes" name="matrix_type"/>
      </OMATP>
      <OMV name="M"/>
    </OMATTR>
  </OMBVAR>
  <OMA>
    <OMS cd="logic1" name="implies"/>
    <OMA>
      <OMS cd="logic1" name="and"/>
      <OMA>
        <OMS cd="relation1" name="eq"/>
        <OMA>
          <OMS cd="linalg4" name="columncount"/>
          <OMV name="M"/>
        </OMA>
        <OMV name="m"/>
      </OMA>
      <OMA>
        <OMS cd="relation1" name="eq"/>
        <OMA>
          <OMS cd="linalg4" name="rowcount"/>
          <OMV name="M"/>
        </OMA>
        <OMV name="n"/>
      </OMA>
    </OMA>
    <OMA><OMS cd="relation1" name="eq"/>
      <OMA>
        <OMS cd="arith1" name="times"/>
        <OMV name="M"/>
        <OMA>
          <OMS cd="linalg7" name="zero"/>
          <OMV name="n"/>
        </OMA>
      </OMA>
      <OMA>
        <OMS cd="linalg7" name="zero"/>
        <OMV name="m"/>
      </OMA>
    </OMA>
  </OMA>
</OMBIND>
</OMOBJ>

forall [ Attrib([ type matrix_type ], M) ] . (implies (and (eq (columncount ( M) , m) , eq (rowcount ( M) , n) ) , eq (times ( M, zero ( n) ) , zero ( m) ) ) )

$$\forall \hspace{0.17em}M.\mathrm{columncount}\left(M\right)=m\wedge \mathrm{rowcount}\left(M\right)=n\Rightarrow M\mathrm{zero}\left(n\right)=\mathrm{zero}\left(m\right)$$

Commented Mathematical property (CMP):

If V is a zero vector of length n and V2 is a vector of length n then V+V2 = V2+V = V2

Formal Mathematical property (FMP):

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
<OMBIND>
  <OMS cd="quant1" name="forall"/>
  <OMBVAR>
    <OMATTR>
      <OMATP>
        <OMS cd="mathmltypes" name="type"/>
        <OMS cd="mathmltypes" name="vector_type"/>
      </OMATP>
      <OMV name="V2"/>
    </OMATTR>
  </OMBVAR>
  <OMA>
    <OMS cd="logic1" name="implies"/>
    <OMA>
      <OMS cd="relation1" name="eq"/>
      <OMA>
        <OMS cd="linalg4" name="size"/>
        <OMV name="V2"/>
      </OMA>
      <OMV name="n"/>
    </OMA>
    <OMA>
      <OMS cd="logic1" name="and"/>
      <OMA>
        <OMS cd="relation1" name="eq"/>
        <OMV name="V2"/>
        <OMA>
          <OMS cd="arith1" name="plus"/>
          <OMA>
            <OMS cd="linalg7" name="zero"/>
            <OMV name="n"/>
          </OMA>
          <OMV name="V2"/>
        </OMA>
      </OMA>
      <OMA>
        <OMS cd="relation1" name="eq"/>
        <OMV name="V2"/>
        <OMA>
          <OMS cd="arith1" name="plus"/>
          <OMV name="V2"/>
          <OMA>
            <OMS cd="linalg7" name="zero"/>
            <OMV name="n"/>
          </OMA>
        </OMA>
      </OMA>
    </OMA>
  </OMA>
</OMBIND>
</OMOBJ>

forall [ Attrib([ type vector_type ], V2) ] . (implies (eq (size ( V2) , n) , and (eq ( V2, plus (zero ( n) , V2) ) , eq ( V2, plus ( V2, zero ( n) ) ) ) ) )

$$\forall \hspace{0.17em}{V}_2.\mathrm{size}\left(V_2\right)=n\Rightarrow V_2=\mathrm{zero}\left(n\right)+V_2\wedge V_2=V_2+\mathrm{zero}\left(n\right)$$

Commented Mathematical property (CMP):

If V is a zero vector of length n and i is in the integral interval [1,n] then V.i = 0

Formal Mathematical property (FMP):

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
<OMA><OMS cd="logic1" name="implies"/>
  <OMA>
    <OMS cd="set1" name="in"/>
    <OMV name="i"/>
    <OMA>
      <OMS cd="interval1" name="integer_interval"/>
      <OMS cd="alg1" name="one"/>
      <OMV name="n"/>
    </OMA>
  </OMA>
  <OMA>
    <OMS cd="relation1" name="eq"/>
    <OMA>
      <OMS cd="linalg1" name="vector_selector"/>
      <OMV name="i"/>
      <OMA>
        <OMS cd="linalg7" name="zero"/>
        <OMV name="n"/>
      </OMA>
    </OMA>
    <OMS cd="alg1" name="zero"/>
  </OMA>
</OMA>
</OMOBJ>

implies (in ( i, integer_interval (one, n) ) , eq (vector_selector ( i, zero ( n) ) , zero) )

$$i\in [1,n]\Rightarrow {\mathrm{zero}\left(n\right)}_i=0$$

Signatures:

sts

constant

Description:

The constant symbol represents the constant vector. It takes two parameters, the length (dimension) of the vector and the constant value, which all the elements are equal to.

Commented Mathematical property (CMP):

If V is a constant vector of length n, with constant value c and i is in the integral interval [1,n] then V.i = c

Formal Mathematical property (FMP):

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
<OMA><OMS cd="logic1" name="implies"/>
  <OMA>
    <OMS cd="set1" name="in"/>
    <OMV name="i"/>
    <OMA>
      <OMS cd="interval1" name="integer_interval"/>
      <OMS cd="alg1" name="one"/>
      <OMV name="n"/>
    </OMA>
  </OMA>
  <OMA>
    <OMS cd="relation1" name="eq"/>
    <OMA>
      <OMS cd="linalg1" name="vector_selector"/>
      <OMV name="i"/>
      <OMA>
        <OMS cd="linalg7" name="constant"/>
        <OMV name="n"/>
        <OMV name="c"/>
      </OMA>
    </OMA>
    <OMV name="c"/>
  </OMA>
</OMA>
</OMOBJ>

implies (in ( i, integer_interval (one, n) ) , eq (vector_selector ( i, constant ( n, c) ) , c) )

$$i\in [1,n]\Rightarrow {\mathrm{constant}(n,c)}_i=c$$

Signatures:

sts

sparse

Description:

The sparse symbol is a constructor for sparse vectors, it is (n+1)-ary, where the first parameter is the length (dimension) of the vector, and every following parameter specifies a possibly non-zero element in the following way. The parameter is a list which should have length two. The first element in the list is the position (one based), whilst the second element in the list is the value. Every other element of the vector is implicitly zero.

Example:

This example shows a representation of the sparse matrix $$\left (\begin{array}[c]1\\0\\0\\0\\0\end{array}\right$$

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
    <OMA>
      <OMS cd="linalg7" name="sparse"/>
      <OMA><OMS cd="list1" name="list"/>
        <OMI>5</OMI>
        <OMI>1</OMI>
      </OMA>
    </OMA>
  </OMOBJ>

sparse (list (5, 1) )

$$\mathrm{sparse}\left((5,1)\right)$$

Signatures:

sts