OpenMath Content Dictionary: list2

Canonical URL:

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

CD Base:

http://www.openmath.org/cd

CD File:

list2.ocd

CD as XML Encoded OpenMath:

list2.omcd

Defines:

append, cons, first, in, list_selector, nil, rest, reverse, size

Date:

2004-03-30

Version:

4 (Revision 2)

Review Date:

2017-12-31

Status:

experimental

---

  Author: OpenMath Consortium
  SourceURL: https://github.com/OpenMath/CDs
            

Several basic list functions are given in this CD.

---

list_selector

Role:

application

Description:

This symbol takes a positive integer n and a list, and represents the n-th element of that list.

Example:

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"/>
  <OMV name="b"/>
  <OMA>
    <OMS name="list_selector" cd="list2"/>
    <OMI> 2 </OMI>
    <OMA>
      <OMS name="list" cd="list1"/>
      <OMV name="a"/>
      <OMV name="b"/>
      <OMV name="c"/>
    </OMA>
  </OMA>
</OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="relation1">eq</csymbol>
  <ci>b</ci>
  <apply><csymbol cd="list2">list_selector</csymbol>
   <cn type="integer">2</cn>
   <apply><csymbol cd="list1">list</csymbol><ci>a</ci><ci>b</ci><ci>c</ci></apply>
  </apply>
 </apply>
</math>

Prefix

eq ( b, list_selector ( 2 , list ( a, b, c) ) )

Popcorn

$b = list2.list_selector(2, [$a , $b , $c])

Rendered Presentation MathML

$$b={(a,b,c)}_2$$

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="logic1" name="implies"/>
  <OMA>
    <OMS cd="relation1" name="gt"/>
    <OMV name="n"/>
    <OMI> 1 </OMI>
  </OMA>
  <OMA>
    <OMS cd="relation1" name="eq"/>
    <OMA>
      <OMS name="list_selector" cd="list2"/>
      <OMV name="n"/>
      <OMV name="l"/>
    </OMA>
    <OMA>
      <OMS name="list_selector" cd="list2"/>
      <OMA>
	<OMS name="minus" cd="arith1"/>
        <OMV name="n"/>
        <OMI> 1 </OMI>
      </OMA>
      <OMA>
	<OMS name="rest" cd="list2"/>
        <OMV name="l"/>
      </OMA>
    </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>n</ci><cn type="integer">1</cn></apply>
  <apply><csymbol cd="relation1">eq</csymbol>
   <apply><csymbol cd="list2">list_selector</csymbol><ci>n</ci><ci>l</ci></apply>
   <apply><csymbol cd="list2">list_selector</csymbol>
    <apply><csymbol cd="arith1">minus</csymbol><ci>n</ci><cn type="integer">1</cn></apply>
    <apply><csymbol cd="list2">rest</csymbol><ci>l</ci></apply>
   </apply>
  </apply>
 </apply>
</math>

Prefix

implies (gt ( n, 1 ) , eq (list_selector ( n, l) , list_selector (minus ( n, 1 ) , rest ( l) ) ) )

Popcorn

$n > 1 ==> list2.list_selector($n, $l) = list2.list_selector($n - 1, list2.rest($l))

Rendered Presentation MathML

$$n>1\Rightarrow l_n={\mathrm{rest}\left(l\right)}_{n-1}$$

Signatures:

sts

---

[Next: first] [Last: in] [Top]

---

first

Role:

application

Description:

This symbol represents a function which returns the first elements of its argument, which should be 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"/>
      <OMV name="a"/>
      <OMA>
        <OMS cd="list2" name="first"/>
        <OMA>
          <OMS cd="list2" name="cons"/>
          <OMV name="a"/>
          <OMV name="b"/>
        </OMA>
      </OMA>
    </OMA>
  </OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="relation1">eq</csymbol>
  <ci>a</ci>
  <apply><csymbol cd="list2">first</csymbol>
   <apply><csymbol cd="list2">cons</csymbol><ci>a</ci><ci>b</ci></apply>
  </apply>
 </apply>
</math>

Prefix

eq ( a, first (cons ( a, b) ) )

Popcorn

$a = list2.first(list2.cons($a, $b))

Rendered Presentation MathML

$$a=\mathrm{first}\left(\mathrm{cons}(a,b)\right)$$

Example:

Specification of the first element of the list [1,2,3]

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0" cdbase="http://www.openmath.org/cd">
  <OMA>
    <OMS cd="list2" name="first"/>
    <OMA>
      <OMS cd="list1" name="list"/>
      <OMI> 1 </OMI>
      <OMI> 2 </OMI>
      <OMI> 3 </OMI>
    </OMA>
  </OMA>
</OMOBJ>

Strict Content MathML

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

Prefix

first (list ( 1 , 2 , 3 ) )

Popcorn

list2.first([1 , 2 , 3])

Rendered Presentation MathML

$$\mathrm{first}\left((1,2,3)\right)$$

Signatures:

sts

---

[Next: rest] [Previous: list_selector] [Top]

---

rest

Role:

application

Description:

This symbol represents a function which returns a list made up of all the elements except the first of its argument, which should be 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"/>
      <OMV name="b"/>
      <OMA>
        <OMS cd="list2" name="rest"/>
        <OMA>
          <OMS cd="list2" name="cons"/>
          <OMV name="a"/>
          <OMV name="b"/>
        </OMA>
      </OMA>
    </OMA>
  </OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="relation1">eq</csymbol>
  <ci>b</ci>
  <apply><csymbol cd="list2">rest</csymbol>
   <apply><csymbol cd="list2">cons</csymbol><ci>a</ci><ci>b</ci></apply>
  </apply>
 </apply>
</math>

Prefix

eq ( b, rest (cons ( a, b) ) )

Popcorn

$b = list2.rest(list2.cons($a, $b))

Rendered Presentation MathML

$$b=\mathrm{rest}\left(\mathrm{cons}(a,b)\right)$$

Example:

Specification of the list [1,2,3], apart from the first element

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0" cdbase="http://www.openmath.org/cd">
  <OMA>
    <OMS cd="list2" name="rest"/>
    <OMA>
      <OMS cd="list1" name="list"/>
      <OMI> 1 </OMI>
      <OMI> 2 </OMI>
      <OMI> 3 </OMI>
    </OMA>
  </OMA>
</OMOBJ>

Strict Content MathML

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

Prefix

rest (list ( 1 , 2 , 3 ) )

Popcorn

list2.rest([1 , 2 , 3])

Rendered Presentation MathML

$$\mathrm{rest}\left((1,2,3)\right)$$

Signatures:

sts

---

[Next: cons] [Previous: first] [Top]

---

cons

Role:

application

Description:

This symbol represents the cons list function. It takes 2 arguments: the second must be a list, where the elements have the same type as the type of the first. The function denotes a new list which has the first argument as its first element followed by the elements of the second argument.

Commented Mathematical property (CMP):

cons(first(lst),rest(lst))=lst

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"/>
    </OMBVAR>
    <OMA>
      <OMS cd="relation1" name="eq"/>
      <OMA>
        <OMS cd="list2" name="cons"/>
        <OMA>
          <OMS cd="list2" name="first"/>
          <OMV name="lst"/>
        </OMA>
        <OMA>
          <OMS cd="list2" name="rest"/>
          <OMV name="lst"/>
        </OMA>
      </OMA>
      <OMV name="lst"/>
    </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>
  <apply><csymbol cd="relation1">eq</csymbol>
   <apply><csymbol cd="list2">cons</csymbol>
    <apply><csymbol cd="list2">first</csymbol><ci>lst</ci></apply>
    <apply><csymbol cd="list2">rest</csymbol><ci>lst</ci></apply>
   </apply>
   <ci>lst</ci>
  </apply>
 </bind>
</math>

Prefix

forall [ lst ] . (eq (cons (first ( lst) , rest ( lst) ) , lst) )

Popcorn

quant1.forall[$lst -> list2.cons(list2.first($lst), list2.rest($lst)) = $lst]

Rendered Presentation MathML

$$\forall \hspace{0.17em}\mathrm{lst}.\mathrm{cons}(\mathrm{first}\left(\mathrm{lst}\right),\mathrm{rest}\left(\mathrm{lst}\right))=\mathrm{lst}$$

Signatures:

sts

---

[Next: nil] [Previous: rest] [Top]

---

nil

Role:

constant

Description:

The empty list

Signatures:

sts

---

[Next: append] [Previous: cons] [Top]

---

append

Role:

application

Description:

The operation of joining one list to another

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="a"/>
      <OMV name="lst1"/>
      <OMV name="lst2"/>
    </OMBVAR>
    <OMA>
      <OMS cd="relation1" name="eq"/>
      <OMA>
        <OMS cd="list2" name="cons"/>
        <OMV name="a"/>
        <OMA>
          <OMS cd="list2" name="append"/>
          <OMV name="lst1"/>
          <OMV name="lst2"/>
        </OMA>
      </OMA>
      <OMA>
        <OMS cd="list2" name="append"/>
        <OMA>
          <OMS cd="list2" name="cons"/>
          <OMV name="a"/>
          <OMV name="lst1"/>
        </OMA>
        <OMV name="lst2"/>
      </OMA>
    </OMA>
  </OMBIND>
</OMOBJ>

Strict Content MathML

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

Prefix

forall [ a lst1 lst2 ] . (eq (cons ( a, append ( lst1, lst2) ) , append (cons ( a, lst1) , lst2) ) )

Popcorn

quant1.forall[$a, $lst1, $lst2 -> list2.cons($a, list2.append($lst1, $lst2)) = list2.append(list2.cons($a, $lst1), $lst2)]

Rendered Presentation MathML

$$\forall \hspace{0.17em}a,{\mathrm{lst}}_1,{\mathrm{lst}}_2.\mathrm{cons}(a,\mathrm{append}({\mathrm{lst}}_1,{\mathrm{lst}}_2))=\mathrm{append}(\mathrm{cons}(a,{\mathrm{lst}}_1),{\mathrm{lst}}_2)$$

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"/>
    </OMBVAR>
    <OMA>
      <OMS cd="relation1" name="eq"/>
      <OMV name="lst"/>
      <OMA>
        <OMS cd="list2" name="append"/>
        <OMS cd="list2" name="nil"/>
        <OMV name="lst"/>
      </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>
  <apply><csymbol cd="relation1">eq</csymbol>
   <ci>lst</ci>
   <apply><csymbol cd="list2">append</csymbol><csymbol cd="list2">nil</csymbol><ci>lst</ci></apply>
  </apply>
 </bind>
</math>

Prefix

forall [ lst ] . (eq ( lst, append (nil, lst) ) )

Popcorn

quant1.forall[$lst -> $lst = list2.append(list2.nil, $lst)]

Rendered Presentation MathML

$$\forall \hspace{0.17em}\mathrm{lst}.\mathrm{lst}=\mathrm{append}(\mathrm{nil},\mathrm{lst})$$

Signatures:

sts

---

[Next: reverse] [Previous: nil] [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="list2" 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="list2">reverse</csymbol><csymbol cd="list2">nil</csymbol></apply>
  <csymbol cd="list2">nil</csymbol>
 </apply>
</math>

Prefix

eq (reverse (nil) , nil)

Popcorn

list2.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="list2" name="reverse"/>
        <OMA>
          <OMS cd="list2" name="cons"/>
          <OMV name="a"/>
          <OMV name="lst"/>
        </OMA>
      </OMA>
      <OMA>
        <OMS cd="list2" name="append"/>
        <OMA>
          <OMS cd="list2" 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="list2">reverse</csymbol>
    <apply><csymbol cd="list2">cons</csymbol><ci>a</ci><ci>lst</ci></apply>
   </apply>
   <apply><csymbol cd="list2">append</csymbol>
    <apply><csymbol cd="list2">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 -> list2.reverse(list2.cons($a, $lst)) = list2.append(list2.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: size] [Previous: append] [Top]

---

size

Role:

application

Description:

This symbol is used to denote the number of elements in a list. It is either a non-negative integer.

Example:

The size of the list (3,6,9) = 3

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="list2" name="size"/>
      <OMA>
        <OMS cd="list1" name="list"/>
        <OMI> 3 </OMI>
        <OMI> 6 </OMI>
        <OMI> 9 </OMI>
      </OMA>
    </OMA>
    <OMI> 3 </OMI>
  </OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="relation1">eq</csymbol>
  <apply><csymbol cd="list2">size</csymbol>
   <apply><csymbol cd="list1">list</csymbol>
    <cn type="integer">3</cn>
    <cn type="integer">6</cn>
    <cn type="integer">9</cn>
   </apply>
  </apply>
  <cn type="integer">3</cn>
 </apply>
</math>

Prefix

eq (size (list ( 3 , 6 , 9 ) ) , 3 )

Popcorn

list2.size([3 , 6 , 9]) = 3

Rendered Presentation MathML

$$\mathrm{size}\left((3,6,9)\right)=3$$

Signatures:

sts

---

[Next: in] [Previous: reverse] [Top]

---

in

Role:

application

Description:

This symbol has two arguments, an element and a list. It is used to denote that the element is in the given list.

Signatures:

sts

---

[First: list_selector] [Previous: size] [Top]