OpenMath Content Dictionary: linalg4vec

Canonical URL:

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

CD File:

linalg4vec.ocd

CD as XML Encoded OpenMath:

linalg4vec.omcd

Defines:

constant, sparse, zero

Date:

2004-11-22

Version:

2 (Revision 1)

Review Date:

2005-01-01

Status:

experimental

---

A CD for the quick construction of some vectors.

November 2004: A.M. Cohen built this CD from a former experimental CD called linalg7 (version 1, revision 0). The descriptions have been edited and the example in the definition of the symbol sparse has been improved.

---

zero

Role:

application

Description:

This symbol represents a function with one argument, which should be a natural number n. When applied to n, it represents the zero vector of size n (in the terminology of linalg3; dimension n in some terminology).

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):

OpenMath XML (source)

<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="linalg3" name="columncount"/>
          <OMV name="M"/>
        </OMA>
        <OMV name="m"/>
      </OMA>
      <OMA>
        <OMS cd="relation1" name="eq"/>
        <OMA>
          <OMS cd="linalg3" 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="linalg4vec" name="zero"/>
          <OMV name="m"/>
        </OMA>
        <OMV name="M"/>
      </OMA>
      <OMA>
        <OMS cd="linalg4vec" name="zero"/>
        <OMV name="n"/>
      </OMA>
    </OMA>
  </OMA>
</OMBIND>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <bind><csymbol cd="quant1">forall</csymbol>
  <bvar>
   <semantics>
    <ci>M</ci>
    <annotation-xml cd="mathmltypes" name="type"><csymbol cd="mathmltypes">matrix_type</csymbol></annotation-xml>
   </semantics>
  </bvar>
  <apply><csymbol cd="logic1">implies</csymbol>
   <apply><csymbol cd="logic1">and</csymbol>
    <apply><csymbol cd="relation1">eq</csymbol>
     <apply><csymbol cd="linalg3">columncount</csymbol><ci>M</ci></apply>
     <ci>m</ci>
    </apply>
    <apply><csymbol cd="relation1">eq</csymbol>
     <apply><csymbol cd="linalg3">rowcount</csymbol><ci>M</ci></apply>
     <ci>n</ci>
    </apply>
   </apply>
   <apply><csymbol cd="relation1">eq</csymbol>
    <apply><csymbol cd="arith1">times</csymbol>
     <apply><csymbol cd="linalg4vec">zero</csymbol><ci>m</ci></apply>
     <ci>M</ci>
    </apply>
    <apply><csymbol cd="linalg4vec">zero</csymbol><ci>n</ci></apply>
   </apply>
  </apply>
 </bind>
</math>

Prefix

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

Popcorn

quant1.forall[$M{mathmltypes.type -> mathmltypes.matrix_type} -> linalg3.columncount($M) = $m and linalg3.rowcount($M) = $n ==> linalg4vec.zero($m) * $M = linalg4vec.zero($n)]

Rendered Presentation MathML

$$\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):

OpenMath XML (source)

<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="linalg3" name="columncount"/>
          <OMV name="M"/>
        </OMA>
        <OMV name="m"/>
      </OMA>
      <OMA>
        <OMS cd="relation1" name="eq"/>
        <OMA>
          <OMS cd="linalg3" 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="linalg4vec" name="zero"/>
          <OMV name="n"/>
        </OMA>
      </OMA>
      <OMA>
        <OMS cd="linalg4vec" name="zero"/>
        <OMV name="m"/>
      </OMA>
    </OMA>
  </OMA>
</OMBIND>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <bind><csymbol cd="quant1">forall</csymbol>
  <bvar>
   <semantics>
    <ci>M</ci>
    <annotation-xml cd="mathmltypes" name="type"><csymbol cd="mathmltypes">matrix_type</csymbol></annotation-xml>
   </semantics>
  </bvar>
  <apply><csymbol cd="logic1">implies</csymbol>
   <apply><csymbol cd="logic1">and</csymbol>
    <apply><csymbol cd="relation1">eq</csymbol>
     <apply><csymbol cd="linalg3">columncount</csymbol><ci>M</ci></apply>
     <ci>m</ci>
    </apply>
    <apply><csymbol cd="relation1">eq</csymbol>
     <apply><csymbol cd="linalg3">rowcount</csymbol><ci>M</ci></apply>
     <ci>n</ci>
    </apply>
   </apply>
   <apply><csymbol cd="relation1">eq</csymbol>
    <apply><csymbol cd="arith1">times</csymbol>
     <ci>M</ci>
     <apply><csymbol cd="linalg4vec">zero</csymbol><ci>n</ci></apply>
    </apply>
    <apply><csymbol cd="linalg4vec">zero</csymbol><ci>m</ci></apply>
   </apply>
  </apply>
 </bind>
</math>

Prefix

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

Popcorn

quant1.forall[$M{mathmltypes.type -> mathmltypes.matrix_type} -> linalg3.columncount($M) = $m and linalg3.rowcount($M) = $n ==> $M * linalg4vec.zero($n) = linalg4vec.zero($m)]

Rendered Presentation MathML

$$\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):

OpenMath XML (source)

<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="linalg4vec" 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="linalg4vec" name="zero"/>
            <OMV name="n"/>
          </OMA>
        </OMA>
      </OMA>
    </OMA>
  </OMA>
</OMBIND>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <bind><csymbol cd="quant1">forall</csymbol>
  <bvar>
   <semantics>
    <ci>V2</ci>
    <annotation-xml cd="mathmltypes" name="type"><csymbol cd="mathmltypes">vector_type</csymbol></annotation-xml>
   </semantics>
  </bvar>
  <apply><csymbol cd="logic1">implies</csymbol>
   <apply><csymbol cd="relation1">eq</csymbol>
    <apply><csymbol cd="linalg4">size</csymbol><ci>V2</ci></apply>
    <ci>n</ci>
   </apply>
   <apply><csymbol cd="logic1">and</csymbol>
    <apply><csymbol cd="relation1">eq</csymbol>
     <ci>V2</ci>
     <apply><csymbol cd="arith1">plus</csymbol>
      <apply><csymbol cd="linalg4vec">zero</csymbol><ci>n</ci></apply>
      <ci>V2</ci>
     </apply>
    </apply>
    <apply><csymbol cd="relation1">eq</csymbol>
     <ci>V2</ci>
     <apply><csymbol cd="arith1">plus</csymbol>
      <ci>V2</ci>
      <apply><csymbol cd="linalg4vec">zero</csymbol><ci>n</ci></apply>
     </apply>
    </apply>
   </apply>
  </apply>
 </bind>
</math>

Prefix

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

Popcorn

quant1.forall[$V2{mathmltypes.type -> mathmltypes.vector_type} -> linalg4.size($V2) = $n ==> $V2 = linalg4vec.zero($n) + $V2 and $V2 = $V2 + linalg4vec.zero($n)]

Rendered Presentation MathML

$$\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):

OpenMath XML (source)

<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="linalg4vec" name="zero"/>
        <OMV name="n"/>
      </OMA>
    </OMA>
    <OMS cd="alg1" name="zero"/>
  </OMA>
</OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="logic1">implies</csymbol>
  <apply><csymbol cd="set1">in</csymbol>
   <ci>i</ci>
   <apply><csymbol cd="interval1">integer_interval</csymbol><csymbol cd="alg1">one</csymbol><ci>n</ci></apply>
  </apply>
  <apply><csymbol cd="relation1">eq</csymbol>
   <apply><csymbol cd="linalg1">vector_selector</csymbol>
    <ci>i</ci>
    <apply><csymbol cd="linalg4vec">zero</csymbol><ci>n</ci></apply>
   </apply>
   <csymbol cd="alg1">zero</csymbol>
  </apply>
 </apply>
</math>

Prefix

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

Popcorn

set1.in($i, interval1.integer_interval(alg1.one, $n)) ==> linalg1.vector_selector($i, linalg4vec.zero($n)) = alg1.zero

Rendered Presentation MathML

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

Signatures:

sts

---

[Next: constant] [Last: sparse] [Top]

---

constant

Description:

This symbol represents a binary function whose first argument should be a natural number. When applied to n and c, it represents the constant (row) vector (so vector as defined in linalg2), so size (dimension) n all of whose components have the value c.

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):

OpenMath XML (source)

<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="linalg4vec" name="constant"/>
                 <OMV name="n"/><OMV name="c"/>
            </OMA>
       </OMA>
       <OMV name="c"/>
  </OMA>
</OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="logic1">implies</csymbol>
  <apply><csymbol cd="set1">in</csymbol>
   <ci>i</ci>
   <apply><csymbol cd="interval1">integer_interval</csymbol><csymbol cd="alg1">one</csymbol><ci>n</ci></apply>
  </apply>
  <apply><csymbol cd="relation1">eq</csymbol>
   <apply><csymbol cd="linalg1">vector_selector</csymbol>
    <ci>i</ci>
    <apply><csymbol cd="linalg4vec">constant</csymbol><ci>n</ci><ci>c</ci></apply>
   </apply>
   <ci>c</ci>
  </apply>
 </apply>
</math>

Prefix

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

Popcorn

set1.in($i, interval1.integer_interval(alg1.one, $n)) ==> linalg1.vector_selector($i, linalg4vec.constant($n, $c)) = $c

Rendered Presentation MathML

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

Signatures:

sts

---

[Next: sparse] [Previous: zero] [Top]

---

sparse

Role:

application

Description:

The sparse symbol is a constructor for sparse vectors. It is (n+1)-ary, where the first argument is the length (dimension) of the vector, and every following argument specifies a possibly non-zero element in the following way. The argument 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 vector $$[0,0,0,0,1]$$

OpenMath XML (source)

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

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="linalg4vec">sparse</csymbol>
  <cn type="integer">5</cn>
  <apply><csymbol cd="list1">list</csymbol>
   <cn type="integer">5</cn>
   <cn type="integer">1</cn>
  </apply>
 </apply>
</math>

Prefix

sparse (5, list (5, 1) )

Popcorn

linalg4vec.sparse(5, [5 , 1])

Rendered Presentation MathML

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

Signatures:

sts

---

[First: zero] [Previous: constant] [Top]