OpenMath Content Dictionary: fns3

Canonical URL:

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

CD File:

fns3.ocd

CD as XML Encoded OpenMath:

fns3.omcd

Defines:

function, specification

Date:

2004-06-01

Version:

1 (Revision 1)

Review Date:

2006-06-01

Status:

experimental

This CD holds further functions concerning functions themselves. A particularly interesting function is

function

which constructs a function with given domain and range.

function

Description:

This symbol denotes a function constructor. When aplied to at least two arguments, which are sets, the first argument is the domain and the second the range of the function. When applied to at least three arguments, the first two of which are stes and the third of which is a lambda expression, the third argument gives the function specification.

Commented Mathematical property (CMP):

The domain of the function f constructed this way is the first argument

Formal Mathematical property (FMP):

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
  <OMA><OMS cd="relation1" name="eq"/>
       <OMA><OMS cd="fns1" name="domain"/>
            <OMA><OMS cd="fns3" name="function"/>
                 <OMV name="X"/>            <OMV name="Y"/>            <OMV name="Z"/>
            </OMA>
       </OMA>
       <OMV name="X"/>
  </OMA>
</OMOBJ>

eq (domain (function ( X, Y, Z) ) , X)

$$\mathrm{domain}\left(\mathrm{function}(X,Y,Z)\right)=X$$

Commented Mathematical property (CMP):

The range of the function f constructed this way is the second argument

Formal Mathematical property (FMP):

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
  <OMA><OMS cd="relation1" name="eq"/>
       <OMA><OMS cd="fns1" name="range"/>
            <OMA><OMS cd="fns3" name="function"/>
                 <OMV name="X"/>            <OMV name="Y"/>            <OMV name="Z"/>
            </OMA>
       </OMA>
       <OMV name="Y"/>
  </OMA>
</OMOBJ>

eq (range (function ( X, Y, Z) ) , Y)

$$\mathrm{range}\left(\mathrm{function}(X,Y,Z)\right)=Y$$

Example:

The following object defines a function from the natural numbers into the integers specificied by the fact that n maps to n(n+1)/2.

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
   <OMA><OMS cd="fns3" name="function"/>
        <OMS cd="setname1" name="N"/>
        <OMS cd="setname1" name="Z"/>
        <OMBIND><OMS cd="fns1" name="lambda"/>
                <OMBVAR><OMV name="n"/></OMBVAR>
                <OMA><OMS cd="arith1" name="divide"/>
                     <OMA><OMS cd="arith1" name="times"/>
                          <OMV name="n"/>
                          <OMA><OMS cd="arith1" name="plus"/>
                               <OMV name="n"/>
                               <OMI> 1 </OMI>
                          </OMA>
                     </OMA>
                     <OMI> 2 </OMI>
                </OMA>
        </OMBIND>
   </OMA>
</OMOBJ>

function (N, Z, lambda [ n] . (divide (times ( n, plus ( n, 1 ) ) , 2 ) ) )

$$\mathrm{function}(\mathbb{N},\mathbb{Z},\lambda \hspace{0.17em}n.\frac{n(n+1)}{2})$$

Signatures:

sts

specification

Description:

This symbol denotes the specification of a function. It is a unary function. When aplied to its argument, which should be a function applied to three arguments, it returns the third argument of the function, that is, the function specification.

Formal Mathematical property (FMP):

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
<OMA><OMS cd="relation1" name="eq"/>
     <OMA><OMS cd="fns3" name="specification"/>
          <OMA><OMS cd="fns3" name="function"/>
               <OMS cd="setname1" name="N"/>
               <OMS cd="setname1" name="Z"/>
               <OMV name="f"/>
          </OMA>
     </OMA>
     <OMV name="f"/>
</OMA>
</OMOBJ>

eq (specification (function (N, Z, f) ) , f)

$$\mathrm{specification}\left(\mathrm{function}(\mathbb{N},\mathbb{Z},f)\right)=f$$

Example:

The following object defines a function from the natural numbers into the integers specificied by the fact that n maps to n(n+1)/2.

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
<OMA><OMS cd="relation1" name="eq"/>
   <OMA><OMS cd="fns3" name="specification"/>
        <OMA><OMS cd="fns3" name="function"/>
             <OMS cd="setname1" name="N"/>
             <OMS cd="setname1" name="Z"/>
             <OMBIND><OMS cd="fns1" name="lambda"/>
                <OMBVAR><OMV name="n"/></OMBVAR>
                <OMA><OMS cd="arith1" name="divide"/>
                     <OMA><OMS cd="arith1" name="times"/>
                          <OMV name="n"/>
                          <OMA><OMS cd="arith1" name="plus"/>
                               <OMV name="n"/>
                               <OMI> 1 </OMI>
                          </OMA>
                     </OMA>
                     <OMI> 2 </OMI>
                </OMA>
             </OMBIND>
        </OMA>
   </OMA>
   <OMBIND><OMS cd="fns1" name="lambda"/>
           <OMBVAR><OMV name="n"/></OMBVAR>
           <OMA><OMS cd="arith1" name="divide"/>
                <OMA><OMS cd="arith1" name="times"/>
                     <OMV name="n"/>
                     <OMA><OMS cd="arith1" name="plus"/>
                          <OMV name="n"/>
                          <OMI> 1 </OMI>
                     </OMA>
                </OMA>
                <OMI> 2 </OMI>
           </OMA>
   </OMBIND>
</OMA>
</OMOBJ>

eq (specification (function (N, Z, lambda [ n] . (divide (times ( n, plus ( n, 1 ) ) , 2 ) ) ) ) , lambda [ n] . (divide (times ( n, plus ( n, 1 ) ) , 2 ) ) )

$$\mathrm{specification}\left(\mathrm{function}(\mathbb{N},\mathbb{Z},\lambda \hspace{0.17em}n.\frac{n(n+1)}{2})\right)=\lambda \hspace{0.17em}n.\frac{n(n+1)}{2}$$

Signatures:

sts