OpenMath Content Dictionary: list4

Canonical URL:

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

CD Base:

http://www.openmath.org/cd

CD File:

list4.ocd

CD as XML Encoded OpenMath:

list4.omcd

Defines:

difference, entry, list_of_lengthn, remove, reverse

Date:

2004-11-30

Version:

5 (Revision 1)

Review Date:

2006-03-30

Status:

experimental

---

Several convenient but not basic list functions are given in this CD.

Arjeh M. Cohen  2004-11-30

---

entry

Description:

This symbol represents a binary function whose first argument should be a list L and whose second argument should be a positive integer i such that the absolute value of i is in the interval [1..n], where n is the length of L. If i is positive, it returns the i-th entry L[i] of L, if i is negative it returns the (n+1-i)-th entry of L.

Commented Mathematical property (CMP):

If i is a positive integer and a is a list of length at least i, then entry(a,i) is equal to list_selector(i,a).

Formal Mathematical property (FMP):

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
  <OMA><OMS cd="logic1" name="implies"/>
       <OMA><OMS cd="relation1" name="gt"/>
            <OMV name="i"/> <OMI>0</OMI>
       </OMA>
       <OMA><OMS cd="relation1" name="eq"/>
            <OMA><OMS cd="list4" name="entry"/>
                 <OMV name="a"/> <OMV name="i"/>
            </OMA>
            <OMA><OMS cd="list3" name="list_selector"/>
                  <OMV name="i"/><OMV name="a"/>
            </OMA>
       </OMA>
  </OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="logic1">implies</csymbol>
  <apply><csymbol cd="relation1">gt</csymbol><ci>i</ci><cn type="integer">0</cn></apply>
  <apply><csymbol cd="relation1">eq</csymbol>
   <apply><csymbol cd="list4">entry</csymbol><ci>a</ci><ci>i</ci></apply>
   <apply><csymbol cd="list3">list_selector</csymbol><ci>i</ci><ci>a</ci></apply>
  </apply>
 </apply>
</math>

Prefix

implies (gt ( i, 0) , eq (entry ( a, i) , list_selector ( i, a) ) )

Popcorn

$i > 0 ==> list4.entry($a, $i) = list3.list_selector($i, $a)

Rendered Presentation MathML

$$i>0\Rightarrow \mathrm{entry}(a,i)=\mathrm{list\_selector}(i,a)$$

Example:

The second entry of the list [1,2,3] is 2.

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
  <OMA><OMS cd="relation1" name="eq"/>
       <OMA><OMS cd="list4" name="entry"/>
            <OMA><OMS cd="list1" name="list"/>
                 <OMI> 1 </OMI>
                 <OMI> 2 </OMI>
                 <OMI> 3 </OMI>
            </OMA>
            <OMI> 2 </OMI>
       </OMA>
       <OMI> 2 </OMI>
  </OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="relation1">eq</csymbol>
  <apply><csymbol cd="list4">entry</csymbol>
   <apply><csymbol cd="list1">list</csymbol>
    <cn type="integer">1</cn>
    <cn type="integer">2</cn>
    <cn type="integer">3</cn>
   </apply>
   <cn type="integer">2</cn>
  </apply>
  <cn type="integer">2</cn>
 </apply>
</math>

Prefix

eq (entry (list ( 1 , 2 , 3 ) , 2 ) , 2 )

Popcorn

list4.entry([1 , 2 , 3], 2) = 2

Rendered Presentation MathML

$$\mathrm{entry}((1,2,3),2)=2$$

Example:

Specification of the second element of the list [1,..,6] counted from the end.

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
  <OMA><OMS cd="relation1" name="eq"/>
       <OMA><OMS cd="list4" name="entry"/>
            <OMA><OMS cd="list1" name="list"/>
                 <OMI> 1 </OMI>      <OMI> 2 </OMI>      <OMI> 3 </OMI>
                 <OMI> 4 </OMI>      <OMI> 5 </OMI>      <OMI> 6 </OMI>
            </OMA>
            <OMI>-2</OMI> 
       </OMA>
       <OMI>5</OMI> 
  </OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="relation1">eq</csymbol>
  <apply><csymbol cd="list4">entry</csymbol>
   <apply><csymbol cd="list1">list</csymbol>
    <cn type="integer">1</cn>
    <cn type="integer">2</cn>
    <cn type="integer">3</cn>
    <cn type="integer">4</cn>
    <cn type="integer">5</cn>
    <cn type="integer">6</cn>
   </apply>
   <cn type="integer">-2</cn>
  </apply>
  <cn type="integer">5</cn>
 </apply>
</math>

Prefix

eq (entry (list ( 1 , 2 , 3 , 4 , 5 , 6 ) , -2) , 5)

Popcorn

list4.entry([1 , 2 , 3 , 4 , 5 , 6], -2) = 5

Rendered Presentation MathML

$$\mathrm{entry}((1,2,3,4,5,6),-2)=5$$

Signatures:

sts

---

[Next: reverse] [Last: list_of_lengthn] [Top]

---

reverse

Role:

application

Description:

The reverse of a list

Formal Mathematical property (FMP):

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0" cdbase="http://www.openmath.org/cd">
  <OMA>
    <OMS cd="relation1" name="eq"/>
    <OMA>
      <OMS cd="list4" name="reverse"/>
      <OMS cd="list2" name="nil"/>
    </OMA>
    <OMS cd="list2" name="nil"/>
  </OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="relation1">eq</csymbol>
  <apply><csymbol cd="list4">reverse</csymbol><csymbol cd="list2">nil</csymbol></apply>
  <csymbol cd="list2">nil</csymbol>
 </apply>
</math>

Prefix

eq (reverse (nil) , nil)

Popcorn

list4.reverse(list2.nil) = list2.nil

Rendered Presentation MathML

$$\mathrm{reverse}\left(\mathrm{nil}\right)=\mathrm{nil}$$

Formal Mathematical property (FMP):

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0" cdbase="http://www.openmath.org/cd">
  <OMBIND>
    <OMS cd="quant1" name="forall"/>
    <OMBVAR>
      <OMV name="lst"/>
      <OMV name="a"/>
    </OMBVAR>
    <OMA>
      <OMS cd="relation1" name="eq"/>
      <OMA><OMS cd="list4" name="reverse"/>
        <OMA><OMS cd="list2" name="cons"/>
             <OMV name="a"/>   <OMV name="lst"/>
        </OMA>
      </OMA>
      <OMA><OMS cd="list3" name="append"/>
           <OMA><OMS cd="list4" name="reverse"/>
          <OMV name="lst"/>
        </OMA>
        <OMA><OMS cd="list2" name="cons"/>
             <OMV name="a"/>
             <OMS cd="list2" name="nil"/>
        </OMA>
      </OMA>
    </OMA>
  </OMBIND>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <bind><csymbol cd="quant1">forall</csymbol>
  <bvar><ci>lst</ci></bvar>
  <bvar><ci>a</ci></bvar>
  <apply><csymbol cd="relation1">eq</csymbol>
   <apply><csymbol cd="list4">reverse</csymbol>
    <apply><csymbol cd="list2">cons</csymbol><ci>a</ci><ci>lst</ci></apply>
   </apply>
   <apply><csymbol cd="list3">append</csymbol>
    <apply><csymbol cd="list4">reverse</csymbol><ci>lst</ci></apply>
    <apply><csymbol cd="list2">cons</csymbol><ci>a</ci><csymbol cd="list2">nil</csymbol></apply>
   </apply>
  </apply>
 </bind>
</math>

Prefix

forall [ lst a ] . (eq (reverse (cons ( a, lst) ) , append (reverse ( lst) , cons ( a, nil) ) ) )

Popcorn

quant1.forall[$lst, $a -> list4.reverse(list2.cons($a, $lst)) = list3.append(list4.reverse($lst), list2.cons($a, list2.nil))]

Rendered Presentation MathML

$$\forall \hspace{0.17em}\mathrm{lst},a.\mathrm{reverse}\left(\mathrm{cons}(a,\mathrm{lst})\right)=\mathrm{append}(\mathrm{reverse}\left(\mathrm{lst}\right),\mathrm{cons}(a,\mathrm{nil}))$$

Signatures:

sts

---

[Next: difference] [Previous: entry] [Top]

---

difference

Description:

This symbol represents a function with two arguments, both lists. When applied to two lists, it represents a list made up of all the elements of the first list which do not occur in the second, appearing in the order in which they occur in the first list.

Example:

Specification of the list [6,6,12], apart from the first 2 elements.

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
  <OMA><OMS cd="relation1" name="eq"/>
       <OMA><OMS cd="list4" name="difference"/>
            <OMA><OMS cd="list1" name="list"/>
                 <OMI> 6 </OMI>      <OMI> 6 </OMI>      <OMI> 12 </OMI>
            </OMA>
            <OMA><OMS cd="list1" name="list"/>
                 <OMI> 6 </OMI>
            </OMA>
       </OMA>
       <OMA><OMS cd="list1" name="list"/>
            <OMI> 12 </OMI>
       </OMA>
  </OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="relation1">eq</csymbol>
  <apply><csymbol cd="list4">difference</csymbol>
   <apply><csymbol cd="list1">list</csymbol>
    <cn type="integer">6</cn>
    <cn type="integer">6</cn>
    <cn type="integer">12</cn>
   </apply>
   <apply><csymbol cd="list1">list</csymbol><cn type="integer">6</cn></apply>
  </apply>
  <apply><csymbol cd="list1">list</csymbol><cn type="integer">12</cn></apply>
 </apply>
</math>

Prefix

eq (difference (list ( 6 , 6 , 12 ) , list ( 6 ) ) , list ( 12 ) )

Popcorn

list4.difference([6 , 6 , 12], [6]) = [12]

Rendered Presentation MathML

$$\mathrm{difference}((6,6,12),\left(6\right))=\left(12\right)$$

Signatures:

sts

---

[Next: remove] [Previous: reverse] [Top]

---

remove

Description:

This symbol represents a function with two arguments, both lists. When applied to two lists, it represents a list made up of all the elements of the first list with those elements removed whose entries occur in the second list.

Example:

Specification of the list [6,5,6] with the second entry removed.

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
  <OMA><OMS cd="relation1" name="eq"/>
       <OMA><OMS cd="list4" name="remove"/>
            <OMA><OMS cd="list1" name="list"/>
                 <OMI> 6 </OMI>      <OMI> 5 </OMI>      <OMI> 6 </OMI>
            </OMA>
            <OMA><OMS cd="list1" name="list"/>
                 <OMI> 2 </OMI>
            </OMA>
       </OMA>
       <OMA><OMS cd="list1" name="list"/>
            <OMI> 6 </OMI>            <OMI> 6 </OMI>
       </OMA>
  </OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="relation1">eq</csymbol>
  <apply><csymbol cd="list4">remove</csymbol>
   <apply><csymbol cd="list1">list</csymbol>
    <cn type="integer">6</cn>
    <cn type="integer">5</cn>
    <cn type="integer">6</cn>
   </apply>
   <apply><csymbol cd="list1">list</csymbol><cn type="integer">2</cn></apply>
  </apply>
  <apply><csymbol cd="list1">list</csymbol>
   <cn type="integer">6</cn>
   <cn type="integer">6</cn>
  </apply>
 </apply>
</math>

Prefix

eq (remove (list ( 6 , 5 , 6 ) , list ( 2 ) ) , list ( 6 , 6 ) )

Popcorn

list4.remove([6 , 5 , 6], [2]) = [6 , 6]

Rendered Presentation MathML

$$\mathrm{remove}((6,5,6),\left(2\right))=(6,6)$$

Signatures:

sts

---

[Next: list_of_lengthn] [Previous: difference] [Top]

---

list_of_lengthn

Description:

This symbol represents a function with two arguments, the first of which is a natural number and the second of which is a list. The first argument is the length of the list.

Example:

A list L of length 3:

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
  <OMA><OMS cd="list4" name="list_of_lengthn"/>
       <OMI> 3 </OMI>
       <OMA><OMS cd="list1" name="list"/>
            <OMV name="L"/>
       </OMA>
  </OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="list4">list_of_lengthn</csymbol>
  <cn type="integer">3</cn>
  <apply><csymbol cd="list1">list</csymbol><ci>L</ci></apply>
 </apply>
</math>

Prefix

list_of_lengthn ( 3 , list ( L) )

Popcorn

list4.list_of_lengthn(3, [$L])

Rendered Presentation MathML

$$\mathrm{list\_of\_lengthn}(3,\left(L\right))$$

Signatures:

sts

---

[First: entry] [Previous: remove] [Top]