OpenMath Content Dictionary: fns2

Canonical URL:
http://www.openmath.org/cd/fns2.ocd
CD File:
fns2.ocd
CD as XML Encoded OpenMath:
fns2.omcd
Defines:
apply_to_list, kernel, right_compose
Date:
2001-03-12
Version:
2
Review Date:
2003-04-01
Status:
official
Uses CD:
arith1, fns1, list1, quant1, relation1, set1, logic1, relation1, alg1

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

apply_to_list

which applies an nary function to all the elements in a specified list. For example, such a function can be used to form sums and products in conjunction with plus and times respectively.


kernel

This symbol denotes the kernel of a given function. This may be defined as the subset of the range of the given function which maps to the identity element of the image of the given function, however no semantics are assumed. The kernel of a function is also known as the null space of the function.

Commented Mathematical property (CMP):
x in the kernal of f implies that f(x) = 0
Formal Mathematical property (FMP):
<OMOBJ>
  <OMA>
    <OMS cd="logic1" name="implies"/>
    <OMA>
      <OMS cd="set1" name="in"/>
      <OMV name="x"/>
      <OMA>
        <OMS cd="fns2" name="kernel"/>
        <OMV name="f"/>
      </OMA>
    </OMA>
    <OMA>
      <OMS cd="relation1" name="eq"/>
      <OMA>
        <OMV name="f"/>
	<OMV name="x"/>
      </OMA>
      <OMS cd="alg1" name="zero"/>
    </OMA>
  </OMA>
</OMOBJ>

implies (in ( x, kernel ( f) ) , eq ( f ( x) , zero) )

Signatures:
sts


[Next: apply_to_list] [Last: right_compose] [Top]

apply_to_list

This symbol is used to denote the repeated application of an n-ary function on the elements of a given list. For example when used with plus or times this can represent sums and products.

The symbol takes two arguments; the first of which is the n-ary function, the second a list.

Example:
For all n 1 + 2 + ... + n = n(n+1)/2.
<OMOBJ>
  <OMBIND>
    <OMS cd="quant1" name="forall"/>
    <OMBVAR>
      <OMV name="n"/>
    </OMBVAR>
    <OMA>
      <OMS cd="relation1" name="eq"/>
      <OMA>
        <OMS cd="fns2" name="apply_to_list"/>
        <OMS cd="arith1" name="plus"/>
        <OMA>
          <OMS cd="list1" name="make_list"/>
          <OMI> 1 </OMI>
          <OMV name="n"/>
          <OMS cd="fns1" name="identity"/>
        </OMA>
      </OMA>
      <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>
    </OMA>
  </OMBIND>
</OMOBJ>

forall [ n ] . (eq (apply_to_list (plus, make_list ( 1 , n, identity) ) , divide (times ( n, plus ( n, 1 ) ) , 2 ) ) )

Example:
One may form a set in the following way. This gives the set {1^2, 2^2, ... , 10^2 }
<OMOBJ>
  <OMA>
    <OMS cd="fns2" name="apply_to_list"/>
    <OMS cd="set1" name="set"/>
    <OMA>
      <OMS cd="list1" name="make_list"/>
      <OMI> 1 </OMI>
      <OMI> 10 </OMI>
      <OMBIND>
        <OMS cd="fns1" name="lambda"/>
        <OMBVAR>
          <OMV name="x"/>
        </OMBVAR>
        <OMA>
         <OMS cd="arith1" name="power"/>
          <OMV name="x"/>
          <OMI> 2 </OMI>
        </OMA>
      </OMBIND>
    </OMA>
  </OMA>
</OMOBJ>

apply_to_list (set, make_list ( 1 , 10 , lambda [ x ] . (power ( x, 2 ) ) ) )

Signatures:
sts


[Next: right_compose] [Previous: kernel] [Top]

right_compose

This symbol represents a function forming the right-composition of its two functional arguments.

Commented Mathematical property (CMP):
right_compose(f,g)(x) = g(f(x))
Formal Mathematical property (FMP):
<OMOBJ>
    <OMBIND>
      <OMS cd="quant1" name="forall"/>
      <OMBVAR>
        <OMV name="f"/>
        <OMV name="g"/>
        <OMV name="x"/>
      </OMBVAR>
      <OMA>
        <OMS cd="relation1" name="eq"/>
        <OMA>
          <OMA>
            <OMS cd="fns2" name="right_compose"/>
            <OMV name="f"/>
            <OMV name="g"/>
          </OMA>
          <OMV name="x"/>
        </OMA>
        <OMA>
          <OMV name="g"/>
          <OMA>
            <OMV name="f"/>
            <OMV name="x"/>
          </OMA>
        </OMA>
      </OMA>
    </OMBIND>
  </OMOBJ>

forall [ f g x ] . (eq (right_compose ( f, g) ( x) , g ( f ( x) ) ) )

Signatures:
sts


[First: kernel] [Previous: apply_to_list] [Top]