index.html 49.7 KB

Raw Blame History Permalink

<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01//EN">
<!--
<!DOCTYPE html PUBLIC "W3C//DTD XHTML 1.1 plus MathML 2.0 plus SVG 1.1//EN"
"http://www.w3.org/2002/04/xhtml-math-svg/xhtml-math-svg-flat.dtd" [
<!ENTITY % MATHML.prefixed "IGNORE" >
]>
--><html>
  <head>
    <META http-equiv="Content-Type" content="text/html; charset=UTF-8">
    <title>Structured Types in MathML 2.0</title>
    <style type="text/css">
code           { font-family: monospace; }

div.constraint,
div.issue,
div.note,
div.notice     { margin-left: 2em; }

li p           { margin-top: 0.3em;
                 margin-bottom: 0.3em; }

div.exampleInner pre { margin-left: 1em;
                       margin-top: 0em; margin-bottom: 0em}
div.exampleOuter {border: 4px double gray;
                  margin: 0em; padding: 0em}
div.exampleInner { background-color: #d5dee3;
                   border-top-width: 4px;
                   border-top-style: double;
                   border-top-color: #d3d3d3;
                   border-bottom-width: 4px;
                   border-bottom-style: double;
                   border-bottom-color: #d3d3d3;
                   padding: 4px; margin: 0em }
div.exampleWrapper { margin: 4px }
div.exampleHeader { font-weight: bold;
                    margin: 4px}
</style>
    <link type="text/css" rel="stylesheet" href="http://www.w3.org/StyleSheets/TR/W3C-WG-NOTE.css">
  </head>
  <body>
    <div class="head">
      <p>
        <a href="http://www.w3.org/"><img width="72" height="48" alt="W3C" src="http://www.w3.org/Icons/w3c_home"></a>
      </p>
      <h1>
        <a id="title"></a>Structured Types in MathML 2.0</h1>
      <h2>
        <a id="w3c-doctype"></a>W3C Working Group Note 10 November 2003</h2>
      <dl>
        <dt>This version:</dt>
        <dd>
          <a href="http://www.w3.org/TR/2003/NOTE-mathml-types-20031110/">http://www.w3.org/TR/2003/NOTE-mathml-types-20031110/</a>
        </dd>
        <dt>Latest version:</dt>
        <dd>
          <a href="http://www.w3.org/TR/mathml-types/">http://www.w3.org/TR/mathml-types/</a>
        </dd>
        <dt>Previous version:</dt>
        <dd>
          <span>This is the first version of this Note.</span>
        </dd>
        <dt>Editors:</dt>
        <dd>Stan Devitt - Invited Expert, StratumTek</dd>
        <dd>Michael Kohlhase, DFKI</dd>
        <dd>Max Froumentin, W3C</dd>
      </dl>
      <p class="copyright">
        <a href="http://www.w3.org/Consortium/Legal/ipr-notice#Copyright">Copyright</a>&nbsp;&copy;&nbsp;2003&nbsp;<a href="http://www.w3.org/"><acronym title="World Wide Web Consortium">W3C</acronym></a><sup>&reg;</sup> (<a href="http://www.lcs.mit.edu/"><acronym title="Massachusetts Institute of Technology">MIT</acronym></a>, <a href="http://www.ercim.org/"><acronym title="European Research Consortium for Informatics and Mathematics">ERCIM</acronym></a>, <a href="http://www.keio.ac.jp/">Keio</a>), All Rights Reserved. W3C <a href="http://www.w3.org/Consortium/Legal/ipr-notice#Legal_Disclaimer">liability</a>, <a href="http://www.w3.org/Consortium/Legal/ipr-notice#W3C_Trademarks">trademark</a>, <a href="http://www.w3.org/Consortium/Legal/copyright-documents">document use</a> and <a href="http://www.w3.org/Consortium/Legal/copyright-software">software licensing</a> rules apply.</p>
    </div>
    <hr>
    <div>
      <h2>
        <a id="abstract"></a>Abstract</h2>
      <p>This Note discusses the facilities that are available in
         the MathML 2.0 Recommendation to facilitate the capturing of
         mathematical type information.  It demonstrates how a
         combination of these features can be systematically used to
         provide support for general mathematical types.</p>
    </div>
    <div>
      <h2>
        <a id="status"></a>Status of this Document</h2>
      <p>
        <em> This section describes the status of this document at the
		    time of its publication.
		    Other documents may supersede this document.
		    A list of current W3C publications and the
		    latest revision of this technical report can be found in the
		    <a href="http://www.w3.org/TR/">W3C technical reports index</a>
		    at http://www.w3.org/TR/.</em>
      </p>
      <p>This Note is a self-contained discussion of mathematical
         types in Content MathML. It contains non-normative
         interpretations of the MathML 2 Recommendation (2nd Edition)
         <a href="#MathML22e">[MathML22e]</a> and provides guidelines for the
         handling of advanced mathematical types using Content MathML.
         Please direct comments and report errors in this document to
         <a href="mailto:www-math@w3.org">www-math@w3.org</a>.</p>
      <p>This document has been produced by the W3C Math Working
	 Group as part of the <a href="http://www.w3.org/Math/">W3C
	 Math Activity</a> (<a href="http://www.w3.org/Math/Activity">Activity statement</a>).  The goals of the Working Group are
	 discussed in the <a href="http://www.w3.org/Math/Documents/Charter2001.html">
	 Working Group Charter</a>.  A list of <a href="http://www.w3.org/TR/2003/REC-MathML2-20031021/appendixi.html">participants
	 in the W3C Math Working Group</a> is available.</p>
      <p>Publication as a Working Group Note does not imply
	 endorsement by the W3C Membership. This is a draft document
	 and may be updated, replaced or obsoleted by other documents
	 at any time. It is inappropriate to cite this document as
	 other than work in progress. Patent disclosures relevant to
	 this Note may be found on the Math Working Group's <a href="http://www.w3.org/Math/Disclosures">patent disclosure
	 page</a>.</p>
    </div>
    <div class="toc">
      <h2>
        <a id="contents"></a>Table of Contents</h2>
      <p class="toc">1 <a href="#types_intro">Introduction</a>
        <br>
&nbsp;&nbsp;&nbsp;&nbsp;1.1 <a href="#goals">Goals</a>
        <br>
&nbsp;&nbsp;&nbsp;&nbsp;1.2 <a href="#overview">Overview</a>
        <br>
2 <a href="#typeattribute">The type attribute</a>
        <br>
3 <a href="#types-with-semantics">Advanced Typing</a>
        <br>
&nbsp;&nbsp;&nbsp;&nbsp;3.1 <a href="#semantics">The semantics Element</a>
        <br>
&nbsp;&nbsp;&nbsp;&nbsp;3.2 <a href="#xmltypes">Some Encodings for Structured Type Objects</a>
        <br>
&nbsp;&nbsp;&nbsp;&nbsp;3.3 <a href="#assoc-types">Associating Structured Types with MathML Objects.</a>
        <br>
&nbsp;&nbsp;&nbsp;&nbsp;3.4 <a href="#types-bvar">Structured Types and Bound Variables.</a>
        <br>
4 <a href="#OpenMathSection">
            Related Work: Types in OpenMath</a>
        <br>
&nbsp;&nbsp;&nbsp;&nbsp;4.1 <a href="#OpenMath-rep">Representing and Associating Types in OpenMath</a>
        <br>
&nbsp;&nbsp;&nbsp;&nbsp;4.2 <a href="#OpenMath-STS">OpenMath's Small Type System</a>
        <br>
5 <a href="#appendixCexamples">Types as used in appendix C of MathML 2</a>
        <br>
6 <a href="#sts-1">An Example with Complex Types</a>
        <br>
      </p>
      <h3>
        <a id="appendices"></a>Appendix</h3>
      <p class="toc">A <a href="#N400446">Bibliography</a>
        <br>
      </p>
    </div>
    <hr>
    <div class="body">
      <div class="div1">
        <h2>
          <a id="types_intro"></a>1 Introduction</h2>
        <div class="div2">
          <h3>
            <a id="goals"></a>1.1 Goals</h3>
          <p>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:
	</p>
          <ul>
            <li>
              <p>clarify the role of the <code>type</code> attribute in MathML,</p>
            </li>
            <li>
              <p>demonstrate in detail how to attach more advanced type information
	      to a MathML object,</p>
            </li>
            <li>
              <p>illustrate this technique with examples using
                  various type systems, including the types discussed
                  in <a href="http://www.w3.org/TR/2003/REC-MathML2-20031021/appendixc.html">Appendix
                  C (Content Element Definitions)</a> of the MathML
                  2.0 Recommendation, the type system used by OpenMath
                  <a href="#OpenMath">[OpenMath]</a>, and an example of a more
                  complicated type system.</p>
            </li>
          </ul>
        </div>
        <div class="div2">
          <h3>
            <a id="overview"></a>1.2 Overview</h3>
          <p>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.</p>
          <p>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.</p>
          <p>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.</p>
          <p>Content MathML, as specified in <a href="http://www.w3.org/TR/2003/REC-MathML2-20031021/chapter4.html">Chapter
            4</a> of the MathML 2 Recommendation defines an
            attribute called <code>type</code>, 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:</p>
          <div class="exampleInner">
            <pre>&lt;math&gt;
  &lt;apply&gt;
    &lt;tendsto type="above"/&gt;
    &lt;ci&gt;x&lt;/ci&gt;
    &lt;cn&gt;0&lt;/cn&gt;
  &lt;/apply&gt;
&lt;/math&gt;</pre>
          </div>
          <p>In this example, the <code>type</code> attribute does not indicate
	    the domain of the <code>tendsto</code> 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 <code>tendsto</code> operator.</p>
          <p>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 <code>type</code> attribute is open-ended, a
            specification of all possible object types would
            necessitate defining an attribute value syntax, e.g.
            "complex &rarr; pair(real,real)". However,
            this would add considerable complexity to the design of
            MathML implementations, as this syntax would require
            writing an specific parser.</p>
          <p>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.</p>
          <p>The next section discusses the <code>type</code>
            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.</p>
        </div>
      </div>
      <div class="div1">
        <h2>
          <a id="typeattribute"></a>2 The type attribute</h2>
        <p>In Content MathML, The <code>type</code> attribute is used to specify the basic type of a limited number of primitive objects.  These include:</p>
        <dl>
          <dt class="label">
            <a id="cn_item"></a>cn</dt>
          <dd>
            <p>The <code>cn</code> element is used to specify actual
                  numerical quantities. The attribute <code>type</code>
                  indicates what type of number is being represented
                  such as integer, rational, real or complex, </p>
            <p>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.</p>
          </dd>
          <dt class="label">
            <a id="ci_item"></a>ci</dt>
          <dd>
            <p>The <code>ci</code> element is used to name mathematical objects.  It
    uses the <code>type</code> attribute primarily to indicate the kind of
    objects that are being represented.</p>
          </dd>
          <dt class="label">
            <a id="declare_item"></a>declare</dt>
          <dd>
            <p>The <code>declare</code> element can be used to
                  establish a default type value for associating a
                  type with other MathML elements such as the
                  <code>ci</code> element. Either the <code>type</code>
                  attribute or the contents of the <code>declare</code>
                  element can be used to specify a type.</p>
          </dd>
          <dt class="label">
            <a id="set_item"></a>set</dt>
          <dd>
            <p>The <code>set</code> element is the container element
		 that constructs a set of elements.  The
		 <code>type</code> attribute is used on the <code>set</code>
		 element to clarify the kind of set that is
		 represented.  For example, a set may be a
		 multiset.</p>
          </dd>
          <dt class="label">
            <a id="tendsto_item"></a>tendsto</dt>
          <dd>
            <p>The <code>tendsto</code> element is used to express
		 the relation that a quantity is tending to a
		 specified value.  The <code>type</code> attribute is
		 used on the <code>tendsto</code> element to indicate the
		 direction of limits.</p>
          </dd>
        </dl>
        <p>The MathML specification does not restrict the values of
         the type attribute in any way. Indeed the attribute content
         is defined as <b>CDATA</b> 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:</p>
        <ol class="1">
          <li>
            <p>There are MathML elements that may require detailed type
	      specifications but cannot have a <code>type</code> attribute.</p>
          </li>
          <li>
            <p>The <code>type</code> 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.</p>
          </li>
          <li>
            <p>Embedding detailed type information in the value of
               the <code>type</code> 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.</p>
          </li>
          <li>
            <p>Mathematical types are mathematical objects
               themselves and thus require a rich structure model, such
               as that of Content MathML, to describe them</p>
          </li>
        </ol>
      </div>
      <div class="div1">
        <h2>
          <a id="types-with-semantics"></a>3 Advanced Typing</h2>
        <p>In order to deal with more sophisticated typing systems,
	two key issues must be solved:</p>
        <ol class="1">
          <li>
            <p>Specify a way to encode non-trivial mathematical type objects.</p>
          </li>
          <li>
            <p>Determine a method to associate the type objects with the corresponding MathML object.</p>
          </li>
        </ol>
        <p>One simple way deal with the second issue is to use
	 MathML's <code>semantics</code> 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 <code>annotation-xml</code>
	 and <code>annotation</code> elements.</p>
        <p>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
	 <a href="#STS">[STS]</a>. A significant part of Appendix C of
	 MathML itself deals with the issues of types and how they are
	 related. Fortunately, the <code>semantics</code> element is
	 designed to support alternative notations, and thus allows
	 using the typing systems mentioned.</p>
        <p>The following section discusses in detail how the
         <code>semantics</code> element can be used to describe types.</p>
        <div class="div2">
          <h3>
            <a id="semantics"></a>3.1 The <code>semantics</code> Element</h3>
          <p>The <code>semantics</code> element is designed to group
            together various kinds of information related to a
            particular mathematical object.  For example,
            <code>semantics</code> is often used to provide both a Content MathML
            and a Presentation MathML representation of an object.</p>
          <p>The <code>semantics</code> element is the container element
            for the MathML expression, together with its semantic
            mappings. <code>semantics</code> 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
            <code>annotation</code> or <code>annotation-xml</code> elements.
            Each of these elements can contain a
            <code>definitionURL</code> and a <code>encoding</code>
            attribute.  Those attributes can be used to clarify the
            meaning of the content of a particular
            <code>annotation-xml</code> element, and the manner in which
            it is encoded, respectively.</p>
          <ul>
            <li>
              <p>The <code>annotation</code> 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 <code>annotation</code> element can contain an attribute
                  called "encoding", defining the format in use.
                  Note that the content model of <code>annotation</code>
                  is <b>PCDATA</b>, so care must be taken that the
                  particular encoding does not conflict with XML
                  parsing rules.</p>
            </li>
            <li>
              <p>The <code>annotation-xml</code> 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 <code>semantics</code> (or
                  vice versa).  <code>annotation-xml</code> can contain an
                  <code>encoding</code> attribute specifying the
                  format used.</p>
            </li>
          </ul>
          <p>By replacing a simple mathematical expression by a
            <code>semantics</code> 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:</p>
          <div class="exampleInner">
            <pre>
&lt;semantics&gt;
  &lt;apply&gt;&lt;divide/&gt;&lt;cn&gt;123&lt;/cn&gt;&lt;cn&gt;456&lt;/cn&gt;&lt;/apply&gt;
  &lt;annotation encoding="Mathematica"&gt;N[123/456, 39]&lt;/annotation&gt;
  &lt;annotation encoding="TeX"&gt;
    $0.269736842105263157894736842105263157894\ldots$
  &lt;/annotation&gt;
  &lt;annotation encoding="Maple"&gt;evalf(123/456, 39);&lt;/annotation&gt;
  &lt;annotation-xml encoding="MathML-Presentation"&gt;
    &lt;mrow&gt;
      &lt;mn&gt; 0.269736842105263157894 &lt;/mn&gt;
      &lt;mover accent='true'&gt;
      &lt;mn&gt; 736842105263157894 &lt;/mn&gt;
      &lt;mo&gt; &amp;OverBar; &lt;/mo&gt;
      &lt;/mover&gt;
    &lt;/mrow&gt;
  &lt;/annotation-xml&gt;
  &lt;annotation-xml encoding="OpenMath"&gt;
    &lt;OMA xmlns="http://www.openmath.org/OpenMath"&gt;
      &lt;OMS cd="arith1" name="divide"/&gt;
      &lt;OMI&gt;123&lt;/OMI&gt;
      &lt;OMI&gt;456&lt;/OMI&gt;
    &lt;/OMA&gt;
  &lt;/annotation-xml&gt;
&lt;/semantics&gt;</pre>
          </div>
          <p>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</p>
          <p>The next section discusses some of the possible type
            encodings supported by this approach.</p>
        </div>
        <div class="div2">
          <h3>
            <a id="xmltypes"></a>3.2 Some Encodings for Structured Type Objects</h3>
          <p>Some 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.</p>
          <p>For example, the function type indicating a function
	    that maps integers to natural numbers (<em>Z</em>
	    &rarr; <em>R</em>) is sometimes written as:</p>
          <div class="exampleInner">
            <pre>(integer) --&gt; (naturalnumber) </pre>
          </div>
          <p>(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</p>
          <div class="exampleInner">
            <pre>&lt;apply&gt;
  &lt;csymbol definitionURL="types.html#funtype"/&gt;
  &lt;csymbol definitionURL="types.html#int_type"/&gt;
  &lt;csymbol definitionURL="types.html#nat_type"/&gt;
&lt;/apply&gt;</pre>
          </div>
          <p>
            <span>where we assume a document called <code>types.html</code>,
	    which specifies the type system employed and provides definitions
	    for the symbols    <em>Z</em>, &rarr;, and <em>N</em>.

</span>
	  The type object
    <em>Z</em> &rarr; <em>R</em>

	    is obtained by  applying  the function type constructor
&rarr;

to the set
	<em>Z</em>

of integers and the set
	<em>N</em>

of natural numbers.  </p>
          <p>An alternative representation of this function type that makes
          more direct use of existing  content MathML elements is:</p>
          <div class="exampleInner">
            <pre>&lt;apply&gt;
  &lt;csymbol definitionURL="types.html#funtype"/&gt;
  &lt;integers/&gt;
  &lt;naturalnumbers/&gt;
&lt;/apply&gt;</pre>
          </div>
          <p>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
            <code>type</code> attribute (barring the use of URIs in the
            attribute).</p>
        </div>
        <div class="div2">
          <h3>
            <a id="assoc-types"></a>3.3 Associating Structured Types with MathML Objects.</h3>
          <p> The <code>semantics</code> element can be used to directly associate
     structured types (as introduced in the previous section)  with a particular MathML object.
     For example:
     </p>
          <div class="exampleInner">
            <pre>&lt;semantics&gt;
  &lt;ci&gt;F&lt;/ci&gt;
  &lt;annotation encoding="ASCII"
	      definitionURL="http://www.example.org/MathML-2.0-appendixC"&gt;
    (integer) --&gt; (naturalnumber)
  &lt;annotation&gt;
  &lt;annotation-xml encoding="MathMLType" definitionURL="types.html"&gt;
    &lt;apply&gt;
      &lt;csymbol definitionURL="types.html#funtype"/&gt;
      &lt;integers/&gt;
      &lt;naturalnumbers/&gt;
    &lt;/apply&gt;
  &lt;annotation-xml&gt;
&lt;/semantics&gt;</pre>
          </div>
          <p>
            <span>
		 The second child element of the <code>semantics</code>
		 element is a <code>annotation</code> element that
		 contains type information in textual format.  The
		 third child element is an <code>annotation-xml</code>
		 element that contains the XML representation of the
		 type, using Content MathML markup.</span>
          </p>
          <p> The <code>definitionURL</code> attribute on the
            <code>annotation-xml</code> and <code>annotation</code> elements
            are used here to specify the nature of the information
            provided within the element (in this case, type
            information).  The <code>encoding</code> attribute on the
            <code>annotation-xml</code> 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.</p>
          <p>In summary the MathML specification allows using the
            <code>semantics</code> element as a general annotation device
            for MathML objects, where the <code>definitionURL</code>
            attribute specifies the relation of the annotation to the
            first child of the <code>semantics</code> 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 <em>X<sub>Z</sub></em>
            represented using Content MathML markup.

	(see <a href="#OpenMathSection"><b>4
            Related Work: Types in OpenMath</b></a> for more details).</p>
          <div class="exampleInner">
            <pre>&lt;semantics&gt;
  &lt;semantics id="typed-var"&gt;
    &lt;ci&gt;X&lt;/ci&gt;
    &lt;annotation-xml definitionURL="type.html" encoding="MathMLType"&gt;
      &lt;integers/&gt;
    &lt;/annotation-xml&gt;
  &lt;/semantics&gt;
  &lt;annotation-xml encoding="OpenMath"&gt;
    &lt;OMOBJ xmlns="http://www.openmath.org/OpenMath"&gt;
      &lt;OMATTR  xlink:href="typed-var"&gt;
	&lt;OMATP&gt;
	  &lt;OMS cd="sts" name="type"/&gt;
	  &lt;OMS cd="setname1" name="integers"/&gt;
	&lt;/OMATP&gt;
	&lt;OMV name="X"/&gt;
      &lt;/OMATTR&gt;
    &lt;/OMOBJ&gt;
  &lt;/annotation-xml&gt;
&lt;/semantics&gt;</pre>
          </div>
          <p>To make the correspondence clear, the parallel markup
            uses cross-references, as described in section 5.3.4 of
            the MathML2 specification.</p>
        </div>
        <div class="div2">
          <h3>
            <a id="types-bvar"></a>3.4 Structured Types and Bound Variables.</h3>
          <p>A natural place to annotate types in formulas is in the declaration of
       bound variables. For example:
     </p>
          <div class="exampleInner">
            <pre>&lt;math&gt;
  &lt;apply&gt;
    &lt;forall/&gt;
    &lt;bvar id="bvF"&gt;
      &lt;semantics&gt;
	&lt;ci&gt;F&lt;/ci&gt;
	&lt;annotation-xml encoding="content-MathML"
	                definitionURL="types.html"&gt;
	  &lt;apply&gt;
	    &lt;csymbol definitionURL="types.html#funtype"/&gt;
	    &lt;csymbol definitionURL="types.html#int_type"/&gt;
	    &lt;csymbol definitionURL="types.html#nat_type"/&gt;
	  &lt;/apply&gt;
	&lt;/annotation-xml&gt;
	&lt;annotation encoding="ASCII" definitionURL="type"&gt;
	  integer --&gt; nat
	&lt;/annotation&gt;
      &lt;/semantics&gt;
    &lt;/bvar&gt;
    &lt;bvar id="bvx"&gt;
      &lt;semantics&gt;
	&lt;ci&gt;x&lt;/ci&gt;
	&lt;annotation-xml encoding="content-MathML"&gt;
	  &lt;csymbol definitionURL="types.html#int_type"/&gt;
	&lt;/annotation-xml&gt;
	&lt;annotation encoding="ASCII" definitionURL="type"&gt;
	  integer
	&lt;/annotation&gt;
      &lt;/semantics&gt;
    &lt;/bvar&gt;
    &lt;apply&gt;&lt;geq/&gt;
      &lt;apply&gt;&lt;ci definitionURL="bvF"&gt;F&lt;/ci&gt;
	&lt;ci definitionURL="bvx"&gt;x&lt;/ci&gt;
      &lt;/apply&gt;
      &lt;cn&gt;0&lt;/cn&gt;
    &lt;/apply&gt;
  &lt;/apply&gt;
&lt;/math&gt;</pre>
          </div>
          <p>Here the bound variables
<em>F</em>

and
<em>x</em>

       are annotated with type information by using the
       <code>semantics</code> element. <span>The correspondence between
       the declaring occurrence of the variable and the bound
       occurrences are made explicit by the use of the
       <code>definitionURL</code> attribute, which points to the
       respective <code>bvar</code> element (see <a href="#MathMLBVar">[MathMLBVar]</a> for a discussion of this
       technique).</span>
          </p>
          <p>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.</p>
          <p>A related way to express the information in the example above
      that does not use the <code>semantics</code> element in
      <code>bvar</code> is:</p>
          <div class="exampleInner">
            <pre>&lt;math&gt;
  &lt;apply&gt;
    &lt;forall/&gt;
    &lt;bvar&gt;&lt;ci&gt;F&lt;/ci&gt;&lt;/bvar&gt;
    &lt;condition&gt;
      &lt;apply&gt;
	&lt;csymbol definitionURL="types.html#type_of"/&gt;
	&lt;ci&gt;F&lt;/ci&gt;
	&lt;apply&gt;
	  &lt;csymbol definitionURL="types.html#funtype"/&gt;
	  &lt;csymbol definitionURL="types.html#int_type"/&gt;
	  &lt;csymbol definitionURL="types.html#nat_type"/&gt;
	&lt;/apply&gt;
      &lt;/apply&gt;
    &lt;/condition&gt;
    &lt;bvar&gt;&lt;ci&gt;x&lt;/ci&gt;&lt;/bvar&gt;
    &lt;condition&gt;
      &lt;apply&gt;
	&lt;csymbol definitionURL="types.html#type_of"/&gt;
	&lt;ci&gt;x&lt;/ci&gt;
        &lt;csymbol definitionURL="types.html#int_type"/&gt;
      &lt;/apply&gt;
    &lt;/condition&gt;
    &lt;apply&gt;&lt;geq/&gt;&lt;apply&gt;&lt;ci&gt;F&lt;/ci&gt;&lt;ci&gt;x&lt;/ci&gt;&lt;/apply&gt;&lt;cn&gt;0&lt;/cn&gt;&lt;/apply&gt;
  &lt;/apply&gt;
&lt;/math&gt;</pre>
          </div>
          <p>Here, the <code>condition</code> element is used to express the type condition "such
	    that
<em>F</em>

has type
<em>Z</em>
&rarr;
<em>R</em>".


The transformation from the first to the second representation is a
well-known technique in typed logics called
<b>relativization</b><a href="#Oberschelp">[Oberschelp]</a>, 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.</p>
        </div>
      </div>
      <div class="div1">
        <h2>
          <a id="OpenMathSection"></a>4
            <span>Related Work:</span> Types in OpenMath</h2>
        <p>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 <code>csymbol</code>-like mechanism
         for representing symbols.</p>
        <p>In this section we briefly compare the representation of
         structured types in content MathML and in OpenMath.</p>
        <div class="div2">
          <h3>
            <a id="OpenMath-rep"></a>4.1 Representing and Associating Types in OpenMath</h3>
          <p>The following representation, which is the counterpart of the example above,
	    shows how types are represented in OpenMath:</p>
          <div class="exampleInner">
            <pre>
&lt;OMOBJ&gt;
  &lt;OMBIND&gt;
    &lt;OMS cd="quant1" name="forall"/&gt;
    &lt;OMBVAR&gt;
      &lt;OMATTR&gt;
      &lt;OMATP&gt;
        &lt;OMS cd="types" name="type"/&gt;
        &lt;OMA&gt;
          &lt;OMS cd="types" name="funtype"/&gt;
          &lt;OMS cd="types" name="int_type"/&gt;
          &lt;OMS cd="types" name="nat_type"/&gt;
        &lt;/OMA&gt;
      &lt;/OMATP&gt;
      &lt;OMV name="F"/&gt;
    &lt;/OMATTR&gt;
    &lt;OMATTR&gt;
      &lt;OMATP&gt;
        &lt;OMS cd="types" name="type"/&gt;
        &lt;OMS cd="types" name="int_type"/&gt;
      &lt;/OMATP&gt;
      &lt;OMV name="x"/&gt;
    &lt;/OMATTR&gt;
  &lt;/OMBVAR&gt;
  &lt;OMA&gt;
    &lt;OMS cd="relation1" name="geq"/&gt;
    &lt;OMA&gt;&lt;OMV name="F"/&gt;&lt;OMV name="x"/&gt;&lt;/OMA&gt;
    &lt;OMI&gt;0&lt;/OMI&gt;
  &lt;/OMA&gt;
  &lt;/OMBIND&gt;
&lt;/OMOBJ&gt;</pre>
          </div>
          <p>OpenMath uses the <code>OMBIND</code> element for binding
            objects while MathML uses the <code>apply</code> element with
            <code>bvar</code> child (which corresponds to the OpenMath
            element <code>OMBVAR</code>, except that the latter can hold
            more than one variable). OpenMath uses the <code>OMA</code>
            element for applications, the <code>OMS</code> element instead
            of MathML's <code>csymbol</code>, and the <code>OMV</code> element
            for variables, instead of <code>ci</code>. This markup
            corresponds directly to Content MathML.</p>
          <p>The main difference to the Content MathML example above
            is the treatment of annotations. Instead of the MathML
            <code>semantics</code> element, OpenMath uses the
            <code>OMATTR</code> element. Its first child is an
            <code>OMATP</code> 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 <code>OMS</code> element whose
            <code>name</code> attribute has the value <code>type</code>
            specifies that the element following it is a type. The
            second child of the <code>OMATTR</code> element is the object
            to which the information in the first one is attached.</p>
          <p>The representation of structured types proposed in
            this Note makes Content MathML as expressive as OpenMath for
            types. The feature symbols in OpenMath <code>OMATP</code>
            elements directly correspond to the value of the
            <code>definitionURL</code> attribute on the
            <code>annotation-xml</code> and <code>annotation</code> elements
            in exactly the same way the <code>definitionURL</code>
            attribute on a <code>csymbol</code> element corresponds to an
            OpenMath <code>OMS</code> element. MathML even slightly
            generalizes OpenMath, which only allows OpenMath
            representations as feature values. MathML allows arbitrary
            XML representations in <code>annotation-xml</code> elements,
            whose format can be specified in the <code>encoding</code>
            attribute. The equivalent of the <code>annotation</code>
            element can be used by the OpenMath <code>OMSTR</code> element
            as a feature value.</p>
        </div>
        <div class="div2">
          <h3>
            <a id="OpenMath-STS"></a>4.2 OpenMath's Small Type System</h3>
          <p>OpenMath comes with a dedicated type system, the "small type
	    system (STS)"
               <a href="#STS">[STS]</a>). 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
	  <a href="http://www.w3.org/TR/2003/REC-MathML2-20031021/appendixb.html"><cite>
	    Appendix B</cite></a> of the MathML 2 specification.
	</p>
          <p>The symbols supplied by the STS system can be found in the
	  <a href="http://www.openmath.org/cd/sts.html"><cite>sts</cite></a>
	  OpenMath Content Dictionary; the symbols corresponding to the values
	  used in the <code>type</code> attribute discussed in
	  <a href="#typeattribute"><b>2 The type attribute</b></a> can be found in the
	  <a href="http://www.openmath.org/cd/mathmltypes.html"><cite>
	    mathmltypes</cite></a> Content Dictionary. Using these
	  Content Dictionaries as targets for the <code>definitionURL</code> attribute
	  makes the following three representations equivalent:  </p>
          <div class="exampleInner">
            <pre>&lt;ci type="integer"&gt;&amp;phi;&lt;/ci&gt;

&lt;semantics&gt;
  &lt;ci&gt;&amp;phi;&lt;/ci&gt;
  &lt;annotation-xml encoding="Content-MathML"
    definitionURL="http://www.openmath.org/standard/sts.pdf"&gt;
    &lt;csymbol definitionURL="http://www.openmath.org/cd/mathmltypes.html#complex_cartesian_type"/&gt;
  &lt;/annotation-xml&gt;
&lt;/semantics&gt;

&lt;semantics&gt;
  &lt;ci&gt;&amp;phi;&lt;/ci&gt;
  &lt;annotation-xml encoding="OpenMath"
    definitionURL="http://www.openmath.org/standard/sts.pdf"&gt;
    &lt;OMS xmlns="http://www.openmath.org/OpenMath" cd="mathmltypes" name="complex_cartesian_type"/&gt;
  &lt;/annotation-xml&gt;
&lt;/semantics&gt;</pre>
          </div>
        </div>
      </div>
      <div class="div1">
        <h2>
          <a id="appendixCexamples"></a>5 Types as used in appendix C of MathML 2</h2>
        <p>The primary place where mathematical types arise in MathML is in the notation of the
    <em>signature</em> of the various mathematical objects defined in appendix C:</p>
        <dl>
          <dt class="label">signature</dt>
          <dd>
            <p>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.</p>
            <p>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 <code>apply</code>. Modifiers modify the attributes of an
  existing object. For example, a <em>symbol</em> might become a
  <em>symbol of type vector</em>.</p>
            <p>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:
</p>
            <div class="exampleInner">
              <pre>[&lt;attribute name&gt;=&lt;attribute-value&gt;]( &lt;list of argument types&gt; )
--&gt; &lt;mathematical result type&gt;(&lt;mathematical subtype&gt;)</pre>
            </div>
            <p>The MMLattributes, if any, appear in the form
   <code>&lt;name&gt;=&lt;value&gt;</code>. 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.</p>
            <p>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
   <code>&lt;elementname&gt;=&lt;type&gt;</code>
     in a manner analogous for that used for attribute values. For example,
     if the argument is named (e.g. <code>bvar</code>) then it is
     represented in the signature by an equation as in:
     </p>
            <div class="exampleInner">
              <pre>[&lt;attribute name&gt;=&lt;attributevalue&gt;]( bvar=symbol,&lt;argument list&gt; ) --&gt;
   &lt;mathematical result type&gt;(&lt;mathematical subtype&gt;)</pre>
            </div>
            <p>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 <code>cn</code>),
    or a name such as string or the name of a MathML constructor.
    Various collections of types such as <em>anything</em>, <em>matrixtype</em>
    are used from time to time. The type name <em>mmlpresentation</em>
    is used to represent any valid MathML presentation object and the name
    <em>MathMLtype</em> is used to describe the collection of all MathML types.
    The type <em>algebraic</em> is used for  expressions constructed
    from one or more symbols through arithmetic operations and <em>interval-type</em>
    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.
  </p>
            <p>The type of the resulting expression depends on the types of the
    operands, and the values of the MathML attributes.</p>
          </dd>
        </dl>
        <p>For example, the definition of <code>csymbol</code> provides a
      signature which takes the form:</p>
        <div class="exampleInner">
          <pre>[definitionURL=definition]({string|mmlpresentation}) -&gt; defined_symbol</pre>
        </div>
        <p>This signature describes how a combination of various
      arguments produces an object which is a defined symbol.</p>
        <p>The signature of more traditional mathematical functions such as <code>exp</code> is given as:</p>
        <div class="exampleInner">
          <pre>real -&gt; real</pre>
        </div>
        <div class="exampleInner">
          <pre>complex -&gt; complex</pre>
        </div>
        <p>These signatures relate the mathematical type of applying the
      given function to arguments of a particular mathematical type.</p>
        <p>A more complicated example is the definition of limit, which has the signature:</p>
        <div class="exampleInner">
          <pre> (algebraic,algebraic) -&gt; tendsto </pre>
        </div>
        <div class="exampleInner">
          <pre> [ type=direction ](algebraic,algebraic) -&gt; tendsto(direction) </pre>
        </div>
      </div>
      <div class="div1">
        <h2>
          <a id="sts-1"></a>6 An Example with Complex Types</h2>
        <p>This example shows a typed version of the
      "inner product" operator. Conceptually, this operator takes an

<em>n</em>-vector as the first argument, an

<em>n</em>&times;<em>m</em>-matrix and yields an

<em>m</em>-vector.
      The type in the example below can be described as
      "For all &alpha;<sub>type</sub>, n<sub>Z</sub>, m<sub>Z</sub>.
vector(<em>n</em>,&alpha;)
&times;
matrix(<em>n</em>,<em>m</em>,&alpha;)
&rarr;
vector(<em>m</em>,&alpha;)".

      It is a so-called "universal type", i.e. for all types

and all natural numbers
<em>n</em>

and

<em>m</em>,
the inner
      product operator has the appropriate function type. Note that in this type system,
      types include typed variables themselves, for instance
<em>n</em>

and
<em>m</em>

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
<em>n</em>

and a type
&alpha;


to construct the type of
<em>n</em>-vectors

with elements of type
&alpha;

.</p>
        <div class="exampleInner">
          <pre>&lt;math&gt;
  &lt;semantics&gt;
    &lt;ci&gt;inner-product&lt;/ci&gt;
    &lt;annotation-xml definitionURL="deptypes-system.html" encoding="content-MathML"&gt;
      &lt;apply&gt;
        &lt;csymbol definitionURL="deptypes-system.html#all_type"/&gt;
        &lt;bvar&gt;
          &lt;semantics&gt;
            &lt;ci&gt;&amp;amp;alpha;&lt;/ci&gt;
            &lt;annotation-xml definitionURL="deptypes-system.html" encoding="content-MathML"&gt;
              &lt;csymbol definitionURL="deptypes-system.html#type_type"/&gt;
            &lt;/annotation-xml&gt;
          &lt;/semantics&gt;
        &lt;/bvar&gt;
        &lt;bvar&gt;
          &lt;semantics&gt;
            &lt;ci&gt;n&lt;/ci&gt;
            &lt;annotation-xml definitionURL="deptypes-system.html" encoding="content-MathML"&gt;
              &lt;csymbol definitionURL="deptypes-system.html#int_type"/&gt;
            &lt;/annotation-xml&gt;
          &lt;/semantics&gt;
        &lt;/bvar&gt;
        &lt;bvar&gt;
          &lt;semantics&gt;
            &lt;ci&gt;m&lt;/ci&gt;
            &lt;annotation-xml definitionURL="deptypes-system.html" encoding="content-MathML"&gt;
              &lt;csymbol definitionURL="deptypes-system.html#int_type"/&gt;
            &lt;/annotation-xml&gt;
          &lt;/semantics&gt;
        &lt;/bvar&gt;
        &lt;apply&gt;
          &lt;csymbol definitionURL="deptypes-system.html#fun_type"/&gt;
          &lt;apply&gt;
            &lt;csymbol definitionURL="deptypes-system.html#vector_type"/&gt;
            &lt;cn&gt;n&lt;/cn&gt;
            &lt;cn&gt;&amp;alpha;&lt;/cn&gt;
          &lt;/apply&gt;
          &lt;apply&gt;
            &lt;csymbol definitionURL="deptypes-system.html#matrix_type"/&gt;
            &lt;cn&gt;n&lt;/cn&gt;
            &lt;cn&gt;m&lt;/cn&gt;
            &lt;cn&gt;&amp;amp;alpha;&lt;/cn&gt;
          &lt;/apply&gt;
          &lt;apply&gt;
            &lt;csymbol definitionURL="deptypes-system.html#vector_type"/&gt;
            &lt;cn&gt;m&lt;/cn&gt;
            &lt;cn&gt;alpha&lt;/cn&gt;
          &lt;/apply&gt;
        &lt;/apply&gt;
      &lt;/apply&gt;
    &lt;/annotation-xml&gt;
  &lt;/semantics&gt;
&lt;/math&gt;
</pre>
        </div>
      </div>
    </div>
    <div class="back">
      <div class="div1">
        <h2>
          <a id="N400446"></a>A Bibliography</h2>
        <dl>
          <dt class="label">
            <a id="Oberschelp"></a>Oberschelp</dt>
          <dd>Arnold Oberschelp, Untersuchungen zur mehrsortigen Quantorenlogik,
  Mathematische Annalen 145, pp. 297- 333, 1962.
  </dd>
          <dt class="label">
            <a id="MathMLBVar"></a>MathMLBVar</dt>
          <dd>
   Michael Kohlhase,  Stan Devitt;
   <em>Bound Variables in MathML</em>,  W3C Note 2003.
   (<a href="http://www.w3.org/TR/2003/NOTE-mathml-bvar-20031110/">http://www.w3.org/TR/2003/NOTE-mathml-bvar-20031110/</a>)
 </dd>
          <dt class="label">
            <a id="MathML22e"></a>MathML22e</dt>
          <dd>David Carlisle, Patrick Ion, Robert Miner, Nico Poppelier,
   <em>Mathematical Markup Language (MathML) Version 2.0 (2nd Edition)</em>
   W3C Recommendation 21 October 2003
   (<a href="http://www.w3.org/TR/2003/REC-MathML2-20031021/">http://www.w3.org/TR/2003/REC-MathML2-20031021/</a>)
 </dd>
          <dt class="label">
            <a id="STS"></a>STS</dt>
          <dd> James H. Davenport,
   <em>A Small OpenMath Type System.</em>
     In ACM SIGSAM Bulletin, volume 34, number 2, pages 16-21, 2000.
     (see also <a href="http://www.openmath.org/standard/sts.pdf">http://www.openmath.org/standard/sts.pdf</a>)
   </dd>
          <dt class="label">
            <a id="OpenMath"></a>OpenMath</dt>
          <dd>O. Caprotti, D. P. Carlisle, A. M. Cohen (editors),
   <em>The OpenMath Standard.</em>
   February 2000 (<a href="http://www.openmath.org/standard"></a>)
   </dd>
        </dl>
      </div>
    </div>
  </body>
</html>