The goals of this Note are to demonstrate how the existing structures in MathML can be used to attach detailed mathematical type information to various parts of an expression. This document attempts to:
clarify the role of the type attribute in MathML,
demonstrate in detail how to attach more advanced type information to a MathML object,
illustrate this technique with examples using various type systems, including the types discussed in Appendix C (Content Element Definitions) of the MathML 2.0 Recommendation, the type system used by OpenMath [OpenMath], and an example of a more complicated type system.
MathML is an XML application for describing mathematical notation which allows the encoding of both structure and content of mathematics. While based on a mathematical vocabulary derived largely from school and early university levels, it is extensible in a number of ways. The primary purpose of this Note is to show how these extension mechanisms can be used to associate detailed mathematical type information with individual expressions or parts of expressions.
MathML has many roles. Depending on the goal of an author they may choose to provide a detailed visual presentation of a mathematical object, a more abstract mathematical description of the object, or both. More than one presentation of MathML content is possible, visual, aural or other, and authors are able to attach a wide variety of additional information to their mathematical equations of formulas.
When the author's goal is to provide a detailed representation of a mathematical object, it is necessary to be able to record the mathematical types of the various parts of this representation. For example, the terms in a product may be scalars or vectors, or the elements of a vector may be integers, complex numbers or symbols representing them.
Content MathML, as specified in Chapter 4 of the MathML 2 Recommendation defines an attribute called type, which provides limited support for mathematical types by allowing authors to specify simple values such as "real", "integer" or "complex-cartesian" as the content of the attribute. Such a simple construct is hardly sufficient for specifying complex type information, especially as the use of the attribute is not allowed on all the elements where one might want to use it. Furthermore, another problem is illustrated by the example below:
<math>
<apply>
<tendsto type="above"/>
<ci>x</ci>
<cn>0</cn>
</apply>
</math>
In this example, the type attribute does not indicate the domain of the tendsto element, but rather the fact that the limit is reached from above. The attribute can therefore not be used to specify the domain of the tendsto operator.
Another situation where the current approach is problematic is where one needs to specify more complex types, for instance the type of functions on complex numbers yielding pairs of real numbers. Even though the content of the type attribute is open-ended, a specification of all possible object types would necessitate defining an attribute value syntax, e.g. "complex → pair(real,real)". However, this would add considerable complexity to the design of MathML implementations, as this syntax would require writing an specific parser.
Nevertheless there is a pressing need to express complex structured types in MathML, as modern treatments of formal and computational aspects of mathematics increasingly make use of elaborate type systems. However the observation that structured objects such as the example type above can be expressed very naturally in Content MathML leads to a better mechanism, detailed below.
The next section discusses the type attribute in detail. The following sections describe and discuss methods for incorporating richer type systems in Content MathML, followed by a number of examples showing possible scenarios.
In Content MathML, The type attribute is used to specify the basic type of a limited number of primitive objects. These include:
The cn element is used to specify actual numerical quantities. The attribute type indicates what type of number is being represented such as integer, rational, real or complex,
The following values are used in the Recommendation with a specific meaning: "real", "integer", "rational", "complex-cartesian", "complex-polar" and "constant". Other values are permitted for extensibility.
The ci element is used to name mathematical objects. It uses the type attribute primarily to indicate the kind of objects that are being represented.
The declare element can be used to establish a default type value for associating a type with other MathML elements such as the ci element. Either the type attribute or the contents of the declare element can be used to specify a type.
The set element is the container element that constructs a set of elements. The type attribute is used on the set element to clarify the kind of set that is represented. For example, a set may be a multiset.
The tendsto element is used to express the relation that a quantity is tending to a specified value. The type attribute is used on the tendsto element to indicate the direction of limits.
The MathML specification does not restrict the values of the type attribute in any way. Indeed the attribute content is defined as CDATA in the MathML Document Type Definition, which is sufficiently open to allow encoding elaborate type structures. However, this approach is not appropriate in many cases, for several reasons:
There are MathML elements that may require detailed type specifications but cannot have a type attribute.
The type attribute cannot easily be used for two purposes at once. For example, one might want to indicate that a set is a multiset and also that its elements are integers, or that a limit is reached from above and that it is over the domain of integers. To deal with these cases, it would be necessary, at least, to develop a notation for encoding such type combinations in the attribute value.
Embedding detailed type information in the value of the type attribute means that a complex syntax must be defined. Because it would reside in an attribute value, this syntax could not be XML, and thus would put extra implementation burden on MathML-aware applications.
Mathematical types are mathematical objects themselves and thus require a rich structure model, such as that of Content MathML, to describe them
In order to deal with more sophisticated typing systems, two key issues must be solved:
Specify a way to encode non-trivial mathematical type objects.
Determine a method to associate the type objects with the corresponding MathML object.
One simple way deal with the second issue is to use MathML's semantics element, which is defined to generally associate additional information with mathematical objects. Additionally this element supports both XML and non-XML based encodings through using annotation-xml and annotation elements.
Regarding the encoding problem, it is a well-known fact that developing a mathematical typing system is a difficult task. However, several such systems exist and each represents a major piece of development effort. Examples include the Simple Type System developed by the OpenMath Consortium [STS]. A significant part of Appendix C of MathML itself deals with the issues of types and how they are related. Fortunately, the semantics element is designed to support alternative notations, and thus allows using the typing systems mentioned.
The following section discusses in detail how the semantics element can be used to describe types.
semantics Element
The semantics element is designed to group together various kinds of information related to a particular mathematical object. For example, semantics is often used to provide both a Content MathML and a Presentation MathML representation of an object.
The semantics element is the container element for the MathML expression, together with its semantic mappings. semantics contains a variable number of child elements, the first of which is the object (which may itself be a complex element structure) to which additional semantic information is attached. The second and subsequent children elements, when present, are annotation or annotation-xml elements. Each of these elements can contain a definitionURL and a encoding attribute. Those attributes can be used to clarify the meaning of the content of a particular annotation-xml element, and the manner in which it is encoded, respectively.
The annotation element is a container for arbitrary data. This data may be in the form of raw text, computer algebra encodings, C programs, or any syntax a processing application might expect. The annotation element can contain an attribute called "encoding", defining the format in use. Note that the content model of annotation is PCDATA, so care must be taken that the particular encoding does not conflict with XML parsing rules.
The annotation-xml element is a container for semantic information in XML syntax. For example, an XML form of the OpenMath semantics could be contained in the element. Another possible use is to embed the Presentation MathML form of a construct given in Content MathML format in the first child element of semantics (or vice versa). annotation-xml can contain an encoding attribute specifying the format used.
By replacing a simple mathematical expression by a semantics element it is possible to attach additional information to a mathematical object. Some of that information may be multiple views of the object (in different formats), and one may be type information about the object. For example:
<semantics>
<apply><divide/><cn>123</cn><cn>456</cn></apply>
<annotation encoding="Mathematica">N[123/456, 39]</annotation>
<annotation encoding="TeX">
$0.269736842105263157894736842105263157894\ldots$
</annotation>
<annotation encoding="Maple">evalf(123/456, 39);</annotation>
<annotation-xml encoding="MathML-Presentation">
<mrow>
<mn> 0.269736842105263157894 </mn>
<mover accent='true'>
<mn> 736842105263157894 </mn>
<mo> ‾ </mo>
</mover>
</mrow>
</annotation-xml>
<annotation-xml encoding="OpenMath">
<OMA xmlns="http://www.openmath.org/OpenMath">
<OMS cd="arith1" name="divide"/>
<OMI>123</OMI>
<OMI>456</OMI>
</OMA>
</annotation-xml>
</semantics>
As the example shows, the encoding attribute is used similarly to a media type, as it indicates how to parse the content of the element. The attribute might indicate the use of a particular XML application such as an OpenMath dictionary or a particular entry of such a dictionary
The next section discusses some of the possible type encodings supported by this approach.
3.2 Some Encodings for Structured Type ObjectsSome computer algebra systems provide elaborate support for arbitrarily complex type systems. Such systems make it possible, for example, to associate with an identifier information such as the fact that it represents an operator that takes unary real-valued functions as input and returns similar functions as values (one example is the differentiation operator). This Note takes the approach that types are structured mathematical objects like any other object.
For example, the function type indicating a function that maps integers to natural numbers (Z → R) is sometimes written as:
(integer) --> (naturalnumber)
(This syntax is used for formatting signatures in appendix C of the MathML 2.0 Recommendation.) This function type might be written as a Content MathML object as
<apply> <csymbol definitionURL="types.html#funtype"/> <csymbol definitionURL="types.html#int_type"/> <csymbol definitionURL="types.html#nat_type"/> </apply>
where we assume a document called types.html, which specifies the type system employed and provides definitions for the symbols Z, →, and N. The type object Z → R is obtained by applying the function type constructor → to the set Z of integers and the set N of natural numbers.
An alternative representation of this function type that makes more direct use of existing content MathML elements is:
<apply> <csymbol definitionURL="types.html#funtype"/> <integers/> <naturalnumbers/> </apply>
The last two representations above explicitly encode the structure of the type as a Content MathML object. This representation of types greatly extends the set of available types in MathML, compared to the use of the type attribute (barring the use of URIs in the attribute).
The semantics element can be used to directly associate structured types (as introduced in the previous section) with a particular MathML object. For example:
<semantics>
<ci>F</ci>
<annotation encoding="ASCII"
definitionURL="http://www.example.org/MathML-2.0-appendixC">
(integer) --> (naturalnumber)
<annotation>
<annotation-xml encoding="MathMLType" definitionURL="types.html">
<apply>
<csymbol definitionURL="types.html#funtype"/>
<integers/>
<naturalnumbers/>
</apply>
<annotation-xml>
</semantics>
The second child element of the semantics element is a annotation element that contains type information in textual format. The third child element is an annotation-xml element that contains the XML representation of the type, using Content MathML markup.
The definitionURL attribute on the annotation-xml and annotation elements are used here to specify the nature of the information provided within the element (in this case, type information). The encoding attribute on the annotation-xml element specifies the format of the XML data. MathML applications can use the value of these attributes to determine whether they can deal with the type information, i.e. whether they support that particular type system.
In summary the MathML specification allows using the semantics element as a general annotation device for MathML objects, where the definitionURL attribute specifies the relation of the annotation to the first child of the semantics element. In particular, this mechanism can be used to attach structured type objects to mathematical objects. Below is a more complex example showing such a type annotation in OpenMath markup of the variable XZ represented using Content MathML markup. (see 4 Related Work: Types in OpenMath for more details).
<semantics>
<semantics id="typed-var">
<ci>X</ci>
<annotation-xml definitionURL="type.html" encoding="MathMLType">
<integers/>
</annotation-xml>
</semantics>
<annotation-xml encoding="OpenMath">
<OMOBJ xmlns="http://www.openmath.org/OpenMath">
<OMATTR xlink:href="typed-var">
<OMATP>
<OMS cd="sts" name="type"/>
<OMS cd="setname1" name="integers"/>
</OMATP>
<OMV name="X"/>
</OMATTR>
</OMOBJ>
</annotation-xml>
</semantics>
To make the correspondence clear, the parallel markup uses cross-references, as described in section 5.3.4 of the MathML2 specification.
3.4 Structured Types and Bound Variables.A natural place to annotate types in formulas is in the declaration of bound variables. For example:
<math>
<apply>
<forall/>
<bvar id="bvF">
<semantics>
<ci>F</ci>
<annotation-xml encoding="content-MathML"
definitionURL="types.html">
<apply>
<csymbol definitionURL="types.html#funtype"/>
<csymbol definitionURL="types.html#int_type"/>
<csymbol definitionURL="types.html#nat_type"/>
</apply>
</annotation-xml>
<annotation encoding="ASCII" definitionURL="type">
integer --> nat
</annotation>
</semantics>
</bvar>
<bvar id="bvx">
<semantics>
<ci>x</ci>
<annotation-xml encoding="content-MathML">
<csymbol definitionURL="types.html#int_type"/>
</annotation-xml>
<annotation encoding="ASCII" definitionURL="type">
integer
</annotation>
</semantics>
</bvar>
<apply><geq/>
<apply><ci definitionURL="bvF">F</ci>
<ci definitionURL="bvx">x</ci>
</apply>
<cn>0</cn>
</apply>
</apply>
</math>
Here the bound variables F and x are annotated with type information by using the semantics element. The correspondence between the declaring occurrence of the variable and the bound occurrences are made explicit by the use of the definitionURL attribute, which points to the respective bvar element (see [MathMLBVar] for a discussion of this technique).
Note that in this example, only the type information makes the formula true (or even meaningful) as in general it is not the case that applying arbitrary functions to arbitrary values yields results that are greater than or equal to zero.
A related way to express the information in the example above that does not use the semantics element in bvar is:
<math>
<apply>
<forall/>
<bvar><ci>F</ci></bvar>
<condition>
<apply>
<csymbol definitionURL="types.html#type_of"/>
<ci>F</ci>
<apply>
<csymbol definitionURL="types.html#funtype"/>
<csymbol definitionURL="types.html#int_type"/>
<csymbol definitionURL="types.html#nat_type"/>
</apply>
</apply>
</condition>
<bvar><ci>x</ci></bvar>
<condition>
<apply>
<csymbol definitionURL="types.html#type_of"/>
<ci>x</ci>
<csymbol definitionURL="types.html#int_type"/>
</apply>
</condition>
<apply><geq/><apply><ci>F</ci><ci>x</ci></apply><cn>0</cn></apply>
</apply>
</math>
Here, the condition element is used to express the type condition "such that F has type Z → R". The transformation from the first to the second representation is a well-known technique in typed logics called relativization[Oberschelp], which transforms formulas in a typed logic into untyped formulas without changing their meaning. Although the two representations have similar semantics (given reasonable assumptions), both have dramatically different computational properties in most formal systems. Therefore, they should not be conflated in Content MathML.
OpenMath is an XML encoding of mathematical objects, designed for extensibility. OpenMath and Content MathML are largely equivalent in expressive power, the main difference being that OpenMath uses a csymbol-like mechanism for representing symbols.
In this section we briefly compare the representation of structured types in content MathML and in OpenMath.
4.1 Representing and Associating Types in OpenMathThe following representation, which is the counterpart of the example above, shows how types are represented in OpenMath:
<OMOBJ>
<OMBIND>
<OMS cd="quant1" name="forall"/>
<OMBVAR>
<OMATTR>
<OMATP>
<OMS cd="types" name="type"/>
<OMA>
<OMS cd="types" name="funtype"/>
<OMS cd="types" name="int_type"/>
<OMS cd="types" name="nat_type"/>
</OMA>
</OMATP>
<OMV name="F"/>
</OMATTR>
<OMATTR>
<OMATP>
<OMS cd="types" name="type"/>
<OMS cd="types" name="int_type"/>
</OMATP>
<OMV name="x"/>
</OMATTR>
</OMBVAR>
<OMA>
<OMS cd="relation1" name="geq"/>
<OMA><OMV name="F"/><OMV name="x"/></OMA>
<OMI>0</OMI>
</OMA>
</OMBIND>
</OMOBJ>
OpenMath uses the OMBIND element for binding objects while MathML uses the apply element with bvar child (which corresponds to the OpenMath element OMBVAR, except that the latter can hold more than one variable). OpenMath uses the OMA element for applications, the OMS element instead of MathML's csymbol, and the OMV element for variables, instead of ci. This markup corresponds directly to Content MathML.
The main difference to the Content MathML example above is the treatment of annotations. Instead of the MathML semantics element, OpenMath uses the OMATTR element. Its first child is an OMATP element, which contains "attribute value pairs": the children at odd positions are symbols that specify the role of their following siblings (they are sometimes called "features"). In this case, the first OMS element whose name attribute has the value type specifies that the element following it is a type. The second child of the OMATTR element is the object to which the information in the first one is attached.
The representation of structured types proposed in this Note makes Content MathML as expressive as OpenMath for types. The feature symbols in OpenMath OMATP elements directly correspond to the value of the definitionURL attribute on the annotation-xml and annotation elements in exactly the same way the definitionURL attribute on a csymbol element corresponds to an OpenMath OMS element. MathML even slightly generalizes OpenMath, which only allows OpenMath representations as feature values. MathML allows arbitrary XML representations in annotation-xml elements, whose format can be specified in the encoding attribute. The equivalent of the annotation element can be used by the OpenMath OMSTR element as a feature value.
OpenMath comes with a dedicated type system, the "small type system (STS)" [STS]). Since all the core OpenMath symbols (which include counterparts to all MathML symbols and containers) have STS types, this makes it a good candidate for using structured types in content MathML. The simple type system can be used to check arities of functions, and expresses roughly the same information as the content validation grammar in Appendix B of the MathML 2 specification.
The symbols supplied by the STS system can be found in the sts OpenMath Content Dictionary; the symbols corresponding to the values used in the type attribute discussed in 2 The type attribute can be found in the mathmltypes Content Dictionary. Using these Content Dictionaries as targets for the definitionURL attribute makes the following three representations equivalent:
<ci type="integer">φ</ci>
<semantics>
<ci>φ</ci>
<annotation-xml encoding="Content-MathML"
definitionURL="http://www.openmath.org/standard/sts.pdf">
<csymbol definitionURL="http://www.openmath.org/cd/mathmltypes.html#complex_cartesian_type"/>
</annotation-xml>
</semantics>
<semantics>
<ci>φ</ci>
<annotation-xml encoding="OpenMath"
definitionURL="http://www.openmath.org/standard/sts.pdf">
<OMS xmlns="http://www.openmath.org/OpenMath" cd="mathmltypes" name="complex_cartesian_type"/>
</annotation-xml>
</semantics>5 Types as used in appendix C of MathML 2
The primary place where mathematical types arise in MathML is in the notation of the signature of the various mathematical objects defined in appendix C:
The signature is a systematic representation that associates the types of different possible combinations of attributes and function arguments to type of mathematical object that is constructed. The possible combinations of parameter and argument types (the left-hand side) each result in an object of some type (the right-hand side). In effect, it describes how to resolve operator overloading.
For constructors, the left-hand side of the signature describes the types of the child elements and the right-hand side describes the type of object that is constructed. For functions, the left-hand side of the signature indicates the types of the parameters and arguments that would be expected when it is applied, or used to construct a relation, and the right-hand side represents the mathematical type of the object constructed by the apply. Modifiers modify the attributes of an existing object. For example, a symbol might become a symbol of type vector.
The signature must be able to record specific attribute values and argument types on the left, and parameterized types on the right.. The syntax used for signatures is of the general form:
[<attribute name>=<attribute-value>]( <list of argument types> ) --> <mathematical result type>(<mathematical subtype>)
The MMLattributes, if any, appear in the form <name>=<value>. They are separated notationally from the rest of the arguments by square brackets. The possible values are usually taken from an enumerated list, and the signature is usually affected by selection of a specific value.
For the actual function arguments and named parameters on the left, the focus is on the mathematical types involved. The function argument types are presented in a syntax similar to that used for a DTD, with the one main exception. The types of the named parameters appear in the signature as <elementname>=<type> in a manner analogous for that used for attribute values. For example, if the argument is named (e.g. bvar) then it is represented in the signature by an equation as in:
[<attribute name>=<attributevalue>]( bvar=symbol,<argument list> ) --> <mathematical result type>(<mathematical subtype>)
There is no formal type system in MathML. The type values that are used in the signatures are common mathematical types such as integer, rational, real, complex (such as found in the description of cn), or a name such as string or the name of a MathML constructor. Various collections of types such as anything, matrixtype are used from time to time. The type name mmlpresentation is used to represent any valid MathML presentation object and the name MathMLtype is used to describe the collection of all MathML types. The type algebraic is used for expressions constructed from one or more symbols through arithmetic operations and interval-type refers to the valid types of intervals as defined in chapter 4. The collection of types is not closed. Users writing their own definitions of new constructs may introduce new types.
The type of the resulting expression depends on the types of the operands, and the values of the MathML attributes.
For example, the definition of csymbol provides a signature which takes the form:
[definitionURL=definition]({string|mmlpresentation}) -> defined_symbol
This signature describes how a combination of various arguments produces an object which is a defined symbol.
The signature of more traditional mathematical functions such as exp is given as:
These signatures relate the mathematical type of applying the given function to arguments of a particular mathematical type.
A more complicated example is the definition of limit, which has the signature:
(algebraic,algebraic) -> tendsto
[ type=direction ](algebraic,algebraic) -> tendsto(direction)6 An Example with Complex Types
This example shows a typed version of the "inner product" operator. Conceptually, this operator takes an n-vector as the first argument, an n×m-matrix and yields an m-vector. The type in the example below can be described as "For all αtype, nZ, mZ. vector(n,α) × matrix(n,m,α) → vector(m,α)". It is a so-called "universal type", i.e. for all types and all natural numbers n and m, the inner product operator has the appropriate function type. Note that in this type system, types include typed variables themselves, for instance n and m are typed to be integers. Furthermore, note that types have a rich set of "type constructors" like the vector type constructor that takes a natural number n and a type α to construct the type of n-vectors with elements of type α .
<math>
<semantics>
<ci>inner-product</ci>
<annotation-xml definitionURL="deptypes-system.html" encoding="content-MathML">
<apply>
<csymbol definitionURL="deptypes-system.html#all_type"/>
<bvar>
<semantics>
<ci>&alpha;</ci>
<annotation-xml definitionURL="deptypes-system.html" encoding="content-MathML">
<csymbol definitionURL="deptypes-system.html#type_type"/>
</annotation-xml>
</semantics>
</bvar>
<bvar>
<semantics>
<ci>n</ci>
<annotation-xml definitionURL="deptypes-system.html" encoding="content-MathML">
<csymbol definitionURL="deptypes-system.html#int_type"/>
</annotation-xml>
</semantics>
</bvar>
<bvar>
<semantics>
<ci>m</ci>
<annotation-xml definitionURL="deptypes-system.html" encoding="content-MathML">
<csymbol definitionURL="deptypes-system.html#int_type"/>
</annotation-xml>
</semantics>
</bvar>
<apply>
<csymbol definitionURL="deptypes-system.html#fun_type"/>
<apply>
<csymbol definitionURL="deptypes-system.html#vector_type"/>
<cn>n</cn>
<cn>α</cn>
</apply>
<apply>
<csymbol definitionURL="deptypes-system.html#matrix_type"/>
<cn>n</cn>
<cn>m</cn>
<cn>&alpha;</cn>
</apply>
<apply>
<csymbol definitionURL="deptypes-system.html#vector_type"/>
<cn>m</cn>
<cn>alpha</cn>
</apply>
</apply>
</apply>
</annotation-xml>
</semantics>
</math>
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