I propose to extend the pragmatic syntax of OpenMath by records. Record structures are utilized ubiquitously for representing objects and accessing their components in programming, and we show that this is true for mathematical practice at the informal but rigorous level as well, even though at the formal level records can be reduced to tuples or partial functions. This situation makes records an ideal case study for an OpenMath language extension (OLE) proposed in a sibling paper.
(1) We call a triple R := (R; +; ) a ring, i . . . . R is called the base set of R, + and called the additive and multiplicative operations of R. are (2) We call a ring commutative i its multiplicative operation is. (3) Let R := (R; +; 0; ; ; 1) be a ring, . . .
These two examples that can be found in any book on elementary algebra already show that we often deal with complex structures made up of simpler structures. Standard mathematical practice establishes a conceptual infrastructure for such structures that goes beyond the minimal requirements of using tuples for that. Two practices are salient here:
1OpenMath objects also include mathematically relevant primitive data types for numbers and strings, but these are irrelevant to this paper.
2We will use the short-hand notation @(f; a1; : : : ; an) for the OpenMath application of the function f to the argument sequence a1; : : : ; an and (s; v; A) for the OpenMath binding with binder s (a symbols) over bound variable x and body A. 1. Even though the rst de nition calls R a triple (it is made up of three components), standard names { we call them accessors for the purposes of this paper { are introduced for the the components, and these are used to refer to the components { see e.g. (2) if they are not given local names. In (1) and (1) the accessors are verbal symbols, which are usually only be used in verbalizations of mathematical objects, accessors can be used in formulae as well, e.g. the accessors i for the ith component of a tuple. 2. The set of accessors for a given structure is variable: while (1) sees a ring as a triple, (3) represents it as a 6-tuple, including the two units and inverse for the additive operation into the mix. Mathematically, this makes sense, since units in monoids and inverses in groups are uniquely determined. The representational exibility of treating de ned functions like \unit-of" at par with the de nitional ones like \base-set-of" makes working with complex structures like vector space homomorphisms (which naturally have between 13 and 35 accessors) tractable.
In programming, a similar situation has led to the development of object-oriented programming, which in turn has been analyzed/formalized in terms of record structures. 2
Record structures are basic data structures whose components are referenced by a xed set of names. They can be formalized as tuples with (named) projections for accessors, and they can be typed by \record types" { i.e. types that are structurally records with the same accessors { in standard ways. In our example, we could represent R = (R; +; ) as the record R = [set = R; addop = +; mulop = ]. Component selection traditionally goes via the \dot operator": e.g. R:set = R. For OpenMath we propose that the accessors are special symbols.
Note that record structures are syntactically similar to { but not identical with { semantic annotations in OpenMath. The latter are represented by OMATP elements in the XML encoding of OpenMath. But OMATP is only allowed as the second child of an OMATTR element, i.e. as \property lists" to an OpenMath object. The situation in content MathML is similar: the annotation xml elements (which correspond to key/value pairs) are only allowed in semantics elements which has a content MathML expression as the rst child. So even though we can represent [set = R; addop = +; mulop = ] as in Listing 1 we cannot use it as a rst-class object, in particular, we cannot just use it as in Figure 1a { here we use the boxed record expression as a gloss for the OpenMath expression in Listing 1.
Listing 1: A record as an OpenMath OMATP <OMATP> <OMS cd=”ring” name=”set”><OMV name=”R”/> <OMS cd=”ring” name=”addop”><OMV name=”plus”/> <OMS cd=”ring” name=”mulop”><OMV name=”times”/> </OMATP> Therefore we propose to lift the OMATP symbols into the rank of an OpenMath object for records, essentially making the syntax in Figure 1a legal. We also propose speci c syntax for a rst-class record selection operator as in Figure 1b.
Note that we formulate our extension request as a request for a language extension in the sense of [Koh14]. That calls for a
1. pragmatic syntax (which we have speci ed above), <OMA> <OMS cd=”relation1” name=”eq”/> <OMV name=”R”/> [set = R; addop = +; mulop = ] </OMA> <OMSEL> <OMV name=”R”/> <OMS cd=”ring” name=”set”/> </OMSEL> (a) Proposal: OMATP as an OpenMath Object.
(b) Proposed Record Selection 2. a set of equations { we take the standard ones: [k1 = v1; : : : ; kn = vn]:ki = vi and [k1 = r:k1; : : : ; k1 = r:k1] = r, if k1; : : : ; kn are the accessors of r, and 3. a content dictionary for records in OpenMath 2 syntax together with a translation of record expressions into OpenMath 2 expressions.
As there are various ways of formalizing records, we will leave the speci cation of the CD to future work. 3
We have argued for the need of a language extension to provide rst-class syntax for records in OpenMath. We have identi ed one possible syntax reusing the existing OMATP element providing a new OMSEL element. [Koh14]