This document is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. The copyright holder grants you permission to redistribute this document freely as a verbatim copy. Furthermore, the copyright holder permits you to develop any derived work from this document provided that the following conditions are met. a) The derived work acknowledges the fact that it is derived from this document, and maintains a prominent reference in the work to the original source. b) The fact that the derived work is not the original OpenMath document is stated prominently in the derived work. Moreover if both this document and the derived work are Content Dictionaries then the derived work must include a different CDName element, chosen so that it cannot be confused with any works adopted by the OpenMath Society. In particular, if there is a Content Dictionary Group whose name is, for example, `math' containing Content Dictionaries named `math1', `math2' etc., then you should not name a derived Content Dictionary `mathN' where N is an integer. However you are free to name it `private_mathN' or some such. This is because the names `mathN' may be used by the OpenMath Society for future extensions. c) The derived work is distributed under terms that allow the compilation of derived works, but keep paragraphs a) and b) intact. The simplest way to do this is to distribute the derived work under the OpenMath license, but this is not a requirement. If you have questions about this license please contact the OpenMath society at http://www.openmath.org.
Author: OpenMath Consortium SourceURL: https://github.com/OpenMath/CDs
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.
kernelThis 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.
<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="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>
<math xmlns="http://www.w3.org/1998/Math/MathML"> <apply><csymbol cd="logic1">implies</csymbol> <apply><csymbol cd="set1">in</csymbol> <ci>x</ci> <apply><csymbol cd="fns2">kernel</csymbol><ci>f</ci></apply> </apply> <apply><csymbol cd="relation1">eq</csymbol> <apply><ci>f</ci><ci>x</ci></apply> <csymbol cd="alg1">zero</csymbol> </apply> </apply> </math>
set1.in($x, fns2.kernel($f)) ==> $f($x) = alg1.zero
x ∈ kernel ( f ) ⇒ f ( x ) = 0
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.
<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="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="map"/> <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>
<math xmlns="http://www.w3.org/1998/Math/MathML"> <bind><csymbol cd="quant1">forall</csymbol> <bvar><ci>n</ci></bvar> <apply><csymbol cd="relation1">eq</csymbol> <apply><csymbol cd="fns2">apply_to_list</csymbol> <csymbol cd="arith1">plus</csymbol> <apply><csymbol cd="list1">map</csymbol> <cn type="integer">1</cn> <ci>n</ci> <csymbol cd="fns1">identity</csymbol> </apply> </apply> <apply><csymbol cd="arith1">divide</csymbol> <apply><csymbol cd="arith1">times</csymbol> <ci>n</ci> <apply><csymbol cd="arith1">plus</csymbol><ci>n</ci><cn type="integer">1</cn></apply> </apply> <cn type="integer">2</cn> </apply> </apply> </bind> </math>
quant1.forall[$n -> fns2.apply_to_list(arith1.plus, list1.map(1, $n, fns1.identity)) = ($n * ($n + 1)) / 2]
∀ n . apply_to_list ( + , map ( 1 , n , Id ) ) = n ( n + 1 ) 2
<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0" cdbase="http://www.openmath.org/cd"> <OMA> <OMS cd="fns2" name="apply_to_list"/> <OMS cd="set1" name="set"/> <OMA> <OMS cd="list1" name="map"/> <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>
<math xmlns="http://www.w3.org/1998/Math/MathML"> <apply><csymbol cd="fns2">apply_to_list</csymbol> <csymbol cd="set1">set</csymbol> <apply><csymbol cd="list1">map</csymbol> <cn type="integer">1</cn> <cn type="integer">10</cn> <bind><csymbol cd="fns1">lambda</csymbol> <bvar><ci>x</ci></bvar> <apply><csymbol cd="arith1">power</csymbol><ci>x</ci><cn type="integer">2</cn></apply> </bind> </apply> </apply> </math>
fns2.apply_to_list(set1.set, list1.map(1, 10, fns1.lambda[$x -> $x ^ 2]))
This symbol is used to denote the chains of application or a binary predicate typified by a < b < c. In particular it is used to support the usage in MathML, where transative relations are classed as nary, but the underlying OpenMath symbols are binary.
The symbol takes two arguments; the first of which is the binary predicate, the second a list. It is true if every application of the predicate on a pair of elements of the list, taken in order, returns true, otherwise it is false.
<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0" cdbase="http://www.openmath.org/cd"> <OMA> <OMS cd="fns2" name="predicate_on_list"/> <OMS cd="relation1" name="lt"/> <OMA> <OMS cd="list1" name="list"/> <OMV name="a"/> <OMV name="b"/> <OMV name="c"/> </OMA> </OMA> </OMOBJ>
<math xmlns="http://www.w3.org/1998/Math/MathML"> <apply><csymbol cd="fns2">predicate_on_list</csymbol> <csymbol cd="relation1">lt</csymbol> <apply><csymbol cd="list1">list</csymbol><ci>a</ci><ci>b</ci><ci>c</ci></apply> </apply> </math>
fns2.predicate_on_list(relation1.lt, [$a , $b , $c])
<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="fns2" name="predicate_on_list"/> <OMV name="p"/> <OMS cd="list2" name="nil"/> </OMA> <OMS cd="logic1" name="true"/> </OMA> </OMOBJ>
<math xmlns="http://www.w3.org/1998/Math/MathML"> <apply><csymbol cd="relation1">eq</csymbol> <apply><csymbol cd="fns2">predicate_on_list</csymbol><ci>p</ci><csymbol cd="list2">nil</csymbol></apply> <csymbol cd="logic1">true</csymbol> </apply> </math>
fns2.predicate_on_list($p, list2.nil) = logic1.true
predicate_on_list ( p , nil ) = T
<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="fns2" name="predicate_on_list"/> <OMV name="p"/> <OMA> <OMS cd="list2" name="append"/> <OMV name="a"/> <OMS cd="list2" name="nil"/> </OMA> </OMA> <OMS cd="logic1" name="true"/> </OMA> </OMOBJ>
<math xmlns="http://www.w3.org/1998/Math/MathML"> <apply><csymbol cd="relation1">eq</csymbol> <apply><csymbol cd="fns2">predicate_on_list</csymbol> <ci>p</ci> <apply><csymbol cd="list2">append</csymbol><ci>a</ci><csymbol cd="list2">nil</csymbol></apply> </apply> <csymbol cd="logic1">true</csymbol> </apply> </math>
fns2.predicate_on_list($p, list2.append($a, list2.nil)) = logic1.true
predicate_on_list ( p , append ( a , nil ) ) = T
<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="fns2" name="predicate_on_list"/> <OMV name="p"/> <OMA> <OMS cd="list2" name="append"/> <OMV name="a"/> <OMA> <OMS cd="list2" name="append"/> <OMV name="b"/> <OMV name="l"/> </OMA> </OMA> </OMA> <OMA> <OMS cd="logic1" name="and"/> <OMA> <OMV name="p"/> <OMV name="a"/> <OMV name="b"/> </OMA> <OMA> <OMS cd="fns2" name="predicate_on_list"/> <OMV name="p"/> <OMA> <OMS cd="list2" name="append"/> <OMV name="b"/> <OMV name="l"/> </OMA> </OMA> </OMA> </OMA> </OMOBJ>
<math xmlns="http://www.w3.org/1998/Math/MathML"> <apply><csymbol cd="relation1">eq</csymbol> <apply><csymbol cd="fns2">predicate_on_list</csymbol> <ci>p</ci> <apply><csymbol cd="list2">append</csymbol> <ci>a</ci> <apply><csymbol cd="list2">append</csymbol><ci>b</ci><ci>l</ci></apply> </apply> </apply> <apply><csymbol cd="logic1">and</csymbol> <apply><ci>p</ci><ci>a</ci><ci>b</ci></apply> <apply><csymbol cd="fns2">predicate_on_list</csymbol> <ci>p</ci> <apply><csymbol cd="list2">append</csymbol><ci>b</ci><ci>l</ci></apply> </apply> </apply> </apply> </math>
fns2.predicate_on_list($p, list2.append($a, list2.append($b, $l))) = ($p($a, $b) and fns2.predicate_on_list($p, list2.append($b, $l)))
predicate_on_list ( p , append ( a , append ( b , l ) ) ) = p ( a , b ) ∧ predicate_on_list ( p , append ( b , l ) )
This symbol represents a function forming the right-composition of its two functional arguments.
<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="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>
<math xmlns="http://www.w3.org/1998/Math/MathML"> <bind><csymbol cd="quant1">forall</csymbol> <bvar><ci>f</ci></bvar> <bvar><ci>g</ci></bvar> <bvar><ci>x</ci></bvar> <apply><csymbol cd="relation1">eq</csymbol> <apply> <apply><csymbol cd="fns2">right_compose</csymbol><ci>f</ci><ci>g</ci></apply> <ci>x</ci> </apply> <apply><ci>g</ci><apply><ci>f</ci><ci>x</ci></apply></apply> </apply> </bind> </math>
quant1.forall[$f, $g, $x -> fns2.right_compose($f, $g)($x) = $g($f($x))]
∀ f , g , x . ( right_compose ( f , g ) ) ( x ) = g ( f ( x ) )
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.5