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

Review Date:

2006-03-30

Status:

experimental

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:

xml prefix mathml

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

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

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

Formal Mathematical property (FMP):

xml prefix mathml

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

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

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

Signatures:

sts

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

xml prefix mathml

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

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

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

Example:

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

xml prefix mathml

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

first (list ( 1 , 2 , 3 ) )

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

Signatures:

sts

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

xml prefix mathml

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

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

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

Example:

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

xml prefix mathml

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

rest (list ( 1 , 2 , 3 ) )

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

Signatures:

sts

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

xml prefix mathml

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

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

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

Signatures:

sts

nil

Role:

constant

Description:

The empty list

Signatures:

sts

append

Role:

application

Description:

The operation of joining one list to another

Formal Mathematical property (FMP):

xml prefix mathml

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

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

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

xml prefix mathml

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

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

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

Signatures:

sts

reverse

Role:

application

Description:

The reverse of a list

Formal Mathematical property (FMP):

xml prefix mathml

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

eq (reverse (nil) , nil)

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

Formal Mathematical property (FMP):

xml prefix mathml

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

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

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

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

xml prefix mathml

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

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

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

Signatures:

sts

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