Bound Variables in MathML

1 Introduction

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?

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.

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

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.

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>

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.

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].

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

• [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.

• [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

  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

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

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

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.

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-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)

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

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.

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:

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:

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] is based on a BVI-based approach; OMV elements are empty, they do not have names.

5 Using definitionURL for Bound Variable Identification.

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.

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>

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).

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

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.