MathMLにおける束縛変数
Bound Variables in MathML

1 導入
Introduction

束縛変数は, 数学の言葉において, 主要な表現の基本となるものです. これらは, 関数, 量化, 修飾要素付きの演算子を表現する事を認めています. MathML2.0勧告の第1版[MathML2]は, 束縛変数の同一性の条件についてややあいまいでした. 例えば, その勧告の全ての例で単純なci要素が使われています. そのため, 束縛変数の実例が定義出現として同じものか疑う余地がありません. 実際のところ, 同一性の問題は, ci要素の中でより精密な表現を使用し始めたときにのみ深刻に生じます. コンテントMathMLのソフトウェアは, semanticsタグや書式属性の大量の利用の影響下にある場合に, できる限り2つの表現が等しいと決めようとするのを避けていました. どのくらい広範囲にわたって, ci要素を数学的に変更すること無しに, (たとえ, 表示目的であっても)修正できるでしょうか?

Bound variables are central representational primitives in mathematical languages. They allow one to express functions, quantification, and operators with qualifiers. The first edition of the MathML 2.0 Recommendation [MathML2] was vague about the identity conditions on bound variables. For example, all examples in that Recommendation use simple ci elements, for which there is never any doubt when an instance of the bound variable is the same as the defining occurrence. In fact, the question of identity only seriously arises when one starts to use more elaborate presentations inside of the ci elements. Content MathML applications were left trying to decide when two presentations are equal, possibly in the presence of heavy use of semantics tags and/or styling attributes. How extensively could a ci element be modified (even for presentational purposes) without changing it mathematically?

この問題に対する安全な回答は"少しもない"でした. ただし, 少なくとも表現の1つは, 数学的同一性を保ったまま説明的な目的で変更される必要があり, そのような正式な例が存在しました. さらにMathML2.0勧告の第1版[MathML2]は, この点で精巧なものではありませんでした.

The safe answer to this question was "not at all", but there were legitimate examples where at very least one of the presentations needed to be changed for expository purposes while retaining the mathematical identity. Furthermore, the first edition of the MathML 2.0 Recommendation [MathML2] did not elaborate on this point.

このメモは, 束縛変数の実例の承認を確実にし, どのように意味情報を扱う既存の仕組みがプレゼンテーションマークアップの直接比較に依存せずに, そのような同一性説明を行うために利用できるか示します. このことは, MathML2.0勧告の第2版[MathML22e]における束縛変数の同一性の概念を明確にするのに用いられる手法です.

This Note investigates the recognition of instances of bound variables and shows how existing mechanisms for dealing with semantics can be used to make such identifications explicit without depending on the direct comparison of the presentational markup. This is the approach that has been used to clarify the notion of identity of bound variables in the second edition of the MathML 2.0 Recommendation [MathML22e].

2 課題
The problem

複雑なプレゼンテーションMathMLの付加情報が使われる場合, bvar要素で定義出現が生じていないciの特定の実例と結び付けることは, 確立しづらいでしょう. また, MathML2.0勧告の第1版[MathML2]は, そのような方法を指定しませんでした. 単独でXML構造に基づいた(ひょっとしたらXML情報セットに基づいた)同一性の厳密な定義は, とても制限されるであろうことに注意して下さい.

When complex Presentation MathML annotations are used, the association of a particular instance of a ci with its defining occurrence in the bvar element can be difficult to establish, and the first edition of the MathML 2.0 Recommendation [MathML2] did not specify a way to do so. Note that a strict definition of identity based solely on the XML structure (possibly based on the XML Information Set) would be too restrictive.

(MathML2.0勧告の第1版[MathML2]での全ての例を含め)最も純粋なコンテントMathMLの場合は, 何も問題はありません. bvar要素の中身は単独のciで, その中身は単独な文字列です. 空白を正規化した後に同じ名前を持つapply要素の中のciがbvar宣言によって束縛される場合, 若干の疑いが生じます.

In most purely Content MathML cases (including all the examples in the the first edition of the MathML 2.0 Recommendation [MathML2]) there is no problem; the content of the bvar element is a single ci, whose content is just a simple character string. There is little doubt that any ci in the body of the apply element that have the same name after whitespace normalizations is bound by the bvar declaration.

<apply>
  <int/>
  <bvar><ci>x</ci></bvar>
  <interval><cn>0</cn><cn>1</cn></interval>
  <apply>
    </plus>  
    <apply><power/><ci>x</ci><cn>2</cn></apply>
    <apply><times/><cn>2</cn><ci>x</ci></apply>
    <cn>5</cn>
  </apply>
</apply>

しかしながら, 勧告は, ci要素の中に任意のプレゼンテーションMathMLを入れることを認めており, この機能は, 下付き・上付き添え字や別のフォントの変数に対してよく用いられます. これらの場合に, どの変数がbvar宣言によって束縛されているか, より明確でなくなります. 例えば, 単純な色の変更は, 上の例の変形である次の例の中で, 束縛変数の実例の1つに注意を引くのに用いられるかもしれません.

However, the Recommendation does allow arbitrary Presentation MathML inside a ci, element and this feature is often used for variables with sub/superscripts, or variables in different font families. In these cases, it becomes less clear which variables are bound by the bvar declaration. For example a simple color change might be used to draw attention to one of the instances of a bound variable as in the following variant of the the above example.

<apply>
  <int/>
  <bvar>
    <ci>
      <mstyle color="red">
	<msub><mi>x</mi><mn>2</mn></msub>
      </mstyle>
    </ci>
  </bvar>
  <interval><cn>0</cn><cn>1</cn></interval>
  <apply>
    </plus>  
    <apply><power/><ci><msub><mi>x</mi><mn>2</mn></msub></ci><cn>2</cn></apply>
    <apply><times/><cn>2</cn><ci><msub><mi>x</mi><mn>2</mn></msub></ci></apply>
    <cn>5</cn>
  </apply>
</apply>

このメモの目標は, 束縛変数としての主要な役割を無くすこと無しに, どのように束縛変数の表示情報を用いるかを明確にすることです.

The goal is to clarify how to use presentational information on bound variables without losing track of their essential role as bound variables.

3 論理学や数学的基盤における束縛変数の背景
Background on bound variables in logics and mathematical foundations

束縛変数を取り扱う際の課題は, ここ百年の間, 論理学や数学的基盤において幅広く研究されてきました. 実際のところ, 束縛変数の取り扱いは, 数学的基盤の集合論の基本となる一階論理学のフレーゲによる取り扱いによって寄与された部分が大きいです。この節は, この文書の残りの部分で使用する用語を定義します.

The problem of handling bound variables has been studied extensively in logic and the foundations of mathematics in the last one hundred years. In fact the handling of bound variables was the main contribution of Frege's treatment of first-order logic that is the basis for the set-theoretic foundation of mathematics. This section defines the terminology that will be used in the rest of this document.

O x.B[x]という形の式において, Oが束縛する演算子であるなら, 変数は[定義: 束縛変数]と呼ばれます. B[x]を識別子xを含んでもよい([定義: 本体]と呼ばれる)式に対して使用します. 演算子Oの後に直接xが出現することを[定義: 宣言出現]と呼び, 本体の中での出現を[定義: 束縛出現]と呼びます.

A variable is called a [Definition: bound variable] in an expression of the form O x.B[x] , if O is a binding operator. We use B[x] for an expression (called the [Definition: body]) that may contain the identifier x. The occurrence of x directly after the operator O is called the [Definition: declaring occurence] and those in the body are called the [Definition: bound occurrences].

一階論理学(および全ての他の数学的基盤)において, 束縛変数は, 2つの決定的な性質を持っています.

In first-order logic (and all other foundations of mathematics), bound variables have two crucial properties:

• [定義: 束縛変数識別子] 束縛変数識別子(BVI)は, 量化記号(または, 総和, 総積, 極限,...といった一般的な束縛する演算子)によって宣言され, 束縛変数の全ての他の出現は, その"宣言"出現への単なる参照です. 束縛する演算子の影響範囲外では, 束縛変数は見えません.

  [Definition: Bound Variable Identity ] Bound variables (BVI) are declared by the quantifier (or generally the binding operator such as a sum, product, limit,...) and all other occurrences of the bound variable are just references to this "declaring" occurrence. Outside the scope of the binding operators, bound variables are invisible.

• [定義: 束縛変数名称] 束縛変数名称(BVN)は, 伝統的な記号表現のために提供されています. このことは, 式のツリー構造の中で機能的に依存した, 線形化した(数式のような)表現を認めています. 例えば, 次のようにです.

  [Definition: Bound Variable Names ] A bound variable name (BVN) is provided for the traditional symbolic presentation. This allows for a linearized (formula-like) representation of the functional dependency in formula-trees, as in

  全てのxに対して x > 1 → x² > x

  For all x. x > 1 → x² > x

  これらの変数名は定義範囲外では本質的に重要でないという論理学の要件に矛盾しないように, 文字による名前変更の決まりは, 体系的に束縛変数の名前を変更することを認めています. 特に, 上の式は, 次の式に数学的に等しいです.

  To be consistent with the logical requirement that names are essentially irrelevant outside their scope, the rule of alphabetic renaming allows one to systematically rename bound variables. In particular, the expression above is mathematically equivalent to

  全てのyに対して y > 1 → y² > y

  For all y. y > 1 → y² > y

束縛変数識別子(BVI)と束縛変数名称(BVN)は, 両方とも束縛変数の本質的な側面です.

Both bound variable identity (BVI) and bound variable names (BVN) are essential aspects of bound variables.

束縛変数識別子は, 束縛変数の意味している本質を提供します. (明確な)束縛変数の無い数学(圏論, 組合せ論理, ド・ブラウン・インデックス)の式がありますが, それらは, 人が理解するにはたいてい難しいです.

Bound variable identity provides the semantical essence of bound variables. There are formulations of mathematics without (explicit) bound variables (Category theory, combinatory logic, De Bruijn Indices), but they are usually hard for humans to understand.

束縛変数名称は, 人が関係する式を理解することを手助けします. 実際のところ, 直観的でない名前の変更は, 理解できない複雑な式を描くでしょう. このことは, 上で説明された変数が自由な論理学が, 意思疎通の道具ではなく理論的な道具に留まっている理由でもあります.

Bound variable names help humans understand the formulae involved. In fact, un-intuitive renaming can render complex formulae unintelligible. This is also the main reason why the variable-free logics mentioned above have remained theoretical tools rather than communication devices.

4 分析
Analysis

MathML2.0勧告の第1版[MathML2]において, コンテントMathMLは, 明確にBVNに基づいた束縛変数の表現にのみ対応していました(プレゼンテーションMathMLであるciの中身のみが, 同一性証明のために用いられていました). 結果として, 同一性の問題を解決することは困難で, その問題の解決が, コンテントMathMLの式・オブジェクトの正式な取り扱いには必要でした.

In the first edition of MathML 2.0 [MathML2] Content MathML only explicitly supported a BVN-based representation of bound variables (only the Presentation MathML ci content could be used for identification). As a consequence, it was difficult to decide the identity question, a resolution of which was needed for formal treatment of Content MathML formulae/objects.

このことは, 名前が単純である限りは, ほとんどの場合に問題にはなりません. ただし, 名前が複雑な(プレゼンテーションMathMLの)オブジェクトを含む場合, BVNに基づいた仕様書は, 束縛出現が宣言出現を参照しているときの課題に取り組むことを潜在的に避けてきました. 例えば, 式の意味をコード化するために解決されるべき主要な課題に対してです.

This is not a problem in most cases, where names are simple. However, when names involve complex (Presentation MathML) objects, the BVN-based specification potentially leaves open the issue of when a bound occurrence refers to a declaring occurrence -- the central question to be resolved in order to decode the meaning of the expression.

実をいうと, 束縛変数をその定義出現と一緒に特定するために, 若干の賢明な選択肢があります. これらは次のものを含みます.

There are really only a few sensible choices for identifying a bound variable with its defining occurrence. They include:

• XML情報セットが同等: 2つのプレゼンテーションMathMLの名前は, それらの情報セットが等しい場合に等しいです. この基準は, おそらくXMLによって最も対応されています. (付録Aと同等の一般的な議論を参照して下さい.)

  XML-Infoset-equality: two Presentation MathML names are equal, if and only if their infosets are. This criterion is probably best supported by XML. (See appendix A and a general discussion of equality)

• 明確なリンク: (HELMプロジェクト(注釈:数学のハイパーテキスト電子図書館プロジェクト)で使われているような)宣言出現または束縛変数への特定のリンクを導入します.

  Explicit links: introducing some specific link to the declaring occurrence or the binding operator (such as used in the HELM project).

表現が同等かどうかの全ての課題は, 画像が等しいかどうかの課題のように複雑になるので, XML情報セットによる手法は, 複雑な表現に対しては非現実的です. このBVNに基づいた同一性証明の枠組みは, せいぜい電算上で高価な等しい表記を導き出すだけです.

The XML-Infoset-equality approach is impractical for complicated presentations where the whole issue of equivalence of presentations becomes as complicated as the issue of equivalence of images. This BVN-based identification schema leads at best to computationally expensive equality notions.

しかしながら, 束縛変数の定義出現への明確なリンクは, 特により困難な状況での利用に対して選択可能な代わりの同一性の証明の枠組みを提供できます. それらのリンクは, 束縛変数識別子(BVI)を明確にし, 実装は, MathMLの既存の枠組みを自然に直観的に利用するものになります. このような手法の有利な点は次のものを含みます.

However, explicit links back to the defining occurrence of a bound variable can provide an optional alternative identification schema especially for use in the more difficult cases. These links make the bound variable identification (BVI) explicit and the implemenation makes natural and intuitive use of existing machinery in MathML. The advantages of such an approach include:

仕様書:
specification:

設計によって, プレゼンテーションMathMLは, 2つのかなり制御された方法でコンテントMathMLの中で許されています. このことは, (しばしば画像のように)ci要素の中で起こってもよいですし, semantics要素を通じて結び付けられてもよいです. やっかいな状況は, ci要素の中身の場合です. このことが導入されたときの見た目は, プレゼンテーションMathMLが埋め込まれた画像に類似したようなものです. 分析できない素子要素になったでしょう. より複雑なものは, semanticsタグを利用して対応されるべきです. 画像と同じように, 2つのci要素は, 等しいsrc属性によって正式に定義されているような本質的に同一な場合のみ等しいです. (視覚的に見分けが付かないにも関わらず)2つの完全に異なるプレゼンテーションMathMLの中身を持つci要素を等しいと思うことは, 2つの異なるファイルや書式を持つ画像を同一と思うことと同じです. そのオブジェクトを"分析"することや潜在的に複雑な分析を行うこと無しでは, 等しいことを決定することは不可能です.

By design, presentation is permitted in Content MathML in only two rather controlled ways. It may occur (much like an image) inside a ci element, or it may be tied in via the semantics element. The troublesome case is the content of ci. The view taken when this was introduced was that such presentation was analogous to embedding an image. It was to be an indecomposable token. Anything more complicated was to be done using semantics tags. By analogy with images, two ci elements are equal just if they are essentially identical which may formally defined by equality of the src attributes. Expecting ci elements with two completely different presentation contents (albeit visually indistinguishable) to be equivalent would be the same as expecting images in two different files and/or formats to be identical. Short of "decomposing" the objects and doing some potentially complicated analysis, equivalence could not possibly be determined.

電算:
computation:

コンテントMathMLの表現を他の内容の書式に変換する必要がある場合, 束縛変数の束縛関係は, 特定されなければなりません. BVNに基づいた手法では, このことは, プレゼンテーションMathMLの表現として変数名の等しさを計算する必要が生じるでしょう. ここで必要とされるであろう洗練された同等かの試験は, XMLソフトウェアでよく対応されている訳ではありません. 特別なXML差分プログラムの中には, 暗に実装しているように見えるものもあります. したがって, このことがより正式な設定の中でコンテントMathMLを採用する深刻な課題であるように, とてもたくさんの要因があります.

When there is a need to transform Content MathML representation into other content formats, the binding relation of the bound variables must be identified. In a BVN-based approach, this entails the need to compute the equivalence of variable names as Presentation MathML representations. The sophisticated equality tests that may be needed here are not very well-supported by XML tools - some sort of specialized XML diff program appears to be implied. Thus, there are too many factors such This is a serious problem the adoption of Content MathML in more formal settings.

互換性:
compatibility:

OpenMath [OpenMath]は, BVIに基づいた手法に基づいています. OMV要素は空要素で, 名前を持ちません.

OpenMath [OpenMath] is based on a BVI-based approach; OMV elements are empty, they do not have names.

5 束縛変数の同一性証明のためのdefinitionURL利用
Using definitionURL for Bound Variable Identification.

既存のソフトウェアとの互換性は重要です. よって, 解決策は, 束縛変数の既存のBVNに基づいた取り扱いを, 利用者に対し束縛変数の同一の条件を明確にするBVIに基いた取り扱いと同様に, 名前だけから明らかでない場合, 改良しなければなりません.

Compatibility with existing applications is important. Thus the solution must augment the existing BVN-based treatment of bound variables with a BVI-based treatment that allows the user to make the identity condition of bound variables clear, where it is not obvious from the name alone.

このことは, 束縛されたci要素でbvar要素によって特定されている宣言の実例を指し示すdefinitionURL属性の利用を通じて, 次の例のように成し遂げられます.

This can be accomplished through the use of the definitionURL attribute on the bound ci element to point to the declaring instance as identified by the bvar element, as in the following example

<lambda>
  <bvar>
    <ci id="the-boundvar">complex presentation</ci>
  </bvar>
  <apply>
    <plus/>
    <ci definitionURL="#the-boundvar">complex presentation</ci>
    <ci definitionURL="#the-boundvar">complex presentation</ci>
  </apply>
</lambda>

"複雑な表現"が出現の度に同一かどうか計算する代わりに, definitionURL属性が同じ宣言されたci要素を指し示しているかどうか確認するだけで済みます. definitionURLの中身はURIで, (URLはウェブの基本であり)よく理解された同一の条件です.

Instead of computing whether "complex presentation" is identical in each occurrence, it is only necessary to check whether the definitionURL point to the same declared ci. The content of the definitionURL is a URI, which has well-understood identity conditions (URIs are the basis of the Web).

もちろん, 束縛変数に対するこのBVIに基いた手法の利用は, 束縛変数の意味を明らかにする方法として, 厳密に選択可能なだけです.

Of course, use of this BVI-based approach to bound variables is a strictly optional way of clarifying bound variable semantics.

<declare definitionURL=".../formalpowerseries"><ci>F</ci></declare>
<apply>
  <set/>
  <bvar><ci>F</ci></bvar>
  <condition>
    <apply>
      <in/>
      <ci>F</ci>
      <csymbol definitionURL="XXX">My Special Formal PSeries</csymbol>
    </apply>
  </condition>
  <ci>x</ci>
</apply>

<declare>
  <ci definitionURL="#the-bvar">F</ci>
  <semantics>
    <ci definitionURL="#the-bvar">F</ci>
    <annotation-xml definitionURL="types.html#type_of">
      <csymbol definitionURL=".../formalpowerseries"/>
    </annotation-xml>
  </semantics>
</declare>
<apply>
  <set/>
  <bvar><ci id="the-bvar">F</ci></bvar>
  <condition>
    <apply>
      <in/>
      <ci definitionURL="#the-bvar">F</ci>
      <csymbol definitionURL="XXX">My Special Formal PSeries</csymbol>
    </apply>
  </condition>
  <ci>x</ci>
</apply>

6 結論
Conclusion

このメモは, コンテントMathMLにおける束縛変数を含む数学事象を表現するための手引きです. このメモは, ワールド・ワイド・ウェブ・コンソーシアム(W3C)の数学作業部会の現時点の合意を表していますが, 規範ではありません.

This Note provides guidelines for representing mathematical objects containing bound variables in Content MathML. The Note represents the current consensus in the Math Working Group of the World Wide Web Consortium (W3C), but is not normative.