1 導入
Introduction
1.1 目標
Goals
このメモの目標は, MathMLにおける既存の構造が, 式の様々な部分に対して詳細な数学型情報を結び付けるために, どのように利用できるか論証します. この文書は次のことを試みています.
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:
-
MathMLにおけるtype属性の役割を明確化しようとしています.
clarify the role of the type attribute in MathML,
-
どのようにMathMLオブジェクトにより進歩的な型情報を結び付けるか詳細に論証しようとしています.
demonstrate in detail how to attach more advanced type information
to a MathML object,
-
MathML 2.0勧告の付録C (コンテント要素の定義)で論じられている型情報, OpenMath[OpenMath]で使われている型システム, より複雑な型システムの例を含む, 様々な型システムを利用した例と一緒に型情報技術を説明しようとしています.
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.
1.2 概要
Overview
MathMLは, 数学の構造も内容も両方コード化することができる数学表記を説明するためのXMLの応用です. 小中学校から大学の初等水準までに広く由来する数学の語彙に基いている一方, 数々の方法で拡張可能です. このメモの主要な目的は, 詳細な数学型情報と個々の式や式の部分部分を結び付けるために, どのようにこれらの仕組みが利用できるかを示すことです.
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は, たくさんの役割を持っています. 著者は, その目的に応じて数学事象の詳細な視覚的な表現, 事象のより抽象的な数学の説明, または両方を選んでもよいです. MathMLの内容の複数の表現が利用可能で, 視覚的, 聴覚的なものなどが利用でき, 著者は, 広範囲にわたる種類の追加情報をそれらの数式に付け加えることができます.
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.
コンテントMathMは, MathML 2勧告の第4章で指定しているように, typeと呼ばれる属性を定義しています. この属性は, 属性の中身として, "real", "integer", "complex-cartesian"といった単純な値を指定することを著者に認めた, 数学型情報への限られた対応を提供します. このような単純な構造は, 複雑な型情報を指定するには十分ではなく, 特に, 属性の利用は, 利用したいであろう要素全てで認められてる訳ではないです. さらに, 他の課題が次の例で表現されています.
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>
この例では, type属性は, tendsto要素の定義域を示さず, むしろ極限は上から近付くという事実を示しています. この属性は, 結果としてtendsto演算子の定義域を指定するのに利用できません.
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.
現在の手法が問題のある他の状況としては, 誰かがより複雑な型情報, 例えば, 定数の組を生じる複素数の関数の型情報を必要としている状況があります. たとえ, type属性の中身が拡張可能であったとしても, 可能性のある全てのオブジェクトの型情報に対する仕様書は, 例えば, "complex → pair(real,real)"といった属性値の構文を定義することを必要とするでしょう. ただし, このことは, 構文が特定の処理プログラムを必要とするであろうことから, MathMLの実装を設計する際に考えられる複雑さを増加させるでしょう.
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.
それでも, 数学の正式な面や電算上の面の現代的な取り扱いはだんだんと精巧な型システムを利用していることから, MathMLの複雑な構造化された型情報を表現する差し迫った必要性があります. ただし, 上の例のような構造化されたオブジェクトはコンテントMathMLの中で自然に表現できるという意見は, 後で詳細を述べるより良い仕組みとなっていくでしょう.
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.
次の節は, 詳細にtypeについて議論しています. 続く節は, 可能性のある筋書きを示す数々の例によって, コンテントMathMLに高度な型システムを組み入れるための方法について説明し議論します.
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.
3 より進んだ型分類
Advanced Typing
より洗練された型分類システムを扱うために, 2つの鍵となる課題が解決されなければなりません.
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.
-
型オブジェクトを対応関係にあるMathMLオブジェクトに結び付ける方法を決定します.
Determine a method to associate the type objects with the corresponding MathML object.
2つ目の課題を扱う単純な方法の1つは, MathMLのsemantics要素を使用することです. この要素は, 一般に追加情報を数学オブジェクトに結び付けるのに定義されました. 加えて, この要素は, annotation-xml要素とannotation要素の利用を通じて, XMLに基いたコード化も, XMLに基かないコード化も両方対応しています.
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.
コード化の課題に関して, 数学型システムを開発することが困難な作業であることは, よく知られた事実です. ただし, いくつかのそのようなシステムは存在し, それぞれが開発の努力の主要な部分を表しています. 例としては, OpenMathコンソーシアムによって開発されたSimple Type System[STS]があります. MathMLの付録Cの重要な部分自体が, 型情報の課題やそれらがどのように関係してるかについて扱っています. 幸運にも, semantics要素は, 代替表記に対応するよう設計され, それによって言及された型システムの利用を認めています.
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.
次の節は, semantics要素が型情報を説明するのにどのように利用できるか論じています.
The following section discusses in detail how the
semantics element can be used to describe types.
3.1 semantics要素
The semantics Element
semantics要素は, 特定の数学事象に関係する様々な種類の情報を一緒にまとめるように設計されています. 例えば, semanticsは, 1つの事象に対するコンテントMathMLとプレゼンテーションMathMLの両方の表現を提供するのによく利用されます.
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.
semantics要素は, MathMLの式に対する, その意味の対応付けを一緒にする入れ物要素です. semanticsは, 変更可能な数の子要素を含み, その最初のものは, 付け加えられた追加の意味情報に対する(それ自身が複雑な要素の情報でもよい)数学事象です. 2番目およびそれに続く子要素は, 存在するなら, annotation要素またはannotation-xml要素です. それらの要素それぞれは, definitionURL属性とencoding属性を含むことができます. それらの属性は, 特定のannotation-xml要素の中身の意味を明確化するのに利用でき, それぞれコード化されるときの決まりがあります.
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.
-
annotation要素は, 任意のデータに対する入れ物要素です. このデータは, 加工されていないテキストデータ, 数式処理システムのコード, Cプログラム, 処理プログラムが受け入れる何らかの構文でもよいです. annotation要素は, 利用される形式を定義する"encoding"と呼ばれる属性を含むことができます. annotationの内容モデルはPCDATAで, そのため, 特定のコードがXML処理の決まりと衝突しないように用心しなければならないことに注意して下さい.
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.
-
annotation-xml要素は, XML構文の意味情報に対する入れ物要素です. 例えば, OpenMath意味情報のXML形式は, この要素に含まれることができます. その他の利用可能なものとして, semanticsの最初の子要素でコンテントMathML形式で与えられた構成のプレゼンテーションMathML形式を埋め込むことができます(逆もまた同様です). annotation-xmlは, 利用されている形式を指定するencoding属性を含むことができます.
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.
単純な数式をsemantics要素で置き換えることで, 数学事象に追加の情報を付け加えることができます. 情報の中にはその事象の(いろいろな形式による)様々な側面を見せるものがあってもよく, あるものは, その事象についての型情報となってもよいです. 例えば, 次のとおりです.
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>
この例が示しているように, encoding属性は, 要素の中身をどのように処理するか示すためにメディアタイプと同じように利用されます. その属性は, OpenMath辞書やそのような辞書の特定の項目といった特定のXMLの適用例を使用することを示すでしょう.
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 Objects
数式処理システムの中には, 任意の複雑な型システムへの精巧な対応を行っているものもあります. そのようなシステムは, 例えば, 入力として1つの定数の値の関数を受け取り, 同じような関数を値として返す演算子(例としては微分演算子)を表すという事実といった情報を, 識別子と結び付けることを可能にします. このメモは, 型情報が他のオブジェクト同様, 構造化された数学オブジェクトであるという手法を扱います.
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.
例えば, 整数を自然数に対応付ける関数を示す関数型(Z → R)は, 時々次のように書かれます.
For example, the function type indicating a function
that maps integers to natural numbers (Z
→ R) is sometimes written as:
(integer) --> (naturalnumber)
(この構文は, MathML 2.0勧告の付録Cで書式の構文として使われています.) この関数型は. コンテントMathMLオブジェクトで次のように書けるでしょう.
(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>
採用している型システムを指定し, 記号Z, →, Nの定義を提供するtypes.htmlと呼ばれる文書があるとします. 型オブジェクトZ → Rは, 関数型の構築要素→を整数の集合Zと自然数の集合Nに適用することで得られます.
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.
既存のコンテントMathMLをより直接的に利用して作られる, この関数型の代替表現は次のとおりです.
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>
上の最後の2つの表現は, コンテントMathMLオブジェクトとして型の構造を明確にコード化しています. 型情報のこの表現は, MathMLの利用可能な型情報の集合を, (属性の中でのURIの利用を除いて)type属性に比べて飛躍的に拡張します.
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).
3.3 構造化された型情報とMathMLオブジェクトを結び付ける
Associating Structured Types with MathML Objects.
semantics要素は, 構造化された型情報を(前の節で紹介したように)特定のMathMLオブジェクトと直接結び付けるのに利用可能です. 例えば次のようにです.
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>
semantics要素の2番目の子要素は, テキストデータの型情報を含むannotation要素です. 3番目の子要素は, コンテントMathMLのマークアップを用いた型情報のXML表現を含むannotation-xml要素です.
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.
annotation-xml要素とannotation要素のdefinitionURL属性は, ここでは, 要素の中で提供される性質(この状況では型情報)を指定するのに使用します. annotation-xml要素のencoding属性は, XMLデータの書式を指定します. MathMLソフトウェアは, これらの属性の値を, 型情報を取り扱えるかどうか, すなわち, 特定の型システムに対応しているかどうかを決めるために利用できます.
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.
要約すると, MathML仕様書は, definitionURL属性がsemantics要素の最初の子要素に対する付加情報の関係を指定することから, semantics要素をMathMLオブジェクトへの一般的な付加情報機能として利用することを認めています. 特に, この仕組みは, 数学事象に構造化された型情報を付け加えるのに利用できます. 下記には, コンテントMathMLマークアップを用いて表現された変数XZに対する, OpenMathマークアップでの型付加情報を示したより複雑な例です. (詳細については4 関連する作業: OpenMathにおける型情報を参照して下さい.)
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>
対応関係を明確にするために, 並列のマークアップは, MathML2仕様書の第5.3.4節で説明されている, 相互参照を使用しています.
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>
ここで, 束縛変数Fとxは, semantics要素を使用して型情報が付加されています. 変数の宣言出現と束縛出現の間の対応関係は, 各bvar要素を示しているdefinitionURL属性の利用により明確になります(この技術の議論については[MathMLBVar]を参照して下さい).
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).
この例において, 一般に任意の関数を任意の値に適用することにより0以上の結果を生じることが真実ではないことから, 型情報のみが式を真に(または意義のあるものにさえ)することに注意して下さい.
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.
上の例の情報を表す, bvarの中のsemantics要素を利用しない関連する方法は, 次のとおりです.
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>
ここで, condition要素は, "型Z → Rを持つFのような"型の条件を表すのに使われています. 最初の表現から2番目の表現への変換は, 相対化[Oberschelp]と呼ばれる型付き論理でよく知られた技術で, 意味を変えることなく型付き論理の式を型の付いていない式に変換します. 2つの表現は同じような意味(既知の道理のかなった前提)を持つにも関わらず, 両方とも, ほとんどの型システムで印象的に違った電算の性質を持ちます. よって, それらはコンテントMathMLの中で1つにされるべきではありません.
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.
4
関連する作業: OpenMathにおける型情報
Related Work: Types in OpenMath
OpenMathは, 数学事象のXMLコード化で, 拡張性を持って設計されています. OpenMathとコンテントMathMLは, 表現する能力の点で大まかに言って同等で, 主な違いは, OpenMathは記号を表現するのにcsymbolに似た仕組みを使用することです.
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.
この節では, 簡潔にコンテントMathMLとOpenMathとにおける構造化された型情報について比較します.
In this section we briefly compare the representation of
structured types in content MathML and in OpenMath.
4.1 OpenMathにおける型情報の表現と対応関係
Representing and Associating Types in OpenMath
次に示す表現は, 上記の例に対応するもので, 型情報がどのようにOpenMathで表現されるか示しています.
The 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は, 束縛された事象を表すのにMathMLがapply要素とbvar子要素を使うのに対し, OMBIND要素を使用します(bvar子要素は, OpenMath要素OMBVARに相当しますが, OMBVAR要素は, 複数の変数を持てる点が異なります). OpenMathは, OMA要素を関数の適用に, OMS要素をMathMLのcsymbol要素の代わりに, OMV要素をci要素の代わりに変数に使用します. これらのマークアップは, 直接的にコンテントMathMLに対応します.
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.
前述のコンテントMathMLの例との主な違いは, 付加情報の取り扱いです. MathMLsemantics要素の代わりに, OpenMathは, OMATTR要素を使用します. その最初の子要素はOMATP要素で, "性質と値の組み"を含んでいます. 奇数番目の子要素は, (ときどき"機能"と呼ばれる)それに続く兄弟要素の役割を指定する記号です. 上の場合では, 最初のOMS要素は, そのname属性が値typeを持っており, 次の要素が型情報であると指定しています. OMATTR要素の2番目の要素は, 最初のものの情報が付け加えられたオブジェクトです.
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.
このメモで提案されている構造化された型情報の表現は, コンテントMathMLを型情報に対するOpenMathと同じように表現に富んだものにします. OpenMathOMATP要素における機能記号は, csymbol要素のdefinitionURL属性がOpenMathOMS要素に相当するのと厳格に同じ方法で, annotation-xml要素とannotation要素のdefinitionURL属性の値に正に相当します. MathMLは, OpenMath表現のみを機能の値として認めているOpenMathをわずかにですが一般化しており, MathMLは, 書式をencoding属性で指定できるannotation-xml要素の中で, 任意のXML表現を認めています. annotation要素と同等のものが, OpenMathOMSTR要素によって機能の値として利用できます.
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.
4.2 OpenMathの小規模型システム
OpenMath's Small Type System
OpenMathは, 専用の型システム"小規模型システム(STS)" [STS])に取り組んでいます. (全てのMathML記号と入れ物要素に相当するものを含む)全ての核となるOpenMath記号は, STS型情報を持つことから, この型システムは, STSをコンテントMathMLにおける構造化された型情報を利用する際の良い候補となります. 単純な型システムは, 関数の引数の数を確認するために利用でき, MathML 2仕様書の付録Bでの内容検証構文と大まかに同じ情報を表します.
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.
STSシステムによって提供される記号は, stsOpenMathコンテント辞書で見ることができます. 2 type属性で論じたtype属性で利用される値に相当する記号は, mathmltypesコンテント辞書で見ることができます. definitionURL属性の対象としてコンテント辞書を用いることは, 次の3つの表現を同等にします.
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 MathML 2 付録Cで使われる型情報
Types as used in appendix C of MathML 2
MathMLで数学型情報が挙げられる主な場所は, 付録Cで定義されている様々なオブジェクトのシグネチャの中です.
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:
- シグネチャ
signature
-
シグネチャは, いろいろな可能性のある性質の組合せの型情報や関数の引数を, 構成された数学オブジェクトの型情報と結び付ける体系的な表現です. 可能性のある変換や引数の型情報の組合せ(左辺)はそれぞれ何らかの型情報のオブジェクト(右辺)に帰着します. 基本的には, どのように演算子の上書きを解決するかについて説明しています.
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.
構築要素に対して, シグネチャの左辺は, 子要素の型情報について説明し, 右辺は, 構築されたオブジェクトの型情報について説明します. 関数に対して, シグネチャの左辺は, 関数が適用されるときに期待されるであろう変数や引数の型情報を示すか, 関数を構成するために利用されるかし, 右辺は, applyによって構成されるオブジェクトの数学型情報を表します. 修飾要素は, 既存のオブジェクトの性質を修飾します. 例えば, 記号はベクトル型の記号になるかもしれません.
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>)
MathML属性が存在するなら, 形式<name>=<value>の中に現れます. それらは, 表記上, 残りの引数と角がっこで仕切られます. 可能性のある値は, 一般に列挙された一覧から選ばれ, シグネチャは, 一般に特定の値の選択によって影響を受けます.
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.
左辺にある実際の関数の引数や名前付き変数に対して, 焦点となるのは, 関係する数学型情報です. 関数の引数の型情報は, 1つの主要な例外を除いてDTDに用いられるものとよく似た構文で表されます. 名前付き変数は, 属性値に用いられるのと類似した決まりに従って<elementname>=<type>としてシグネチャの中に現れます. 例えば, 引数が(例えばbvarと)名付けられている場合, このことは, 次のような等式によってシグネチャの中で表されます.
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>)
MathMLには, 公式な型システムがありません. シグネチャで用いられる型の値は, (cnの説明で見られるような)integer, rational, real, complexといった一般的な数学型や, 文字列やMathML構築要素名といった名前です. anything, matrixtypeといった型情報の様々な集合は, 時々使用されます. 型名mmlpresentationは, 何らかの有効なプレゼンテーションMathMLオブジェクトを表すのに用いられ, MathMLtypeという名前は 全てのMathML型情報の集合を説明するのに用いられます. algebraicといった型は, 算術演算を通じて複数の記号から構成される式で使用されます. interval-typeは, 第4章で定義された範囲の有効な型を参照します. 型情報の集合は拡張可能です. 新しい構成の独自の定義を書く利用者は, 新しい型情報を導入してもよいです.
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.
結果として生じた式の型情報は, 被演算子の型情報やMathML属性の値に依存します.
The type of the resulting expression depends on the types of the
operands, and the values of the MathML attributes.
例えば, csymbolの定義は, 次の形式を取るシグネチャを提供します.
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.
expといったより伝統的な数学関数のシグネチャは次のように与えられます.
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
この例は, "内積"演算子の型情報を示しています. 概念的に, この演算子は, 最初の引数にn次元ベクトル, 次の引数にn×m行列, そしてm次元ベクトルを返します. 下記の例の型情報は, "全てのαtypeに対して, nZ, mZ.
vector(n,α)
×
matrix(n,m,α)
→
vector(m,α)"と説明できるでしょう. これは, いわゆる"普遍的な型"で, すなわち, 全ての型と全ての自然数n, mに対して, 内積演算子は, 適切な関数の型を持ちます. この型システムにおいて, 型情報は型付き変数自体を含み, 例えば, nとmは整数であるという型情報を持たされることに注意して下さい. さらに, 型情報は, α型の要素のn次元ベクトル型を構築するのに, 自然数nと型情報αを持つベクトル型の構築要素のように, "型情報構築要素"の高度な集合を持つことに注意して下さい.
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>